N:: Set = data zero
         |S (n:: N)

Plus (A :: Set) 
     (B :: Set)
     :: Set
     = data   i (a:: A)
            | j (b:: B)

Pi (A :: Set)
   (B :: A -> Set)
   :: Set
   = (a::A) -> B a

Sigma (A :: Set)
      (B :: A -> Set)
      :: Set
      = data
        p (a :: A) (b :: B a)

W (A :: Set)
  (B :: A -> Set)
  :: Set
  = data 
    sup(a :: A) (b:: B a -> W A B)


package pi3refl  =

 mutual

  Ubb :: Set =

      data
             Nhat 
           | Plushat  (a:: Ubb) (b:: Ubb) 
           | Pihat    (a:: Ubb) (b:: Sbb a -> Ubb) 
           | Sigmahat (a:: Ubb) (b:: Sbb a -> Ubb) 
           | What     (a:: Ubb) (b:: Sbb a -> Ubb) 
           | univ (u:: Univ)


  Sbb (u:: Ubb) :: Set = case u of 
                             (Nhat) ->  N
                             (Plushat a b) ->    Plus 
                                                 (Sbb a) 
                                                 (Sbb b)
                             (Pihat a b)  ->     Pi 
                                                 (Sbb a) 
                                                 (\(x:: Sbb a)-> Sbb (b x) )
                             (Sigmahat a b)  ->  Sigma
                                                 (Sbb a) 
                                                 (\(x:: Sbb a)-> Sbb (b x) )
                             (What a b)  ->      W 
                                                 (Sbb a) 
                                                 (\(x:: Sbb a)-> Sbb (b x) )
                             (univ u') ->        U u' 

  Univ :: Set = data 
                  su0  ( a0:: Ubb)
                       ( a1:: Sbb a0 -> Ubb)
                       ( f :: (a :: Ubb) -> (Sbb a -> Ubb) -> Ubb) 
                       ( g :: (a ::  Ubb)-> (b:: Sbb a -> Ubb)
                               -> (c:: Sbb(f a b))-> Ubb) 
                       ( n :: M)
                 |su1  ( u :: Univ)
                       (a0 :: U u)
                       (a1 :: Sbb (That u a0) -> U u) 
                       ( f :: (a :: U u) -> (Sbb (That u a) -> U u) -> U u) 
                       ( g :: (a ::  U u)-> (b:: Sbb (That u a) -> U u)
                               -> (c:: Sbb (That u (f a b)))-> U u) 
                       ( i :: tau
                              (m u) 
                              (That u a0) 
                              (\(x:: Sbb (That u a0))-> That u (a1 x)))

  U (u:: Univ) :: Set
    = data
      Nhat
      | Plushat  (a:: U u)
                 (b:: U u)
      | Pihat    (a:: U u)
                 (b:: Sbb (That u a) -> U u )
      | Sigmahat (a:: U u)
                 (b:: Sbb (That u a) -> U u )
      | What     (a:: U u)
                 (b:: Sbb (That u a) -> U u )
      | a0hat    
      | a1hat    (a :: Sbb (a0lift u))
      | fhat     (a:: U u)
                 (b:: Sbb (That u a) -> U u )
      | ghat     (a:: U u)
                 (b:: Sbb (That u a) -> U u )
                 (c:: Sbb (flift u a b))
      | suhat    (a0 :: U u)
                 (a1 :: Sbb (That u a0) -> U u)
                 (f :: (a :: U u)->(b:: Sbb (That u a) -> U u) -> U u)
                 (g :: (a :: U u)->(b:: Sbb (That u a) -> U u)
                       ->(c :: Sbb (That u (f a b))) 
                       -> U u)
                 (i  :: tau
                        (m u)
                        (That u a0)
                        (\(x :: Sbb(That u a0))-> That u (a1 x))) 
      | tuhat    (a0 :: U u)
                 (a1 :: Sbb (That u a0) -> U u)
                 (f :: (a :: U u)->(b:: Sbb (That u a) -> U u) -> U u)
                 (g :: (a :: U u)->(b:: Sbb (That u a) -> U u)
                       ->(c :: Sbb (That u (f a b))) 
                       -> U u)
                 (i  :: tau
                        (m u)
                        (That u a0)
                        (\(x :: Sbb(That u a0))-> That u (a1 x))) 
                 (a ::  U (SU1hat u a0 a1 f g i))


              

  That (u:: Univ)
       (a:: U u) 
       :: Ubb       
       = case a of 
        (Nhat)         -> Nhat@Ubb
        (Plushat a' b) -> Plushat@Ubb 
                          (That u a') 
                          (That u b)
        (Pihat a' b)   -> Pihat@Ubb 
                          (That u a') 
                          (\(x:: Sbb (That u a')) -> That u (b x) )
        (Sigmahat a' b)-> Sigmahat@Ubb 
                          (That u a') 
                          (\(x:: Sbb (That u a')) -> That u (b x) )
        (What a' b) ->    What@Ubb 
                          (That u a') 
                          (\(x:: Sbb (That u a')) -> That u (b x) )
        (a0hat)        -> a0lift u
        (a1hat c)      -> a1lift u c
        (fhat a'  b)   -> flift u a' b
        (ghat a'  b c) -> glift u a' b c
        (suhat a0 a1 f g i) 
                       -> univ@Ubb (su1@Univ u a0 a1 f g i)
        (tuhat a0 a1 f g i a) 
                       -> That (SU1hat u a0 a1 f g i) a

        
  T    (u:: Univ)
       (a:: U u) 
       :: Set
       = Sbb (That u a)


  M    :: Set = data 
                 sup (f :: (b :: Ubb)->
                           (c :: (Sbb b)-> Ubb)-> Ubb)
                     (g :: (b :: Ubb)->
                           (c :: (Sbb b)-> Ubb)-> 
                           (d :: Sbb (f b c))-> M) 


  tauhat(m :: M)
        (a :: Ubb)
        (b :: (Sbb a)-> Ubb)
        :: Ubb  = case m of 
                      (sup f g) ->  f a  b

  tau   (m :: M)
        (a :: Ubb)
        (b :: (Sbb a)-> Ubb)
        :: Set  = Sbb (tauhat m a b)
                

  subm  (m :: M)
        (a :: Ubb)
        (b :: (Sbb a)-> Ubb)
        (i :: tau m a b)
        :: M   = case m of 
                     (sup f g) ->  g a b i 
 

  m  (u :: Univ)
     :: M     = case u of 
                    (su0 a0 a1 f g n) 
                        ->  n
                    (su1 u' a0 a1 f g i) 
                        ->  subm 
                            (m u' ) 
                            (That u' a0) 
                            (\(x:: T u' a0)-> That u' (a1 x))
                            i                                 

  


  SU1hat (  u :: Univ)
         ( a0 :: U u)
         ( a1 :: Sbb (That u a0) -> U u) 
         ( f  :: (a :: U u) -> (Sbb (That u a) -> U u) -> U u) 
         ( g  :: (a ::  U u)-> (b:: Sbb (That u a) -> U u)
                  -> (c:: Sbb (That u (f a b)))-> U u) 
          (i  :: tau
                 (m u) 
                 (That u a0) 
                 (\(x:: Sbb (That u a0))-> That u (a1 x)))
        :: Univ
     = su1@Univ  u a0 a1 f g i

  a0lift ( u :: Univ)
        :: Ubb
        = case u of 
         (su0 a0 a1 f g n) -> a0
         (su1 u' a0 a1 f g i) ->  That u' a0
           

  a1lift ( u :: Univ)
         ( a :: Sbb (a0lift u))
         :: Ubb
        = case u of 
         (su0 a0 a1 f g n) -> a1 a
         (su1 u' a0 a1 f g i) ->  That u' (a1 a)
           


  flift ( u :: Univ)
        ( a :: U u)
        ( b :: Sbb (That u a) -> U u)
        :: Ubb
        = case u of 
         (su0 a0 a1 f g n) ->
           f (That u a) 
              ((\(x:: T u a) -> That u (b x)))
         (su1 u' a0 a1 f g i) ->  
           That u' 
           (f 
            (tuhat@(U u') a0 a1 f g i a)  
            (((\(x:: T u a)-> (tuhat@(U u') a0 a1 f g i (b x))))))



  glift ( u :: Univ)
        ( a :: U u)
        ( b :: Sbb (That u a) -> U u)
        ( c :: Sbb (flift u a b))
        :: Ubb
        = case u of 
              (su0 a0 a1 f g n) ->  
                g 
                (That u a) 
                ((\(x:: T u a) -> That u (b x)))
                c
              (su1 u' a0 a1 f g i) ->  
                That u' 
                (g 
                 (tuhat@(U u') a0 a1 f g i a)  
                 (((\(x:: T u a)-> (tuhat@(U u') a0 a1 f g i (b x)))))
                 c)