--#include "MBSet.alfa" open Datoids use eqNat OP (I::Set) :: Type = data nil | nonrec (A::Set) (phi::A -> OP I) | rec (i::I) (phi::OP I) Fam (I::Set) :: Type = I -> OP I F (I::Set)(im::I -> Set)(fi::OP I) :: Set = case fi of { (nil) -> Unit; (nonrec A f) -> Sigma A (\(a::A) -> F I im (f a)); (rec i phi) -> And (im i) (F I im phi);} F0 (I::Set)(fam::Fam I)(im::I -> Set)(i::I) :: Set = F I im (fam i) -- imX and imY could be hidden F1 (I::Set) (imX::I -> Set) (imY::I -> Set) (fi::OP I) (f::(i::I) -> imX i -> imY i) (x::F I imX fi) :: F I imY fi = case fi of { (nil) -> case x of { (tt) -> tt@_;}; (nonrec A g) -> case x of { (si a b) -> si@_ a (F1 I imX imY (g a) f b);}; (rec i phi) -> case x of { (Pair a b) -> Pair@_ (f i a) (F1 I imX imY phi f b);};} T (I::Set)(fam::Fam I) :: I -> Set = \(i::I) -> data Intro (im::F0 I fam (T I fam) i) out (I::Set)(fam::Fam I)(i::I)(x::T I fam i) :: F0 I fam (T I fam) i = case x of { (Intro im) -> im;} It (I::Set) (fam::Fam I) (C::I -> Set) (d::(i::I) -> F I C (fam i) -> C i) :: (i::I) -> T I fam i -> C i = \(i::I) -> \(h::T I fam i) -> d i (F1 I (T I fam) C (fam i) (It I fam C d) (out I fam i h)) refENat (n::Nat) :: True (eqNat n n) = case n of { (zer) -> tt@_; (suc n') -> refENat n';} d_size (I::Set)(phi::OP I)(i::I)(im::F I (\(h::I) -> Nat) phi) :: Nat = case phi of { (nil) -> one; (nonrec A phi') -> case im of { (si a b) -> d_size I (phi' a) i b;}; (rec i phi') -> case im of { (Pair a b) -> a + (d_size I phi' i b);};} dsize (I::Set)(fam::Fam I) :: (i::I) -> (im::F I (\(h::I) -> Nat) (fam i)) -> Nat = \(i::I) -> d_size I (fam i) i size (I::Set)(fam::Fam I)(i::I)(x::T I fam i) :: Nat = It I fam (\(h::I) -> Nat) (dsize I fam) i x {-# Alfa unfoldgoals off brief on hidetypeannots off wide typesignatures nd hiding on var "F" hide 1 var "out" hide 2 var "size" hide 3 var "F0" hide 1 var "F1" hide 1 var "T" hide 1 var "It" hide 1 var "d_size" hide 1 var "dsize" hide 1 #-}