Any fun

Hi,

had just liked to flip over a predicate transformer  that I tinkered
with today.

------------------------------------------------------------------------------
                                          (   n : Nat   !
data (---------!  where (------------! ;  !-------------!
     ! Nat : * )        ! zero : Nat )    ! suc n : Nat )
------------------------------------------------------------------------------
     (  n : Nat  !                                (     i : Fin n      !
data !-----------!  where (------------------! ;  !--------------------!
     ! Fin n : * )        ! fz : Fin (suc n) )    ! fs i : Fin (suc n) )
------------------------------------------------------------------------------
     (  A, B : *  !        (     a : A      !    (     b : B      !
data !------------!  where !----------------! ;  !----------------!
     ! Or A B : * )        ! inl a : Or A B )    ! inr b : Or A B )
------------------------------------------------------------------------------
     ( n : Nat ;  P : Fin n -> * !                            
let  !---------------------------!                            
     !        Any n P : *        )                            
                                                               
     Any n P <= rec n                                          
     { Any n P <= case n                                      
       { Any zero P => Fin zero                                
         Any (suc n) P => Or (Any n (lam i => P (fs i))) (P fz)
       }                                                      
     }                                                        
------------------------------------------------------------------------------
     ( n : Nat ;  P : Fin n -> * ;  p : Any n P !                        
let  !------------------------------------------!                        
     !           findex n P p : Fin n           )                        
                                                                         
     findex n P p <= rec n                                                
     { findex n P p <= case n                                            
       { findex zero P p <= case p                                        
         findex (suc n) P p <= case p                                    
         { findex (suc n) P (inl a) => fs (findex n (lam i => P (fs i)) a)
           findex (suc n) P (inr b) => fz                                
         }                                                                
       }                                                                  
     }                                                                    
------------------------------------------------------------------------------
     ( n : Nat ;  P : Fin n -> * ;  p : Any n P !                
let  !------------------------------------------!                
     !      find n P p : P (findex n P p)       )                
                                                                 
     find n P p <= rec n                                        
     { find n P p <= case n                                      
       { find zero P p <= case p                                
         find (suc n) P p <= case p                              
         { find (suc n) P (inl a) => find n (lam i => P (fs i)) a
           find (suc n) P (inr b) => b                          
         }                                                      
       }                                                        
     }                                                          
------------------------------------------------------------------------------
     ( A : * ;  B : A -> * !        (  a : A ;  b : B a   !
data !---------------------!  where !---------------------!
     !    Sigma A B : *    )        ! tup a b : Sigma A B )
------------------------------------------------------------------------------
     ( n : Nat ;  P : (Fin n) -> * ;  p : Any n P !  
let  !--------------------------------------------!  
     !      chexist n P p : Sigma (Fin n) P       )  
                                                     
     chexist n P p => tup (findex n P p) (find n P p)
------------------------------------------------------------------------------

I was hoping it could be useful for formulating the pigoeon hole
principle.

------------------------------------------------------------------------------
     ( i : Fin (suc n) ;  j : Fin n !        
let  !------------------------------!        
     !    thin i j : Fin (suc n)    )        
                                             
     thin i j <= rec i                        
     { thin i j <= case i                    
       { thin fz j => fs j                    
         thin (fs i) j <= case j              
         { thin (fs i) fz => fz              
           thin (fs i) (fs j) => fs (thin i j)
         }                                    
       }                                      
     }                                        
------------------------------------------------------------------------------
     (  A, B : *   !        (   a : A ;  b : B   !
data !-------------!  where !--------------------!
     ! And A B : * )        ! pair a b : And A B )
------------------------------------------------------------------------------
     ( n : Nat ;  P : Fin n -> * !                              
let  !---------------------------!                              
     !        All n P : *        )                              
                                                               
     All n P <= rec n                                          
     { All n P <= case n                                        
       { All zero P => Fin (suc zero)                          
         All (suc n) P => And (All n (lam i => P (fs i))) (P fz)
       }                                                        
     }                                                          
------------------------------------------------------------------------------
     (  i ;  j   !                      
data !-----------!  where (-------------!
     ! H i j : * )        ! occ : H i j )
------------------------------------------------------------------------------
[     ( n : Nat ;  p : All (suc n) (lam i => Any n (lam j => H i j)) !!
!let  !--------------------------------------------------------------!!
!     ! PHP n p : Any n (lam j => Any (suc! (lam i =>            !!  !!
!     !                 !             !% n) !  And (H i j)       !!  !!
!     !                 !                   !  % (H (thin i j) j)))  )]
------------------------------------------------------------------------------

Cheers,
Sebastian