--#include "MBSet.alfa" Sig :: Type = data nil | nonrec (D::Datoid) (fi'::D.Elem -> Sig) | rec (fi'::Sig) Im (fi::Sig)(X::Set) :: Set = case fi of { (nil) -> Unit; (nonrec D fi') -> Sigma D.Elem (\(h::D.Elem) -> Im (fi' h) X); (rec fi') -> And X (Im fi' X);} Im1 (fi::Sig)(a::Set)(b::Set)(f::a -> b)(x::Im fi a) :: Im fi b = case fi of { (nil) -> case x of { (tt) -> tt@_;}; (nonrec D fi') -> case x of { (si a' b') -> si@_ a' (Im1 (fi' a') a b f b');}; (rec fi') -> case x of { (Pair a' b') -> Pair@_ (f a') (Im1 fi' a b f b');};} T (fi::Sig) :: Set = data Intro (im::Im fi (T fi)) out (fi::Sig)(i::T fi) :: Im fi (T fi) = case i of { (Intro im) -> im;} It (fi::Sig)(C::Set)(d::Im fi C -> C) :: T fi -> C = \(h::T fi) -> d (Im1 fi (T fi) C (It fi C d) (out fi h)) MIt (fi::Sig) (G::Set) (s::(X::Set) -> (X -> G) -> Im 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::Im 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 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) topeq (X::Set)(ext::rel X)(fi::Sig)(a::Im fi X)(b::Im 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) -> Im (fi' h) X) Bool a0 b0 (topeq 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) (topeq X ext fi' a1 b1);};};} eqKnot (fi::Sig)(a::T fi)(b::T fi) :: Bool = topeq (T fi) (eqKnot fi) fi (out fi a) (out fi b) It2 (fi::Sig) (C::Set) (d::(X::Set) -> (X -> X -> C) -> (fi1::Sig) -> Im fi1 X -> Im 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') eqIt2 (fi::Sig) :: rel (T fi) = It2 fi Bool topeq sigmaCond2 (D::Datoid) (P::D.Elem -> Set -> Set) (C::Set) (Y::Set) (a::D.Elem) (b::D.Elem) (ifTrue::P b (Y -> C) -> P b Y -> C) (ifFalse::C) (pa::P a (Y -> C)) (pb::P b Y) :: C = let caseOn (e::Bool)(cast::True e -> P a (Y -> C) -> P b (Y -> C)) :: C = case e of { (false) -> ifFalse; (true) -> ifTrue (cast tt@_ pa) pb;} in caseOn (D.eq a b) (D.subst (\(h::D.Elem) -> P h ((h'::Y) -> C)) a b) topeq' (fi::Sig)(Y::Set)(x::Im fi (Y -> Bool)) :: Im fi Y -> Bool = case fi of { (nil) -> case x of { (tt) -> \(y::Im nil@_ Y) -> case y of { (tt) -> true@_;};}; (nonrec D fi') -> case x of { (si x0 x1) -> \(y::Im (nonrec@_ D fi') Y) -> case y of { (si y0 y1) -> sigmaCond2 D (\(h::D.Elem) -> Im (fi' h)) Bool Y x0 y0 (topeq' (fi' y0) Y) false@_ x1 y1;};}; (rec fi') -> case x of { (Pair x0 x1) -> \(y::Im (rec@_ fi') Y) -> case y of { (Pair y0 y1) -> and (x0 y0) (topeq' fi' Y x1 y1);};};} topeq2 (fi::Sig)(x::Im fi (T fi -> Bool)) :: T fi -> Bool = \(y::T fi) -> case y of { (Intro y') -> topeq' fi (T fi) x y';} eqIt (fi::Sig) :: rel (T fi) = It fi ((h::T fi) -> Bool) (topeq2 fi) Md_eq (fi::Sig) (X::Set) (Y::Set) (eq::X -> Y -> Bool) (x::Im fi X) (y::Im fi Y) :: Bool = case fi of { (nil) -> case x of { (tt) -> case y of { (tt) -> true@_;};}; (nonrec D fi') -> case x of { (si x0 x1) -> case y of { (si y0 y1) -> sigmaCond2 D ? Bool Y x0 y0 eq false@_ x1 y1;};}; (rec fi') -> case x of { (Pair a b) -> case y of { (Pair a' b') -> and (eq a a') (Md_eq fi' X Y eq b b');};};} Md_eq2 (fi::Sig)(X::Set)(eq::X -> T fi -> Bool)(x::Im fi X)(y::T fi) :: Bool = case y of { (Intro im) -> Md_eq fi X (T fi) eq x im;} M_eq (fi::Sig)(x::T fi) :: T fi -> Bool = MIt fi ((y::T fi) -> Bool) (Md_eq2 fi) x {-# Alfa unfoldgoals off brief on hidetypeannots off wide typesignatures 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 #-}