{-- Mahlo universe --}

fam(X : Type) 
  = data{ $fam (dom:Set, el : (a : dom) -> X) }
  : Type, 

fun( X : Set, Y : Set)
  = ( x : X )->Y
  : Set,

pred( X : Set)
  = ( x : X )->Set
  : Type,

dom_ofx( X : Type, f : fam X) 
  = case f of{ $fam dom el -> dom}
  : Set,

dom_of 
  = dom_ofx Set
  : ( f : fam Set) -> Set,

mem_of( f : fam Set)
  = case f of{ $fam dom el -> el }
  : pred (dom_of f),

{-- the set of internal subfamilies of a family of sets --}

ifam( f : fam Set) 
  = data{ $ifam( d : dom_of f, e : fun (mem_of f d) (dom_of f)) }
  : Set, 

ifam_ofx( X : Set, f : fam Set) 
  = data{ $ifam( d : dom_of f, el : fun (mem_of f d) X) }
  : Set, 

idom_of( AB : fam Set, a : ifam AB) 
  = case a of{ $ifam d el -> d }
  :  dom_of AB, 

imem_of( AB : fam Set, a : ifam AB) 
  = case a of{ $ifam d el -> el}
  : fun (mem_of AB (idom_of AB a)) (dom_of AB),

int_ops( AB : fam Set, f : fun (ifam AB) (ifam AB))
  = theory{
  A = dom_of AB
    : Set,

  B = mem_of AB
    : pred A,

  Q( a : A, b : fun (B a) A) 
    = idom_of AB (f ($ifam a b))
    : A, 

  QQ( a : A, b : fun (B a) A) 
    = imem_of AB (f ($ifam a b)) 
    : fun (B (Q a b)) A
  }
  : Theory, 

{-
One way to define a mahlo universe.
-}

Mahlo 
  = let{ M (U : Set, T : pred U)
          = data{ $0 ,
                  $1 ,
                  $S( a : U) ,
                  $plus( a : U, b : U) ,
                  $sig( a : U, b : fun (T a) U) ,
                  $pi( a : U, b : fun (T a) U) , 
                     {- (p : ifam ($fam U T))  -}
                  $n ,
                  $w( a : U, b : fun (T a) U) ,
                  $m( q  : (a : U) -> fun (fun (T a) U) U,
                       qq : (a : U, b : fun (T a) U) -> fun (T (q a b)) U) }
           : Set }
    in  let{ N (U : Set, T : pred U)
              = \ x -> 
                case x of{
                  $0   -> data{} ,
                  $1   -> data{ $zero } ,
                  $S a -> data{ $zero , $succ( p : T a) },
                  $plus a b -> 
                    data{ $inl( a : T a) , $inr( b : T b) },
                  $sig a b -> 
                    data{ $pr( fst : T a, snd : T (b fst)) },
                  $pi a b -> 
                    data{ $lambda ( f : ( x : T a) -> T (b x) ) },
                  $n ->
                    let{ x = data{ $zero , $succ( p : x) } : Set }
                    in  x,
                  $w a b ->
                    let{ w = data{ $sup( d : T a, b : fun (T (b d)) w) } : Set  }
                    in  w,
                  $m q qq ->
                    let{ f( x : Set, y : fun x U) 
                          = data{ $q(  a : x, b : fun (T (y a)) x),
                                    {- p : ifam ($fam x (\z->T(y z))) -}
                                  $qq( a : x, b : fun (T (y a)) x,
                                       c : T (q (y a) (\x -> y (b x)))) }
                          : Set }
                    in  let{ g( x : Set, y : fun x U)
                              = \ i -> case i of{
                                  $q a b    -> q (y a) (\x -> y (b x)),
                                  $qq a b c -> qq (y a) (\x -> y (b x)) c}
                              : fun (f x y) U }
                        in  let{ xy = case xy of{ $fam x y -> $fam (f x y) (g x y)}
                                    : fam U }
                            in  dom_ofx U xy }
             : pred (M U T) }
        in  let{ x = case x of{ $fam dom el -> $fam (M dom el) (N dom el)}
                  : fam Set }
            in  x
  : fam Set