{- By Anton Setzer, June '99 -}
N :: Set = data zero | S (n :: N)
Pi (A :: Set) (B :: A -> Set) :: Set
= (a :: A) -> B a
package mahlo =
mutual
U :: Set
= data Nhat
| Pihat (a :: U)
(b :: T a -> U)
| su (f :: (a :: U)-> (T a -> U) -> U)
(g :: (a :: U)-> (b :: T a -> U) -> T (f a b) -> U)
T (u:: U)
:: Set
= case u of
(Nhat) -> N
(Pihat a b) -> Pi (T a ) (\(x :: T a)-> T (b x))
(su f g) -> SU f g
SU (f :: (a :: U)-> (T a -> U) -> U)
(g :: (a :: U)-> (b :: T a -> U)-> T (f a b) -> U)
:: Set
= data Nhat
| fhat (a :: SU f g)
(b :: T (TU f g a) -> SU f g)
| ghat (a :: SU f g)
(b :: T (TU f g a) -> SU f g)
(c :: T (f (TU f g a)
(\(x :: T (TU f g a))-> TU f g (b x))))
TU (f :: (a :: U)-> (T a -> U) -> U)
(g :: (a :: U)-> (b :: T a -> U)-> T (f a b) -> U)
(u :: SU f g)
:: U
= case u of
(Nhat) -> Nhat@U
(fhat a b) -> f (TU f g a)
(\(x :: T (TU f g a))-> TU f g (b x))
(ghat a b c) -> g (TU f g a)
(\(x :: T (TU f g a))-> TU f g (b x))
c