--#include "MBSet.alfa" open Datoids use eqBool, DBool Sig :: Type = data nil | nonrec (D::Datoid) (fi'::D.Elem -> Sig) | rec (fi'::Sig) F (fi::Sig)(X::Set) :: Set = case fi of { (nil) -> Unit; (nonrec D fi') -> Sigma D.Elem (\(h::D.Elem) -> F (fi' h) X); (rec fi') -> And X (F fi' X);} F1 (fi::Sig)(a::Set)(b::Set)(f::a -> b)(x::F fi a) :: F fi b = case fi of { (nil) -> case x of { (tt) -> tt@_;}; (nonrec D fi') -> case x of { (si a' b') -> si@_ a' (F1 (fi' a') a b f b');}; (rec fi') -> case x of { (Pair a' b') -> Pair@_ (f a') (F1 fi' a b f b');};} T (fi::Sig) :: Set = data Intro (im::F fi (T fi)) out (fi::Sig)(i::T fi) :: F fi (T fi) = case i of { (Intro im) -> im;} It (fi::Sig)(C::Set)(d::F fi C -> C) :: T fi -> C = \(h::T fi) -> d (F1 fi (T fi) C (It fi C d) (out fi h)) FIH (fi::Sig)(Y::Set)(C::Y -> Set)(x::F fi Y) :: Set = case fi of { (nil) -> Unit; (nonrec D fi') -> case x of { (si d z) -> FIH (fi' d) Y C z;}; (rec fi') -> case x of { (Pair y z) -> And (C y) (FIH fi' Y C z);};} FIH1 (fi::Sig)(Y::Set)(C::Y -> Set)(r::(y::Y) -> C y)(x::F fi Y) :: FIH fi Y C x = case fi of { (nil) -> case x of { (tt) -> tt@_;}; (nonrec D fi') -> case x of { (si a b) -> FIH1 (fi' a) Y C r b;}; (rec fi') -> case x of { (Pair a b) -> Pair@_ (r a) (FIH1 fi' Y C r b);};} R (fi::Sig) (C::T fi -> Set) (d::(y::F fi (T fi)) -> FIH fi (T fi) C y -> C (Intro@_ y)) (x::T fi) :: C x = case x of { (Intro im) -> d im (FIH1 fi (T fi) C (R fi C d) im);} MIt (fi::Sig)(G::Set)(s::(X::Set) -> (X -> G) -> F fi X -> G)(x::T fi) :: G = case x of { (Intro im) -> s (T fi) (MIt fi G s) im;} d_count (fi::Sig)(im::F fi Nat) :: Nat = case fi of { (nil) -> one; (nonrec D fi') -> case im of { (si a b) -> d_count (fi' a) b;}; (rec fi') -> case im of { (Pair a b) -> a + (d_count fi' b);};} count (fi::Sig)(i::T fi) :: Nat = It fi Nat (d_count fi) i d_eq (X::Set)(ext::rel X)(fi::Sig)(a::F fi X)(b::F fi X) :: Bool = case fi of { (nil) -> true@_; (nonrec D fi') -> case a of { (si a0 af) -> case b of { (si b0 bf) -> let af' (h::True (D.eq a0 b0)) :: F (fi' b0) X = D.subst (\(c0::D.Elem) -> F (fi' c0) X) a0 b0 h af Foo (b::Bool)(h::True (eqBool b (D.eq a0 b0))) :: Bool = case b of { (false) -> false@_; (true) -> d_eq X ext (fi' b0) (af' (DBool.subst True true@_ (D.eq a0 b0) h tt@_)) bf;} in Foo (D.eq a0 b0) (DBool.ref (D.eq a0 b0));};}; (rec fi') -> case a of { (Pair a' b') -> case b of { (Pair a0 b0) -> and (ext a' a0) (d_eq X ext fi' b' b0);};};} utest (X::Set)(ext::rel X) :: (fi::Sig) -> rel (F fi X) = let rec (fi::Sig)(a::F fi X)(b::F fi X) :: Bool = case fi of { (nil) -> true@_; (nonrec D fi') -> case a of { (si a0 a1) -> case b of { (si b0 b1) -> let Branch (d::D.Elem) :: Set = F (fi' d) X caseOn (e::Bool)(a1'::True e -> Branch b0) :: Bool = case e of { (true) -> rec (fi' b0) (a1' tt@_) b1; (false) -> false@_;} e0 = D.eq a0 b0 in caseOn e0 (\(h::True e0) -> D.subst Branch a0 b0 h a1);};}; (rec fi') -> case a of { (Pair a0 a1) -> case b of { (Pair b0 b1) -> and (ext a0 b0) (rec fi' a1 b1);};};} in rec sigmaCond (D::Datoid) (P::D.Elem -> Set) (C::Set) (a::D.Elem) (b::D.Elem) (ifTrue::P b -> P b -> C) (ifFalse::C) (pa::P a) (pb::P b) :: C = let caseOn (e::Bool)(cast::True e -> P a -> P b) :: C = case e of { (false) -> ifFalse; (true) -> ifTrue (cast tt@_ pa) pb;} in caseOn (D.eq a b) (D.subst P a b) utest3 (X::Set)(ext::rel X)(fi::Sig)(a::F fi X)(b::F fi X) :: Bool = case fi of { (nil) -> true@_; (nonrec D fi') -> case a of { (si a0 a1) -> case b of { (si b0 b1) -> {-#h#-}sigmaCond D (\(h::D.Elem) -> F (fi' h) X) Bool a0 b0 (utest3 X ext (fi' b0)) false@_ a1 b1;};}; (rec fi') -> case a of { (Pair a0 a1) -> case b of { (Pair b0 b1) -> and (ext a0 b0) (utest3 X ext fi' a1 b1);};};} utest2 (X::Set)(ext::rel X)(fi::Sig)(a::F fi X)(b::F fi X) :: Bool = case fi of { (nil) -> true@_; (nonrec D fi') -> case a of { (si a0 a1) -> case b of { (si b0 b1) -> let Branch (d::D.Elem) :: Set = F (fi' d) X -- If a0 and b0 are equal, the respective branches are isomorphic. transfer (t::True (D.eq a0 b0))(x::Branch a0) :: Branch b0 = D.subst Branch a0 b0 t x caseOn (e::Bool)(cast::True e -> Branch a0 -> Branch b0) :: Bool = case e of { (true) -> utest2 X ext (fi' b0) (cast tt@_ a1) b1; (false) -> false@_;} in caseOn (D.eq a0 b0) transfer;};}; (rec fi') -> case a of { (Pair a0 a1) -> case b of { (Pair b0 b1) -> and (ext a0 b0) (utest2 X ext fi' a1 b1);};};} It2 (fi::Sig) (C::Set) (d::(X::Set) -> (X -> X -> C) -> (fi1::Sig) -> F fi1 X -> F fi1 X -> C) :: T fi -> T fi -> C = \(h::T fi) -> \(h'::T fi) -> d (T fi) (It2 fi C d) fi (out fi h) (out fi h') {-# Alfa unfoldgoals off brief on hidetypeannots off wide nd hiding on var "Unit" as "()" con "tt" as "*" var "Sigma" quantifier domain on as "S" with symbolfont var "fi" as "F" with symbolfont var "fi'" as "F1" with symbolfont var "And" infix rightassoc as "´" with symbolfont con "AndI" tuple con "Pair" tuple con "si" tuple var "fi2" as "F2" with symbolfont var "fi1" as "F1" with symbolfont #-}