-- {\Huge \bf Formal proof of minimality of generated covers} -- Checked on Alfa/Agda version 2001-07-01 (HBC) -- file: regular66.agda -- {\Large \bf Basic Type Theory} -- -- Fam (A::Set) :: Type = A -> Set -- {\em Syntactic sugar for the $\Pi$-construction} Pi (A::Set)(B::Fam A) :: Set = (x::A) -> B x ForAll (A::Set)(B::Fam A) :: Set = (x::A) -> B x -- {\em Syntactic sugar relating to the $\Sigma$-construction} Sigma (A::Set)(B::Fam A) :: Set = sig {_1 :: A; _2 :: B _1;} Exists (A::Set)(B::Fam A) :: Set = sig {_1 :: A; _2 :: B _1;} pair (A::Set)(B::Fam A)(a::A)(b::B a) :: Sigma A B = struct { _1 = a; _2 = b;} split (A::Set) (B::Fam A) (C::Fam (Sigma A B)) (c::Sigma A B) (d::(x::A) -> (y::B x) -> C (pair A B x y)) :: C c = d c._1 c._2 Cart (A::Set)(B::Set) :: Set = sig {_1 :: A; _2 :: B;} proj1 (A::Set)(B::Set)(c::Cart A B) :: A = c._1 proj2 (A::Set)(B::Set)(c::Cart A B) :: B = c._2 and (A::Set)(B::Set) :: Set = Cart A B -- {\em Disjoint binary sums} Sum (A::Set)(B::Set) :: Set = data inl (x::A) | inr (y::B) when (A::Set) (B::Set) (C::Fam (Sum A B)) (c::Sum A B) (d::(x::A) -> C (inl@_ x)) (e::(y::B) -> C (inr@_ y)) :: C c = case c of { (inl x) -> d x; (inr y) -> e y;} -- {\em If and only if} iff (A::Set)(B::Set) :: Set = Cart (A -> B) (B -> A) -- {\em The empty set} empty :: Set = data elempty (A::Set)(x::empty) :: A = case x of { } -- {\em Natural numbers} Nat :: Set = data zero | succ (x::Nat) rec (C::(z::Nat) -> Set) (t::Nat) (f::C zero@_) (g::(x::Nat) -> (y::C x) -> C (succ@_ x)) :: C t = case t of { (zero) -> f; (succ x) -> g x (rec C x f g);} -- {\em A basic dependent type} L (z::Nat) :: Set = case z of { (zero) -> empty; (succ x) -> Nat;} -- {\em Deriving first projection from split} pr1 (A::Set)(B::Fam A)(c::Sigma A B) :: A = split A B (\(h::Sigma A B) -> A) c (\(x::A) -> \(y::B x) -> x) pr2 (A::Set)(B::Fam A)(c::Sigma A B) :: B (pr1 A B c) = split A B (\(h::Sigma A B) -> B (pr1 A B h)) c (\(x::A) -> \(y::B x) -> y) -- {\em The type of families of sets} Fams :: Type = sig {ind :: Set; fam :: Fam ind;} -- {\em The type of equivalence relations on $X$:} EQ (X::Set) :: Type = sig {eq :: X -> X -> Set; ref :: (x::X) -> eq x x; sym :: (x::X) -> (y::X) -> eq x y -> eq y x; tra :: (x::X) -> (y::X) -> (z::X) -> eq x y -> eq y z -> eq x z;} -- {\em The power set of $X$, as full as it gets here.} P (X::Set) :: Type = Fam X -- Extensional version of power set w.r.t. $X$ and an equivalence -- relation E. Note that equality of subsets $S$ and $T$ is then -- $Sx$ iff $Tx$ Pe (X::Set)(E::EQ X) :: Type = sig {sub :: P X; ext :: (x::X) -> (y::X) -> sub x -> E.eq x y -> sub y;} -- {\em Extensional membership} MemberE (X::Set)(E::EQ X)(a::X)(S::Pe X E) :: Set = S.sub a EqualE (X::Set)(E::EQ X)(S::Pe X E)(T::Pe X E) :: Set = ForAll X (\(h::X) -> iff (MemberE X E h S) (MemberE X E h T)) SubsetsE (X::Set)(E::EQ X)(S::Pe X E)(T::Pe X E) :: Set = ForAll X (\(h::X) -> MemberE X E h S -> MemberE X E h T) refEE (X::Set)(E::EQ X)(S::Pe X E) :: EqualE X E S S = \(x::X) -> struct { _1 = \(h::MemberE X E x S) -> h; _2 = \(h::MemberE X E x S) -> h;} transEE (X::Set) (E::EQ X) (S::Pe X E) (T::Pe X E) (U::Pe X E) (p::EqualE X E S T) (q::EqualE X E T U) :: EqualE X E S U = \(x::X) -> let mutual p1 :: iff (MemberE X E x S) (MemberE X E x T) = p x q1 :: iff (MemberE X E x T) (MemberE X E x U) = q x in let mutual p11 :: (x'::MemberE X E x S) -> MemberE X E x T = proj1 ((x'::MemberE X E x S) -> MemberE X E x T) ((x'::MemberE X E x T) -> MemberE X E x S) p1 p12 :: (x'::MemberE X E x T) -> MemberE X E x S = proj2 ((x'::MemberE X E x S) -> MemberE X E x T) ((x'::MemberE X E x T) -> MemberE X E x S) p1 q11 :: (x'::MemberE X E x T) -> MemberE X E x U = proj1 ((x'::MemberE X E x T) -> MemberE X E x U) ((x'::MemberE X E x U) -> MemberE X E x T) q1 q12 :: (x'::MemberE X E x U) -> MemberE X E x T = proj2 ((x'::MemberE X E x T) -> MemberE X E x U) ((x'::MemberE X E x U) -> MemberE X E x T) q1 in struct { _1 = \(h::MemberE X E x S) -> q11 (p11 h); _2 = \(h::MemberE X E x U) -> p12 (q12 h);} Subsetlemma1E (X::Set)(E::EQ X)(S::Pe X E)(T::Pe X E)(p::EqualE X E S T) :: SubsetsE X E S T = \(x::X) -> \(h::MemberE X E x S) -> let temp :: (x'::MemberE X E x S) -> MemberE X E x T = proj1 ((x'::MemberE X E x S) -> MemberE X E x T) ((x'::MemberE X E x T) -> MemberE X E x S) (p x) in temp h IntersectE (X::Set)(E::EQ X)(S::Pe X E)(T::Pe X E) :: Pe X E = struct { sub = \(h::X) -> Cart (MemberE X E h S) (MemberE X E h T); ext = \(x::X) -> \(y::X) -> \(h::sub x) -> \(h'::E.eq x y) -> struct { _1 = S.ext x y h._1 h'; _2 = T.ext x y h._2 h';};} singletonE (X::Set)(E::EQ X)(x::X) :: Pe X E = struct { sub = \(h::X) -> E.eq h x; ext = \(x'::X) -> \(y::X) -> \(h::sub x') -> \(h'::E.eq x' y) -> E.tra y x' x (E.sym x' y h') h;} singext (X::Set)(E::EQ X)(x::X)(y::X)(p::E.eq x y) :: EqualE X E (singletonE X E x) (singletonE X E y) = \(x'::X) -> struct { _1 = \(h::MemberE X E x' (singletonE X E x)) -> E.tra x' x y h p; _2 = \(h::MemberE X E x' (singletonE X E y)) -> E.sym x x' (E.tra x y x' p (E.sym x' y h));} -- {\em Type of equivalence relations on $X$ with truth-values in $F$} EQS (F::Fams)(X::Set) :: Type = sig {eq :: X -> X -> F.ind; ref :: (x::X) -> F.fam (eq x x); sym :: (x::X) -> (y::X) -> F.fam (eq x y) -> F.fam (eq y x); tra :: (x::X) -> (y::X) -> (z::X) -> F.fam (eq x y) -> F.fam (eq y z) -> F.fam (eq x z);} makebigE (F::Fams)(X::Set)(r::EQS F X) :: EQ X = struct { eq = \(h::X) -> \(h'::X) -> F.fam (r.eq h h'); ref = r.ref; sym = r.sym; tra = r.tra;} Rw (F::Fams)(X::Set) :: Set = Pi X (\(h::X) -> F.ind) Re (F::Fams)(X::Set)(E::EQS F X) :: Set = sig {sub :: Rw F X; ext :: ForAll X (\(h::X) -> ForAll X (\(h'::X) -> F.fam (sub h) -> F.fam (E.eq h h') -> F.fam (sub h')));} MemberSE (F::Fams)(X::Set)(E::EQS F X)(a::X)(S::Re F X E) :: Set = F.fam (S.sub a) EqualsetsSE (F::Fams)(X::Set)(E::EQS F X)(S::Re F X E)(T::Re F X E) :: Set = ForAll X (\(h::X) -> iff (MemberSE F X E h S) (MemberSE F X E h T)) reflSE (F::Fams)(X::Set)(E::EQS F X)(S::Re F X E) :: EqualsetsSE F X E S S = \(x::X) -> struct { _1 = \(h::MemberSE F X E x S) -> h; _2 = \(h::MemberSE F X E x S) -> h;} SubsetSE (F::Fams)(X::Set)(E::EQS F X)(S::Re F X E)(T::Re F X E) :: Set = ForAll X (\(h::X) -> MemberSE F X E h S -> MemberSE F X E h T) big (F::Fams)(X::Set)(E::EQS F X)(S::Re F X E) :: Pe X (makebigE F X E) = struct { sub = \(h::X) -> F.fam (S.sub h); ext = \(x::X) -> \(y::X) -> \(h::sub x) -> \(h'::(makebigE F X E).eq x y) -> S.ext x y h h';} -- Build a regular universe above A, B. -- sigma codes the Sigma -- epsilon embeds the family -- Can (F::Fams) :: Fams = let mutual U :: Set = data cross (a::U) (b::U) | sigma (a::U) (b::(x::T a) -> U) | emb (a::F.ind) T :: (a::U) -> Set = \(a::U) -> case a of { (cross a' b) -> Cart (T a') (T b); (sigma a' b) -> Sigma (T a') (\(h::T a') -> T (b h)); (emb a') -> F.fam a';} in struct { ind = U; fam = T;} EqualSets (X::Set)(A::Fam X)(B::Fam X) :: Set = ForAll X (\(h::X) -> iff (A h) (B h)) -- Power-set of X relative to the universe U, and associated relations MakeSet (X::Set)(U::Fams)(S::Rw U X) :: Set = Sigma X (\(h::X) -> U.fam (S h)) UnionE (F::Fams) (X::Set) (E::EQS (Can F) X) (c::(Can F).ind) (f::(Can F).fam c -> Re (Can F) X E) :: Re (Can F) X E = struct { sub = \(x::X) -> sigma@_ c (\(x'::(Can F).fam c) -> (f x').sub x); ext = \(x::X) -> \(x'::X) -> \(h::(Can F).fam (sub x)) -> \(h'::(Can F).fam (E.eq x x')) -> split ((Can F).fam c) (\(h0::(Can F).fam c) -> (Can F).fam ((f h0).sub x)) (\(h0::Sigma ((Can F).fam c) (\(h0::(Can F).fam c) -> (Can F).fam ((f h0).sub x))) -> (Can F).fam (sub x')) h (\(x0::(Can F).fam c) -> \(y::(Can F).fam ((f x0).sub x)) -> struct { _1 = x0; _2 = let f2 :: Re (Can F) X E = f x0 in let f3 :: ForAll X (\(h0::X) -> ForAll X (\(h1::X) -> (x1::(Can F).fam ((f x0).sub h0)) -> (x2::(Can F).fam (E.eq h0 h1)) -> (Can F).fam ((f x0).sub h1))) = f2.ext in f3 x x' y h';});} ULem (F::Fams) (X::Set) (E::EQS (Can F) X) (c::(Can F).ind) (f::(Can F).fam c -> Re (Can F) X E) (x::(Can F).fam c) :: SubsetSE (Can F) X E (f x) (UnionE F X E c f) = \(x'::X) -> \(h::MemberSE (Can F) X E x' (f x)) -> struct { _1 = x; _2 = h;} -- a subclass relation between a regular subset and a subset Subclass (F::Fams)(X::Set)(E::EQS F X)(W::Re F X E)(V::Pe X (makebigE F X E)) :: Set = ForAll X (\(h::X) -> MemberSE F X E h W -> MemberE X (makebigE F X E) h V) SubclassEE (X::Set)(E::EQ X)(W::Pe X E)(V::Pe X E) :: Set = ForAll X (\(h::X) -> MemberE X E h W -> MemberE X E h V) ULem2 (F::Fams) (X::Set) (E::EQS (Can F) X) (c::(Can F).ind) (f::(Can F).fam c -> Re (Can F) X E) (V::Pe X (makebigE (Can F) X E)) (p::ForAll ((Can F).fam c) (\(h::(Can F).fam c) -> Subclass (Can F) X E (f h) V)) :: Subclass (Can F) X E (UnionE F X E c f) V = \(x::X) -> \(h::MemberSE (Can F) X E x (UnionE F X E c f)) -> p h._1 x h._2 -- The property that a small cover relation is monotone in the second argument Mono (F::Fams)(X::Set)(E::EQS F X)(R::(a::X) -> (b::Re F X E) -> Set) :: Set = ForAll X (\(x::X) -> ForAll (Re F X E) (\(S::Re F X E) -> ForAll (Re F X E) (\(S'::Re F X E) -> SubsetSE F X E S S' -> R x S -> R x S'))) -- Collection theorem for subsets CollThm (F::Fams) (c::(Can F).ind) (E::EQS (Can F) ((Can F).fam c)) (V'::Re (Can F) ((Can F).fam c) E) (V::Pe ((Can F).fam c) (makebigE (Can F) ((Can F).fam c) E)) (R::(a::(Can F).fam c) -> (b::Re (Can F) ((Can F).fam c) E) -> Set) (mono::Mono (Can F) ((Can F).fam c) E R) (unb::ForAll ((Can F).fam c) (\(x::(Can F).fam c) -> MemberSE (Can F) ((Can F).fam c) E x V' -> Sigma (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (R x W)))) :: Sigma (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (ForAll ((Can F).fam c) (\(h::(Can F).fam c) -> MemberSE (Can F) ((Can F).fam c) E h V' -> R h W))) = let J :: Fams = Can F in let C :: Set = J.fam c in let mutual k :: J.ind = sigma@_ c V'.sub K :: Set = J.fam k in let mutual F2 :: K -> Re J C E = \(h::K) -> pr1 (Re J C E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (R (pr1 ((Can F).fam c) (\(h'::(Can F).fam c) -> J.fam (V'.sub h')) h) W)) (unb (pr1 ((Can F).fam c) (\(h'::(Can F).fam c) -> J.fam (V'.sub h')) h) (pr2 (J.fam c) (\(h'::J.fam c) -> J.fam (V'.sub h')) h)) G :: Pi K (\(h::K) -> Cart (Subclass J C E (F2 h) V) (R (pr1 ((Can F).fam c) (\(h'::(Can F).fam c) -> J.fam (V'.sub h')) h) (F2 h))) = \(x::K) -> struct { _1 = proj1 (Subclass J C E (F2 x) V) (R (pr1 ((Can F).fam c) (\(h::(Can F).fam c) -> J.fam (V'.sub h)) x) (pr1 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (R (pr1 ((Can F).fam c) (\(h::(Can F).fam c) -> J.fam (V'.sub h)) x) W)) (unb (pr1 ((Can F).fam c) (\(h::(Can F).fam c) -> J.fam (V'.sub h)) x) (pr2 (J.fam c) (\(h::J.fam c) -> J.fam (V'.sub h)) x)))) (pr2 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (R (pr1 ((Can F).fam c) (\(h::(Can F).fam c) -> J.fam (V'.sub h)) x) W)) (unb (pr1 ((Can F).fam c) (\(h::(Can F).fam c) -> J.fam (V'.sub h)) x) (pr2 (J.fam c) (\(h::J.fam c) -> J.fam (V'.sub h)) x))); _2 = proj2 (Subclass (Can F) ((Can F).fam c) E (pr1 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (R (pr1 (J.fam c) (\(h'::J.fam c) -> J.fam (V'.sub h')) x) W)) (unb (pr1 (J.fam c) (\(h'::J.fam c) -> J.fam (V'.sub h')) x) (pr2 (J.fam c) (\(h'::J.fam c) -> J.fam (V'.sub h')) x))) V) (R (pr1 ((Can F).fam c) (\(h'::(Can F).fam c) -> J.fam (V'.sub h')) x) (F2 x)) (pr2 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (R (pr1 (J.fam c) (\(h'::J.fam c) -> J.fam (V'.sub h')) x) W)) (unb (pr1 (J.fam c) (\(h'::J.fam c) -> J.fam (V'.sub h')) x) (pr2 (J.fam c) (\(h'::J.fam c) -> J.fam (V'.sub h')) x)));} in struct { _1 = UnionE F C E k F2; _2 = struct { _1 = ULem2 F C E (sigma@_ c V'.sub) F2 V (\(x::(Can F).fam (sigma@_ c V'.sub)) -> proj1 (Subclass (Can F) ((Can F).fam c) E (F2 x) V) (R (pr1 ((Can F).fam c) (\(h'::(Can F).fam c) -> J.fam (V'.sub h')) x) (F2 x)) (G x)); _2 = \(x::(Can F).fam c) -> \(h::MemberSE (Can F) ((Can F).fam c) E x V') -> mono x (F2 (pair ((Can F).fam c) (\(h'::(Can F).fam c) -> J.fam (V'.sub h')) x h)) (UnionE F C E k F2) (ULem F C E (sigma@_ c V'.sub) F2 (pair ((Can F).fam c) (\(h'::(Can F).fam c) -> J.fam (V'.sub h')) x h)) (proj2 (Subclass J C E (F2 (pair ((Can F).fam c) (\(h'::(Can F).fam c) -> J.fam (V'.sub h')) x h)) V) (R x (F2 (pair ((Can F).fam c) (\(h'::(Can F).fam c) -> J.fam (V'.sub h')) x h))) (G (pair ((Can F).fam c) (\(h'::(Can F).fam c) -> J.fam (V'.sub h')) x h)));};} -- The type of cover relations CRe (X::Set)(E::EQ X) :: Type = sig {rel :: (x::X) -> (U::Pe X E) -> Set; ext :: (x::X) -> (x'::X) -> (U::Pe X E) -> (U'::Pe X E) -> E.eq x x' -> EqualE X E U U' -> rel x U -> rel x' U';} -- The type of small cover relations (covers are small) CRSE (F::Fams)(X::Set)(E::EQS F X) :: Type = sig {rel :: (x::X) -> (U::Re F X E) -> Set; ext :: (x::X) -> (x'::X) -> (U::Re F X E) -> (U'::Re F X E) -> F.fam (E.eq x x') -> EqualsetsSE F X E U U' -> rel x U -> rel x' U';} -- Construct the canonical extension of a small cover to a cover Extend (F::Fams)(X::Set)(E::EQS F X)(R::CRSE F X E) :: CRe X (makebigE F X E) = struct { rel = \(x::X) -> \(U::Pe X (makebigE F X E)) -> Sigma (Re F X E) (\(W::Re F X E) -> and (Subclass F X E W U) (R.rel x W)); ext = \(x::X) -> \(x'::X) -> \(U::Pe X (makebigE F X E)) -> \(U'::Pe X (makebigE F X E)) -> \(h::(makebigE F X E).eq x x') -> \(h'::EqualE X (makebigE F X E) U U') -> \(h0::rel x U) -> let mutual r1 :: Re F X E = pr1 (Re F X E) (\(W::Re F X E) -> and (Subclass F X E W U) (R.rel x W)) h0 r2 :: and (Subclass F X E (pr1 (Re F X E) (\(W::Re F X E) -> and (Subclass F X E W U) (R.rel x W)) h0) U) (R.rel x (pr1 (Re F X E) (\(W::Re F X E) -> and (Subclass F X E W U) (R.rel x W)) h0)) = pr2 (Re F X E) (\(W::Re F X E) -> and (Subclass F X E W U) (R.rel x W)) h0 in let incl :: SubsetsE X (makebigE F X E) U U' = Subsetlemma1E X (makebigE F X E) U U' h' in struct { _1 = r1; _2 = struct { _1 = \(x0::X) -> \(h1::MemberSE F X E x0 r1) -> incl x0 (r2._1 x0 h1); _2 = R.ext x x' h0._1 r1 h (\(x0::X) -> struct { _1 = \(h1::MemberSE F X E x0 h0._1) -> h1; _2 = \(h1::MemberSE F X E x0 r1) -> h1;}) r2._2;};};} -- The statements that a cover relation is reflexive and transitive ReflexiveE (X::Set)(E::EQ X)(R::CRe X E) :: Type = (U::Pe X E) -> (a::X) -> MemberE X E a U -> R.rel a U TransitiveE (X::Set)(E::EQ X)(R::CRe X E) :: Type = (U::Pe X E) -> (V::Pe X E) -> (x::X) -> R.rel x U -> ForAll X (\(y::X) -> U.sub y -> R.rel y V) -> R.rel x V TransitiveSE (F::Fams)(X::Set)(E::EQS F X)(R::CRSE F X E) :: Set = (U::Re F X E) -> (V::Re F X E) -> (x::X) -> R.rel x U -> ForAll X (\(y::X) -> F.fam (U.sub y) -> R.rel y V) -> R.rel x V -- The statement that a small cover relation is reflexive ReflexiveSE (F::Fams)(X::Set)(E::EQS F X)(R::CRSE F X E) :: Set = ForAll X (\(x::X) -> ForAll (Re F X E) (\(U::Re F X E) -> MemberSE F X E x U -> R.rel x U)) -- Monotonicity of cover relation in second argument MonoE (F::Fams)(X::Set)(E::EQS F X)(R::CRSE F X E) :: Type = (x::X) -> (S::Re F X E) -> (S'::Re F X E) -> SubsetSE F X E S S' -> R.rel x S -> R.rel x S' MonoLemma (F::Fams) (X::Set) (E::EQS F X) (R::CRSE F X E) (refl::ReflexiveSE F X E R) (trans::TransitiveSE F X E R) :: MonoE F X E R = \(x::X) -> \(S::Re F X E) -> \(S'::Re F X E) -> \(h::SubsetSE F X E S S') -> \(h'::R.rel x S) -> trans S S' x h' (\(x'::X) -> \(h0::F.fam (S.sub x')) -> refl x' S' (h x' h0)) TrThm2 (F::Fams) (c::(Can F).ind) (E::EQS (Can F) ((Can F).fam c)) (R::CRSE (Can F) ((Can F).fam c) E) (refl::ReflexiveSE (Can F) ((Can F).fam c) E R) :: TransitiveSE (Can F) ((Can F).fam c) E R -> TransitiveE ((Can F).fam c) (makebigE (Can F) ((Can F).fam c) E) (Extend (Can F) ((Can F).fam c) E R) = \(h::TransitiveSE (Can F) ((Can F).fam c) E R) -> \(U::Pe ((Can F).fam c) (makebigE (Can F) ((Can F).fam c) E)) -> \(V::Pe ((Can F).fam c) (makebigE (Can F) ((Can F).fam c) E)) -> \(x::(Can F).fam c) -> \(h'::(Extend (Can F) ((Can F).fam c) E R).rel x U) -> \(h0::ForAll ((Can F).fam c) (\(y::(Can F).fam c) -> (x'::U.sub y) -> (Extend (Can F) ((Can F).fam c) E R).rel y V)) -> let F' :: Fams = Can F in let X :: Set = F'.fam c in let mutual Ex (y::X)(W::Pe X (makebigE F' X E)) :: Set = (Extend F' X E R).rel y W Exs (W1::Re F' X E)(W2::Pe X (makebigE F' X E)) :: Set = ForAll X (\(y::X) -> MemberSE F' X E y W1 -> Ex y W2) Rs (W1::Re F' X E)(W2::Re F' X E) :: Set = ForAll X (\(y::X) -> MemberSE F' X E y W1 -> R.rel y W2) in let U' :: Re F' X E = pr1 (Re F' X E) (\(W::Re (Can F) ((Can F).fam c) E) -> and (Subclass (Can F) ((Can F).fam c) E W U) (R.rel x W)) h' in let lemma1 :: Subclass F' X E U' U = proj1 (Subclass F' X E U' U) (R.rel x (pr1 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> and (Subclass (Can F) ((Can F).fam c) E W U) (R.rel x W)) h')) (pr2 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> and (Subclass (Can F) ((Can F).fam c) E W U) (R.rel x W)) h') in let lemma2 :: Exs U' V = \(x'::X) -> \(h1::MemberSE F' X E x' U') -> h0 x' (lemma1 x' h1) in let lemma3 :: Sigma (Re F' X E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (ForAll ((Can F).fam c) (\(h1::X) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1 U') -> R.rel h1 W))) = CollThm F c E U' V (\(x'::(Can F).fam c) -> R.rel x') (MonoLemma F' X E R refl h) (\(x'::(Can F).fam c) -> \(h1::MemberSE (Can F) ((Can F).fam c) E x' U') -> h0 x' (lemma1 x' h1)) in let lemma4 :: Sigma (Re F' X E) (\(h1::Re (Can F) ((Can F).fam c) E) -> ForAll ((Can F).fam c) (\(h1'::X) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1' U') -> R.rel h1' (pr1 (Re (Can F) ((Can F).fam c) E) (\(W'::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W' V) (ForAll ((Can F).fam c) (\(h1''::(Can F).fam c) -> (x''::MemberSE (Can F) ((Can F).fam c) E h1'' U') -> R.rel h1'' W'))) lemma3))) = struct { _1 = pr1 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (ForAll ((Can F).fam c) (\(h1::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1 U') -> R.rel h1 W))) lemma3; _2 = proj2 (Subclass (Can F) ((Can F).fam c) E (pr1 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (ForAll ((Can F).fam c) (\(h1::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1 U') -> R.rel h1 W))) lemma3) V) (ForAll ((Can F).fam c) (\(h1::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1 U') -> R.rel h1 (pr1 (Re (Can F) ((Can F).fam c) E) (\(W'::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W' V) (ForAll ((Can F).fam c) (\(h1'::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1' U') -> R.rel h1' W'))) lemma3))) (pr2 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (ForAll ((Can F).fam c) (\(h1::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1 U') -> R.rel h1 W))) lemma3);} in struct { _1 = pr1 (Re (Can F) ((Can F).fam c) E) (\(h1::Re (Can F) ((Can F).fam c) E) -> ForAll ((Can F).fam c) (\(h1'::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1' U') -> R.rel h1' (pr1 (Re (Can F) ((Can F).fam c) E) (\(W'::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W' V) (ForAll ((Can F).fam c) (\(h1''::(Can F).fam c) -> (x''::MemberSE (Can F) ((Can F).fam c) E h1'' U') -> R.rel h1'' W'))) lemma3))) lemma4; _2 = struct { _1 = proj1 (Subclass (Can F) ((Can F).fam c) E (pr1 (Re (Can F) ((Can F).fam c) E) (\(h1::Re (Can F) ((Can F).fam c) E) -> ForAll ((Can F).fam c) (\(h1'::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1' U') -> R.rel h1' (pr1 (Re (Can F) ((Can F).fam c) E) (\(W'::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W' V) (ForAll ((Can F).fam c) (\(h1''::(Can F).fam c) -> (x''::MemberSE (Can F) ((Can F).fam c) E h1'' U') -> R.rel h1'' W'))) lemma3))) lemma4) V) (ForAll ((Can F).fam c) (\(h1::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1 U') -> R.rel h1 (pr1 (Re (Can F) ((Can F).fam c) E) (\(W'::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W' V) (ForAll ((Can F).fam c) (\(h1'::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1' U') -> R.rel h1' W'))) lemma3))) (pr2 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W V) (ForAll ((Can F).fam c) (\(h1::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1 U') -> R.rel h1 W))) lemma3); _2 = h U' (pr1 (Re (Can F) ((Can F).fam c) E) (\(h1::Re (Can F) ((Can F).fam c) E) -> ForAll ((Can F).fam c) (\(h1'::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1' U') -> R.rel h1' (pr1 (Re (Can F) ((Can F).fam c) E) (\(W'::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W' V) (ForAll ((Can F).fam c) (\(h1''::(Can F).fam c) -> (x''::MemberSE (Can F) ((Can F).fam c) E h1'' U') -> R.rel h1'' W'))) lemma3))) lemma4) x (proj2 (Subclass (Can F) ((Can F).fam c) E (pr1 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> and (Subclass (Can F) ((Can F).fam c) E W U) (R.rel x W)) h') U) (R.rel x U') (pr2 (Re (Can F) ((Can F).fam c) E) (\(W::Re (Can F) ((Can F).fam c) E) -> and (Subclass (Can F) ((Can F).fam c) E W U) (R.rel x W)) h')) (pr2 (Re (Can F) ((Can F).fam c) E) (\(h1::Re (Can F) ((Can F).fam c) E) -> ForAll ((Can F).fam c) (\(h1'::(Can F).fam c) -> (x'::MemberSE (Can F) ((Can F).fam c) E h1' U') -> R.rel h1' (pr1 (Re (Can F) ((Can F).fam c) E) (\(W'::Re (Can F) ((Can F).fam c) E) -> Cart (Subclass (Can F) ((Can F).fam c) E W' V) (ForAll ((Can F).fam c) (\(h1''::(Can F).fam c) -> (x''::MemberSE (Can F) ((Can F).fam c) E h1'' U') -> R.rel h1'' W'))) lemma3))) lemma4);};} -- The type of preorders: PreOrder (O::Set)(OE::EQ O) :: Type = sig {rel :: O -> O -> Set; refl :: (x::O) -> rel x x; tra :: (x::O) -> (y::O) -> (z::O) -> (p::rel x y) -> (q::rel y z) -> rel x z; ext :: (x::O) -> (y::O) -> (z::O) -> (u::O) -> (p::OE.eq x y) -> (q::OE.eq z u) -> (r::rel y z) -> rel x u;} -- The type of presentations: Pres (O::Set)(OE::EQ O) :: Type = sig {I :: Set; IE :: EQ I; g :: I -> O; extg :: (i::I) -> (j::I) -> IE.eq i j -> OE.eq (g i) (g j); G :: I -> Pe O OE; extG :: (i::I) -> (j::I) -> IE.eq i j -> EqualE O OE (G i) (G j); Pod :: PreOrder O OE; Pos :: Pe O OE;} -- extract relation part Po (O::Set)(OE::EQ O)(Ge::Pres O OE) :: (x::O) -> (y::O) -> Set = Ge.Pod.rel -- Elements below some element in $U$: SubGen (O::Set)(OE::EQ O)(Ge::Pres O OE)(U::Pe O OE) :: Pe O OE = struct { sub = \(x::O) -> Sigma O (\(u::O) -> and (Po O OE Ge x u) (MemberE O OE u U)); ext = \(x::O) -> \(y::O) -> \(h::sub x) -> \(h'::OE.eq x y) -> let mutual p1 :: O = h._1 p2 :: and (Po O OE Ge x h._1) (MemberE O OE h._1 U) = h._2 in struct { _1 = p1; _2 = struct { _1 = Ge.Pod.ext y x h._1 p1 (OE.sym x y h') (OE.ref h._1) p2._1; _2 = p2._2;};};} -- Intersection Inter (Op::Set)(U::Fam Op)(V::Fam Op) :: Fam Op = \(h::Op) -> Cart (U h) (V h) -- The type of formal spaces extending a presentation $Ge$ FormalSpace (O::Set)(OE::EQ O)(Ge::Pres O OE) :: Type = sig {cov :: CRe O OE; refl :: (a::O) -> (U::Pe O OE) -> (p::MemberE O OE a U) -> cov.rel a U; axiom :: (i::Ge.I) -> cov.rel (Ge.g i) (Ge.G i); trans :: (a::O) -> (U::Pe O OE) -> (V::Pe O OE) -> (p1::cov.rel a U) -> (p2::(y::O) -> MemberE O OE y U -> cov.rel y V) -> cov.rel a V; loc :: (a::O) -> (U::Pe O OE) -> (V::Pe O OE) -> (p::cov.rel a U) -> (q::cov.rel a V) -> cov.rel a (IntersectE O OE (SubGen O OE Ge U) (SubGen O OE Ge V)); ext :: (a::O) -> (b::O) -> (p::Ge.Pod.rel a b) -> cov.rel a (singletonE O OE b);} MonoEE (X::Set)(E::EQ X)(R::CRe X E) :: Type = (x::X) -> (S::Pe X E) -> (S'::Pe X E) -> SubclassEE X E S S' -> R.rel x S -> R.rel x S' MonoFS (O::Set)(OE::EQ O)(Ge::Pres O OE)(FS::FormalSpace O OE Ge) :: MonoEE O OE FS.cov = \(x::O) -> \(S::Pe O OE) -> \(S'::Pe O OE) -> \(h::SubclassEE O OE S S') -> \(h'::FS.cov.rel x S) -> FS.trans x S S' h' (\(y::O) -> \(h0::MemberE O OE y S) -> FS.refl y S' (h y h0)) -- Build basic family for regular universe from generator data Base (O::Set)(OE::EQ O)(Ge::Pres O OE) :: Fams = let mutual A :: Set = data ix | ixe (x::Ge.I) (y::Ge.I) | os | ose (x::O) (y::O) | ax (i::Ge.I) (x::O) | po (x::O) (y::O) | pos (x::O) B :: A -> Set = \(h::A) -> case h of { (ix) -> Ge.I; (ixe x y) -> Ge.IE.eq x y; (os) -> O; (ose x y) -> OE.eq x y; (ax i x) -> MemberE O OE x (Ge.G i); (po x y) -> Po O OE Ge x y; (pos x) -> MemberE O OE x Ge.Pos;} in struct { ind = A; fam = B;} small (O::Set)(OE::EQ O)(Ge::Pres O OE) :: EQS (Can (Base O OE Ge)) O = struct { eq = \(h::O) -> \(h'::O) -> emb@_ (ose@_ h h'); ref = OE.ref; sym = OE.sym; tra = OE.tra;} smallG (O::Set)(OE::EQ O)(Ge::Pres O OE)(i::Ge.I) :: Re (Can (Base O OE Ge)) O (small O OE Ge) = let F :: Fams = Can (Base O OE Ge) in let E' :: EQS (Can (Base O OE Ge)) O = small O OE Ge in UnionE (Base O OE Ge) O E' (sigma@_ (emb@_ ix@_) (\(j::(Base O OE Ge).fam ix@_) -> emb@_ (ixe@_ i j))) (\(h::(Can (Base O OE Ge)).fam (sigma@_ (emb@_ ix@_) (\(x::(Base O OE Ge).fam ix@_) -> emb@_ (ixe@_ i x)))) -> struct { sub = \(x::O) -> emb@_ (ax@_ (pr1 Ge.I (\(h'::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h')) h) x); ext = \(x::O) -> \(x'::O) -> \(h'::(Can (Base O OE Ge)).fam (sub x)) -> \(h0::(Can (Base O OE Ge)).fam (E'.eq x x')) -> let part1 :: (x0::O) -> (y::O) -> (x1::(Ge.G (pr1 ((Base O OE Ge).fam ix@_) (\(h1::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h1)) h)).sub x0) -> (x2::OE.eq x0 y) -> (Ge.G (pr1 ((Base O OE Ge).fam ix@_) (\(h1::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h1)) h)).sub y = (Ge.G (pr1 ((Base O OE Ge).fam ix@_) (\(h1::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h1)) h)).ext in part1 x x' h' h0;}) SmallGLemma (O::Set)(OE::EQ O)(Ge::Pres O OE)(i::Ge.I) :: Subclass (Can (Base O OE Ge)) O (small O OE Ge) (smallG O OE Ge i) (Ge.G i) = \(x::O) -> \(h::MemberSE (Can (Base O OE Ge)) O (small O OE Ge) x (smallG O OE Ge i)) -> let mutual part1 :: Sigma ((Base O OE Ge).fam ix@_) (\(h'::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h')) = pr1 (Sigma ((Base O OE Ge).fam ix@_) (\(h'::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h'))) (\(h'::Sigma ((Base O OE Ge).fam ix@_) (\(h'::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h'))) -> (Base O OE Ge).fam (ax@_ (pr1 Ge.I (\(h''::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h'')) h') x)) h part2 :: (Base O OE Ge).fam (ax@_ (pr1 Ge.I (\(h''::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h'')) (pr1 (Sigma ((Base O OE Ge).fam ix@_) (\(h'::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h'))) (\(h'::Sigma ((Base O OE Ge).fam ix@_) (\(h'::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h'))) -> (Base O OE Ge).fam (ax@_ (pr1 Ge.I (\(h''::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h'')) h') x)) h)) x) = pr2 (Sigma ((Base O OE Ge).fam ix@_) (\(h'::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h'))) (\(h'::Sigma ((Base O OE Ge).fam ix@_) (\(h'::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h'))) -> (Base O OE Ge).fam (ax@_ (pr1 Ge.I (\(h''::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h'')) h') x)) h in let mutual part11 :: (Base O OE Ge).fam ix@_ = pr1 ((Base O OE Ge).fam ix@_) (\(h'::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h')) part1 part12 :: (Base O OE Ge).fam (ixe@_ i (pr1 ((Base O OE Ge).fam ix@_) (\(h'::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h')) part1)) = pr2 ((Base O OE Ge).fam ix@_) (\(h'::(Base O OE Ge).fam ix@_) -> (Base O OE Ge).fam (ixe@_ i h')) part1 in let part3 :: EqualE O OE (Ge.G i) (Ge.G part11) = Ge.extG i part11 part12 in let part4 :: (x'::MemberE O OE x (Ge.G part11)) -> MemberE O OE x (Ge.G i) = proj2 ((x'::MemberE O OE x (Ge.G i)) -> MemberE O OE x (Ge.G part11)) ((x'::MemberE O OE x (Ge.G part11)) -> MemberE O OE x (Ge.G i)) (part3 x) in part4 part2 SubGenSE (O::Set) (OE::EQ O) (Ge::Pres O OE) (U'::Re (Can (Base O OE Ge)) O (small O OE Ge)) :: Re (Can (Base O OE Ge)) O (small O OE Ge) = struct { sub = \(x::O) -> sigma@_ (emb@_ os@_) (\(y::(Base O OE Ge).fam os@_) -> cross@_ (emb@_ (po@_ x y)) (U'.sub y)); ext = \(x::O) -> \(x'::O) -> \(h::(Can (Base O OE Ge)).fam (sub x)) -> \(h'::(Can (Base O OE Ge)).fam ((small O OE Ge).eq x x')) -> let mutual p1 :: (Base O OE Ge).fam os@_ = h._1 p2 :: Cart ((Base O OE Ge).fam (po@_ x h._1)) ((Can (Base O OE Ge)).fam (U'.sub h._1)) = h._2 in struct { _1 = p1; _2 = struct { _1 = Ge.Pod.ext x' x h._1 p1 (OE.sym x x' h') (OE.ref h._1) p2._1; _2 = p2._2;};};} IntersectionSE (O::Set) (OE::EQ O) (Ge::Pres O OE) (U::Re (Can (Base O OE Ge)) O (small O OE Ge)) (V::Re (Can (Base O OE Ge)) O (small O OE Ge)) :: Re (Can (Base O OE Ge)) O (small O OE Ge) = struct { sub = \(x::O) -> cross@_ (U.sub x) (V.sub x); ext = \(x::O) -> \(x'::O) -> \(h::(Can (Base O OE Ge)).fam (sub x)) -> \(h'::(Can (Base O OE Ge)).fam ((small O OE Ge).eq x x')) -> struct { _1 = U.ext x x' h._1 h'; _2 = V.ext x x' h._2 h';};} ExtIntSE (O::Set) (OE::EQ O) (Ge::Pres O OE) (U::Re (Can (Base O OE Ge)) O (small O OE Ge)) (U'::Re (Can (Base O OE Ge)) O (small O OE Ge)) (V::Re (Can (Base O OE Ge)) O (small O OE Ge)) (V'::Re (Can (Base O OE Ge)) O (small O OE Ge)) (p::EqualsetsSE (Can (Base O OE Ge)) O (small O OE Ge) U V) (q::EqualsetsSE (Can (Base O OE Ge)) O (small O OE Ge) U' V') :: EqualsetsSE (Can (Base O OE Ge)) O (small O OE Ge) (IntersectionSE O OE Ge U U') (IntersectionSE O OE Ge V V') = \(x::O) -> struct { _1 = \(h::MemberSE (Can (Base O OE Ge)) O (small O OE Ge) x (IntersectionSE O OE Ge U U')) -> struct { _1 = (p x)._1 h._1; _2 = (q x)._1 h._2;}; _2 = \(h::MemberSE (Can (Base O OE Ge)) O (small O OE Ge) x (IntersectionSE O OE Ge V V')) -> struct { _1 = (p x)._2 h._1; _2 = (q x)._2 h._2;};} ILem (O::Set) (OE::EQ O) (Ge::Pres O OE) (U'::Re (Can (Base O OE Ge)) O (small O OE Ge)) (V'::Re (Can (Base O OE Ge)) O (small O OE Ge)) (U::Pe O OE) (V::Pe O OE) (p::Subclass (Can (Base O OE Ge)) O (small O OE Ge) U' U) (q::Subclass (Can (Base O OE Ge)) O (small O OE Ge) V' V) :: Subclass (Can (Base O OE Ge)) O (small O OE Ge) (IntersectionSE O OE Ge U' V') (IntersectE O (makebigE (Can (Base O OE Ge)) O (small O OE Ge)) U V) = \(x::O) -> \(h::MemberSE (Can (Base O OE Ge)) O (small O OE Ge) x (IntersectionSE O OE Ge U' V')) -> struct { _1 = p x h._1; _2 = q x h._2;} SGLem (O::Set) (OE::EQ O) (Ge::Pres O OE) (U'::Re (Can (Base O OE Ge)) O (small O OE Ge)) (U::Pe O OE) (p::Subclass (Can (Base O OE Ge)) O (small O OE Ge) U' U) :: Subclass (Can (Base O OE Ge)) O (small O OE Ge) (SubGenSE O OE Ge U') (SubGen O (makebigE (Can (Base O OE Ge)) O (small O OE Ge)) Ge U) = \(x::O) -> \(h::MemberSE (Can (Base O OE Ge)) O (small O OE Ge) x (SubGenSE O OE Ge U')) -> let mutual p1 :: (Base O OE Ge).fam os@_ = h._1 p2 :: (Can (Base O OE Ge)).fam (cross@_ (emb@_ (po@_ x h._1)) (U'.sub h._1)) = h._2 in let p2a :: (Base O OE Ge).fam (po@_ x h._1) = p2._1 in struct { _1 = p1; _2 = struct { _1 = p2a; _2 = p p1 p2._2;};} -- build singleton singletonSE (O::Set)(OE::EQ O)(Ge::Pres O OE)(x::O) :: Re (Can (Base O OE Ge)) O (small O OE Ge) = struct { sub = \(x'::O) -> emb@_ (ose@_ x' x); ext = \(x'::O) -> \(x0::O) -> \(h::(Can (Base O OE Ge)).fam (sub x')) -> \(h'::(Can (Base O OE Ge)).fam ((small O OE Ge).eq x' x0)) -> OE.tra x0 x' x (OE.sym x' x0 h') h;} -- Build cover from derivation CoverDer (O::Set)(OE::EQ O)(Ge::Pres O OE) :: Type = sig {D :: Set; L :: D -> O; R :: D -> Re (Can (Base O OE Ge)) O (small O OE Ge);} MinCovDer (O::Set)(OE::EQ O)(Ge::Pres O OE) :: CoverDer O OE Ge = let F :: Fams = Can (Base O OE Ge) in let E' :: EQS (Can (Base O OE Ge)) O = small O OE Ge in let MkSet (U::Re F O E') :: Set = Sigma O (\(h::O) -> MemberSE F O E' h U) in let mutual Der :: Set = data ref (a::O) (U::Re F O E') (p::MemberSE F O E' a U) | axiom (i::Ge.I) | trans (U::Re F O E') (p::Der) (q::MkSet (C p) -> Der) (r::(x::MkSet (C p)) -> and (OE.eq (c (q x)) x._1) (EqualsetsSE F O E' (C (q x)) U)) | loc (p::Der) (q::Der) (e::OE.eq (c p) (c q)) | ext (a::O) (b::O) (p::Ge.Pod.rel a b) c (d::Der) :: O = case d of { (ref a U p) -> a; (axiom i) -> Ge.g i; (trans U p q r) -> c p; (loc p q e) -> c p; (ext a b p) -> a;} C (d::Der) :: Re F O E' = case d of { (ref a U p) -> U; (axiom i) -> smallG O OE Ge i; (trans U p q r) -> U; (loc p q e) -> IntersectionSE O OE Ge (SubGenSE O OE Ge (C p)) (SubGenSE O OE Ge (C q)); (ext a b p) -> singletonSE O OE Ge b;} in struct { D = Der; L = c; R = C;} GenCov (O::Set)(OE::EQ O)(Ge::Pres O OE)(Min::CoverDer O OE Ge) :: CRSE (Can (Base O OE Ge)) O (small O OE Ge) = let F :: Fams = Can (Base O OE Ge) in let E' :: EQS (Can (Base O OE Ge)) O = small O OE Ge in let MkSet (U::Re F O E') :: Set = Sigma O (\(h::O) -> MemberSE F O E' h U) in let Min2 :: CoverDer O OE Ge = MinCovDer O OE Ge in let mutual Der :: Set = Min.D c (d::Der) :: O = Min.L d C (d::Der) :: Re F O E' = Min.R d in struct { rel = \(x::O) -> \(U::Re (Can (Base O OE Ge)) O (small O OE Ge)) -> Sigma Der (\(d::Der) -> and (OE.eq x (c d)) (EqualsetsSE F O E' (C d) U)); ext = \(x::O) -> \(x'::O) -> \(U::Re (Can (Base O OE Ge)) O (small O OE Ge)) -> \(U'::Re (Can (Base O OE Ge)) O (small O OE Ge)) -> \(h::(Can (Base O OE Ge)).fam ((small O OE Ge).eq x x')) -> \(h'::EqualsetsSE (Can (Base O OE Ge)) O (small O OE Ge) U U') -> \(h0::rel x U) -> let mutual der :: Der = pr1 Der (\(d::Der) -> and (OE.eq x (c d)) (EqualsetsSE F O E' (C d) U)) h0 part1 :: OE.eq x (c der) = proj1 (OE.eq x (c (pr1 Der (\(d::Der) -> and (OE.eq x (c d)) (EqualsetsSE F O E' (C d) U)) h0))) (EqualsetsSE F O E' (C (pr1 Der (\(d::Der) -> and (OE.eq x (c d)) (EqualsetsSE F O E' (C d) U)) h0)) U) (pr2 Der (\(d::Der) -> and (OE.eq x (c d)) (EqualsetsSE F O E' (C d) U)) h0) part2 :: EqualsetsSE F O E' (C der) U = proj2 (OE.eq x (c (pr1 Der (\(d::Der) -> and (OE.eq x (c d)) (EqualsetsSE F O E' (C d) U)) h0))) (EqualsetsSE F O E' (C (pr1 Der (\(d::Der) -> and (OE.eq x (c d)) (EqualsetsSE F O E' (C d) U)) h0)) U) (pr2 Der (\(d::Der) -> and (OE.eq x (c d)) (EqualsetsSE F O E' (C d) U)) h0) in struct { _1 = der; _2 = struct { _1 = OE.tra x' x (c der) (OE.sym x x' h) part1; _2 = transEE O OE (big F O E' (C der)) (big (Can (Base O OE Ge)) O (small O OE Ge) U) (big (Can (Base O OE Ge)) O (small O OE Ge) U') part2 h';};};} reflGC (O::Set) (OE::EQ O) (Ge::Pres O OE) (a::O) (U::Re (Can (Base O OE Ge)) O (small O OE Ge)) (p::MemberSE (Can (Base O OE Ge)) O (small O OE Ge) a U) :: (GenCov O OE Ge (MinCovDer O OE Ge)).rel a U = struct { _1 = ref@_ a U p; _2 = struct { _1 = OE.ref a; _2 = reflSE (Can (Base O OE Ge)) O (small O OE Ge) U;};} reflGC2 (O::Set)(OE::EQ O)(Ge::Pres O OE) :: ReflexiveSE (Can (Base O OE Ge)) O (small O OE Ge) (GenCov O OE Ge (MinCovDer O OE Ge)) = reflGC O OE Ge reflLemma (O::Set) (OE::EQ O) (Ge::Pres O OE) (R::CRSE (Can (Base O OE Ge)) O (small O OE Ge)) :: ReflexiveSE (Can (Base O OE Ge)) O (small O OE Ge) R -> ReflexiveE O OE (Extend (Can (Base O OE Ge)) O (small O OE Ge) R) = \(h::ReflexiveSE (Can (Base O OE Ge)) O (small O OE Ge) R) -> \(U::Pe O OE) -> \(a::O) -> \(h'::MemberE O OE a U) -> struct { _1 = singletonSE O OE Ge a; _2 = struct { _1 = \(x::O) -> \(h0::MemberSE (Can (Base O OE Ge)) O (small O OE Ge) x (singletonSE O OE Ge a)) -> U.ext a x h' (OE.sym x a h0); _2 = h a (singletonSE O OE Ge a) (OE.ref a);};} transGC (O::Set)(OE::EQ O)(Ge::Pres O OE) :: TransitiveSE (Can (Base O OE Ge)) O (small O OE Ge) (GenCov O OE Ge (MinCovDer O OE Ge)) = let F :: Fams = Can (Base O OE Ge) in let E' :: EQS F O = small O OE Ge in let M :: CoverDer O OE Ge = MinCovDer O OE Ge in let MkSet (U::Re F O E') :: Set = Sigma O (\(h::O) -> MemberSE F O E' h U) in let mutual Der :: Set = M.D c (d::Der) :: O = M.L d C (d::Der) :: Re (Can (Base O OE Ge)) O (small O OE Ge) = M.R d EL (x::O)(y::O) :: Set = OE.eq x y in \(U::Re F O E') -> \(V::Re F O E') -> \(x::O) -> \(h::(GenCov O OE Ge (MinCovDer O OE Ge)).rel x U) -> \(h'::ForAll O (\(y::O) -> (x'::F.fam (U.sub y)) -> (GenCov O OE Ge (MinCovDer O OE Ge)).rel y V)) -> let mutual d :: Der = pr1 M.D (\(d::M.D) -> and (OE.eq x (M.L d)) (EqualsetsSE F O E' (M.R d) U)) h h1 :: EL x (c d) = proj1 (OE.eq x (M.L (pr1 M.D (\(d::M.D) -> and (OE.eq x (M.L d)) (EqualsetsSE F O E' (M.R d) U)) h))) (EqualsetsSE F O E' (M.R (pr1 M.D (\(d::M.D) -> and (OE.eq x (M.L d)) (EqualsetsSE F O E' (M.R d) U)) h)) U) (pr2 M.D (\(d::M.D) -> and (OE.eq x (M.L d)) (EqualsetsSE F O E' (M.R d) U)) h) h2 :: EqualsetsSE F O E' (C d) U = proj2 (OE.eq x (M.L (pr1 M.D (\(d::M.D) -> and (OE.eq x (M.L d)) (EqualsetsSE F O E' (M.R d) U)) h))) (EqualsetsSE F O E' (M.R (pr1 M.D (\(d::M.D) -> and (OE.eq x (M.L d)) (EqualsetsSE F O E' (M.R d) U)) h)) U) (pr2 M.D (\(d::M.D) -> and (OE.eq x (M.L d)) (EqualsetsSE F O E' (M.R d) U)) h) in let mutual h2a (u::O) :: (x'::MemberSE F O E' u (C d)) -> MemberSE F O E' u U = proj1 ((x'::MemberSE F O E' u (M.R (pr1 M.D (\(d::M.D) -> and (OE.eq x (M.L d)) (EqualsetsSE F O E' (M.R d) U)) h))) -> MemberSE F O E' u U) ((x'::MemberSE F O E' u U) -> MemberSE F O E' u (M.R (pr1 M.D (\(d::M.D) -> and (OE.eq x (M.L d)) (EqualsetsSE F O E' (M.R d) U)) h))) (h2 u) h2b (u::O) :: (x'::MemberSE F O E' u U) -> MemberSE F O E' u (C d) = proj2 ((x'::MemberSE F O E' u (M.R (pr1 M.D (\(d::M.D) -> and (OE.eq x (M.L d)) (EqualsetsSE F O E' (M.R d) U)) h))) -> MemberSE F O E' u U) ((x'::MemberSE F O E' u U) -> MemberSE F O E' u (M.R (pr1 M.D (\(d::M.D) -> and (OE.eq x (M.L d)) (EqualsetsSE F O E' (M.R d) U)) h))) (h2 u) in let mutual h3 (u::O)(v::F.fam (U.sub u)) :: Der = (h' u v)._1 h4 (u::O)(v::F.fam (U.sub u)) :: EL u (c (h' u v)._1) = (h' u v)._2._1 h5 (u::O)(v::F.fam (U.sub u)) :: EqualsetsSE F O E' (C (h' u v)._1) V = (h' u v)._2._2 in let K' :: Set = MkSet (C d) in let mutual h3c (w::K') :: Der = split O (\(h0::O) -> MemberSE F O E' h0 (M.R d)) (\(h0::Sigma O (\(h0::O) -> MemberSE F O E' h0 (M.R d))) -> M.D) w (\(x'::O) -> \(y::MemberSE F O E' x' (M.R d)) -> h3 x' (h2a x' y)) h4c (w::K') :: OE.eq w._1 (c (h3c w)) = h4 w._1 (h2a w._1 w._2) h5c (w::K') :: and (EL (c (h3c w)) w._1) (EqualsetsSE F O E' (C (h3c w)) V) = struct { _1 = OE.sym w._1 (c (h3c w)) (h4c w); _2 = h5 w._1 (h2a w._1 w._2);} in struct { _1 = trans@_ V d h3c h5c; _2 = struct { _1 = h1; _2 = reflSE F O E' V;};} GeneratedFS (O::Set)(OE::EQ O)(G::Pres O OE) :: FormalSpace O OE G = let F :: Fams = Base O OE G in let M :: CoverDer O OE G = MinCovDer O OE G in let MinCov :: CRSE (Can (Base O OE G)) O (small O OE G) = GenCov O OE G M in struct { cov = Extend (Can F) O (small O OE G) MinCov; refl = \(a::O) -> \(U::Pe O OE) -> \(p::MemberE O OE a U) -> reflLemma O OE G MinCov (reflGC2 O OE G) U a p; axiom = \(i::G.I) -> struct { _1 = smallG O OE G i; _2 = struct { _1 = SmallGLemma O OE G i; _2 = struct { _1 = axiom@_ i; _2 = struct { _1 = OE.ref (G.g i); _2 = \(x::O) -> struct { _1 = \(h::MemberSE (Can (Base O OE G)) O (small O OE G) x (M.R (axiom@_ i))) -> h; _2 = \(h::MemberSE (Can (Base O OE G)) O (small O OE G) x (smallG O OE G i)) -> h;};};};};}; trans = \(a::O) -> \(U::Pe O OE) -> \(V::Pe O OE) -> \(p1::cov.rel a U) -> \(p2::(y::O) -> (x::MemberE O OE y U) -> cov.rel y V) -> let trlemma :: TransitiveSE (Can F) O (small O OE G) MinCov = transGC O OE G in let trlemma2 :: TransitiveE ((Can F).fam (emb@_ os@_)) (makebigE (Can F) ((Can F).fam (emb@_ os@_)) (small O OE G)) (Extend (Can F) ((Can F).fam (emb@_ os@_)) (small O OE G) MinCov) = TrThm2 F (emb@_ os@_) (small O OE G) MinCov (reflGC2 ((Can F).fam (emb@_ os@_)) OE G) (transGC O OE G) in trlemma2 U V a p1 p2; ext = \(a::O) -> \(b::O) -> \(p::G.Pod.rel a b) -> struct { _1 = singletonSE O OE G b; _2 = struct { _1 = \(x::O) -> \(h::MemberSE (Can F) O (small O OE G) x (singletonSE O OE G b)) -> h; _2 = struct { _1 = ext@_ a b p; _2 = struct { _1 = OE.ref a; _2 = \(x::O) -> struct { _1 = \(h::MemberSE (Can (Base O OE G)) O (small O OE G) x (M.R (ext@_ a b p))) -> h; _2 = \(h::MemberSE (Can (Base O OE G)) O (small O OE G) x (singletonSE O OE G b)) -> h;};};};};}; loc = \(a::O) -> \(U''::Pe O OE) -> \(V::Pe O OE) -> \(p::cov.rel a U'') -> \(q::cov.rel a V) -> let mutual U' :: Re (Can F) O (small O OE G) = p._1 p1 :: Subclass (Can F) O (small O OE G) p._1 U'' = p._2._1 p2 :: MinCov.rel a U' = p._2._2 V' :: Re (Can F) O (small O OE G) = q._1 q1 :: Subclass (Can F) O (small O OE G) V' V = q._2._1 q2 :: MinCov.rel a V' = q._2._2 EL (x::O)(y::O) :: Set = OE.eq x y in let mutual g1 :: M.D = p2._1 g2 :: and (EL a (M.L g1)) (EqualsetsSE (Can (Base O OE G)) O (small O OE G) (M.R g1) U') = p2._2 h1 :: M.D = q2._1 h2 :: and (EL a (M.L h1)) (EqualsetsSE (Can (Base O OE G)) O (small O OE G) (M.R h1) V') = q2._2 in let mutual c1 :: O = M.L g1 c2 :: O = M.L h1 in let mutual d1 :: EL a c1 = p2._2._1 d2 :: EL a c2 = q2._2._1 in let mutual e1 :: EqualsetsSE (Can (Base O OE G)) O (small O OE G) (M.R g1) U' = g2._2 e2 :: EqualsetsSE (Can (Base O OE G)) O (small O OE G) (M.R h1) V' = h2._2 in let mutual s1 :: Subclass (Can F) O (small O OE G) (M.R g1) U'' = \(x::O) -> \(h::MemberSE (Can F) O (small O OE G) x (M.R p._2._2._1)) -> p1 x ((e1 x)._1 h) s2 :: Subclass (Can F) O (small O OE G) (M.R h1) V = \(x::O) -> \(h::MemberSE (Can F) O (small O OE G) x (M.R q._2._2._1)) -> q1 x ((e2 x)._1 h) in let mutual U3 :: Re (Can (Base O OE G)) O (small O OE G) = M.R g1 V3 :: Re (Can (Base O OE G)) O (small O OE G) = M.R h1 in struct { _1 = IntersectionSE O OE G (SubGenSE O OE G U3) (SubGenSE O OE G V3); _2 = struct { _1 = ILem O OE G (SubGenSE O OE G U3) (SubGenSE O OE G V3) (SubGen O OE G U'') (SubGen O OE G V) (SGLem O OE G U3 U'' s1) (SGLem O OE G V3 V s2); _2 = struct { _1 = loc@_ g1 h1 (OE.tra c1 a c2 (OE.sym a c1 d1) d2); _2 = struct { _1 = d1; _2 = \(x::O) -> struct { _1 = \(h::MemberSE (Can (Base O OE G)) O (small O OE G) x (M.R (loc@_ p2._1 q2._1 (OE.tra c1 a c2 (OE.sym a c1 d1) d2)))) -> h; _2 = \(h::MemberSE (Can (Base O OE G)) O (small O OE G) x (IntersectionSE O OE G (SubGenSE O OE G U3) (SubGenSE O OE G V3))) -> h;};};};};};} Minimality (O::Set)(OE::EQ O)(G::Pres O OE)(FS::FormalSpace O OE G) :: (x::O) -> (U::Pe O OE) -> (GeneratedFS O OE G).cov.rel x U -> FS.cov.rel x U = \(x::O) -> \(U::Pe O OE) -> \(h::(GeneratedFS O OE G).cov.rel x U) -> let M :: CoverDer O OE G = MinCovDer O OE G in let Kv (x::O)(V::Pe O OE) :: Set = FS.cov.rel x V in let Mono (d::M.D) (W::Re (Can (Base O OE G)) O (small O OE G)) (V::Pe O OE) (p::Subclass (Can (Base O OE G)) O (small O OE G) W V) (q::Kv (M.L d) (big (Can (Base O OE G)) O (small O OE G) W)) :: Kv (M.L d) V = MonoFS O OE G FS (M.L d) (big (Can (Base O OE G)) O (small O OE G) W) V p q in let mutual c (d::M.D) :: O = M.L d C (d::M.D) :: Re (Can (Base O OE G)) O (small O OE G) = M.R d EL (x::O)(y::O) :: Set = OE.eq x y in let lem1 (d::M.D) (U::Pe O OE) (p::Subclass (Can (Base O OE G)) O (small O OE G) (C d) U) :: Kv (c d) U = case d of { (ref a U' p') -> Mono d U' U p (FS.refl (c (ref@_ a U' p')) (big (Can (Base O OE G)) O (small O OE G) U') p'); (axiom i) -> Mono d (C d) U p (MonoFS O OE G FS (c (axiom@_ i)) (G.G i) (big (Can (Base O OE G)) O (small O OE G) (C (axiom@_ i))) (\(x'::O) -> \(h'::MemberE O OE x' (G.G i)) -> struct { _1 = {-#h#-}struct { _1 = i; _2 = G.IE.ref i;}; _2 = h';}) (FS.axiom i)); (trans U' p' q r) -> let ih (x::O) (s::MemberSE (Can (Base O OE G)) O (small O OE G) x (C p')) :: Kv (c (q (struct { _1 = x; _2 = s;}))) U = lem1 (q (struct { _1 = x; _2 = s;})) U (\(x'::O) -> \(h'::MemberSE (Can (Base O OE G)) O (small O OE G) x' (C (q (struct { _1 = x; _2 = s;})))) -> let su1 :: MemberSE (Can (Base O OE G)) O (small O OE G) x' U' = ((r (struct { _1 = x; _2 = s;}))._2 x')._1 h' in p x' su1) in FS.trans (c (trans@_ U' p' q r)) (big (Can (Base O OE G)) O (small O OE G) (C p')) U (lem1 p' (big (Can (Base O OE G)) O (small O OE G) (C p')) (\(x'::O) -> \(h'::MemberSE (Can (Base O OE G)) O (small O OE G) x' (C p')) -> h')) (\(y::O) -> \(h'::MemberE O OE y (big (Can (Base O OE G)) O (small O OE G) (C p'))) -> FS.cov.ext (c (q (struct { _1 = y; _2 = h';}))) y U U (proj1 (OE.eq (c (q (struct { _1 = y; _2 = h';}))) y) (EqualE O OE (big (Can (Base O OE G)) O (small O OE G) (C (q (struct { _1 = y; _2 = h';})))) (big (Can (Base O OE G)) O (small O OE G) U')) (r (struct { _1 = y; _2 = h';}))) (refEE O OE U) (ih y h')); (ext a b q) -> Mono d (C d) U p (FS.ext (M.L (ext@_ a b q)) b q); (loc p' q e) -> let mutual su1 :: Kv (c p') (big (Can (Base O OE G)) O (small O OE G) (C p')) = lem1 p' (big (Can (Base O OE G)) O (small O OE G) (C p')) (\(x'::O) -> \(h'::MemberSE (Can (Base O OE G)) O (small O OE G) x' (C p')) -> h') su2 :: Kv (c q) (big (Can (Base O OE G)) O (small O OE G) (C q)) = lem1 q (big (Can (Base O OE G)) O (small O OE G) (C q)) (\(x'::O) -> \(h'::MemberSE (Can (Base O OE G)) O (small O OE G) x' (C q)) -> h') in let su3 :: Kv (c p') (IntersectE O OE (SubGen O OE G (big (Can (Base O OE G)) O (small O OE G) (C p'))) (SubGen O OE G (big (Can (Base O OE G)) O (small O OE G) (C q)))) = FS.loc (c p') (big (Can (Base O OE G)) O (small O OE G) (C p')) (big (Can (Base O OE G)) O (small O OE G) (C q)) su1 (FS.cov.ext (c q) (c p') (big (Can (Base O OE G)) O (small O OE G) (C q)) (big (Can (Base O OE G)) O (small O OE G) (C q)) (OE.sym (c p') (c q) e) (refEE O OE (big (Can (Base O OE G)) O (small O OE G) (C q))) su2) in Mono p' (IntersectionSE O OE G (SubGenSE O OE G (C p')) (SubGenSE O OE G (C q))) U p su3;} in let mutual W :: Re (Can (Base O OE G)) O (small O OE G) = h._1 p2 :: Subclass (Can (Base O OE G)) O (small O OE G) W U = h._2._1 p3 :: (GenCov O OE G M).rel x W = h._2._2 in let mutual q1 :: M.D = p3._1 q2 :: EL x (c q1) = p3._2._1 q3 :: EqualsetsSE (Can (Base O OE G)) O (small O OE G) (C q1) W = p3._2._2 in let q4 :: Subclass (Can (Base O OE G)) O (small O OE G) (C q1) U = \(x'::O) -> \(h'::MemberSE (Can (Base O OE G)) O (small O OE G) x' (C q1)) -> p2 x' ((q3 x')._1 h') in FS.cov.ext (c q1) x U U (OE.sym x (c q1) q2) (refEE O OE U) (lem1 q1 U q4) -- Formal spaces with positivity predicate Inhabited (X::Set)(E::EQ X)(S::Pe X E) :: Set = Sigma X (\(h::X) -> MemberE X E h S) FormalSpacePos (O::Set)(OE::EQ O)(G::Pres O OE) :: Type = sig {fs :: FormalSpace O OE G; p1 :: (x::O) -> (U::Pe O OE) -> (p::MemberE O OE x G.Pos) -> (r::fs.cov.rel x U) -> Inhabited O OE U; p2 :: (x::O) -> (U::Pe O OE) -> (r::fs.cov.rel x U) -> fs.cov.rel x (IntersectE O OE U G.Pos);} {-# Alfa hiding on con "zero" as "0" con "succ" as "S" var "Nat" as "N" with symbolfont var "Prod" infix 7 as "´" with symbolfont var "Sum" infix as "+" var "Fun" infix rightassoc as "®" with symbolfont var "apply" hide 2 var "pair" hide 2 tuple var "pr1" hide 2 var "pr2" hide 2 var "rec" hide 1 var "when" hide 3 var "empty" as "Æ" with symbolfont var "elempty" as "!" var "Pi" as "P" with symbolfont var "Sigma" as "S" with symbolfont var "split" hide 3 var "Cart" infix as "´" with symbolfont con "sigma" as "s" with symbolfont con "emb" as "e" with symbolfont var "Power" as "Rw" var "Member" hide 2 var "Subclass" hide 3 infix as "Í" with symbolfont var "iff" infix as "«" with symbolfont var "Can" as "G" with symbolfont var "ind" var "fam" var "R" as "R" var "and" infix as "Ù" with symbolfont var "MemberSE" hide 3 infix as "e" with symbolfont var "MemberE" hide 2 infix as "e" with symbolfont var "EqualE" hide 2 infix as "==" var "SubsetsE" hide 2 infix as "Í" with symbolfont var "EqualsetsSE" hide 3 infix as "==" var "SubsetSE" hide 3 infix as "Í" with symbolfont var "E" var "Es" var "Rs" infix as "<" with symbolfont var "Ex" infix as "<<" with symbolfont var "Exs" infix as "<<" with symbolfont var "proj1" hide 2 var "proj2" hide 2 var "singletonE" hide 2 mixfix as "{_}" var "IntersectionSE" hide 3 infix as "Ç" with symbolfont var "singletonSE" hide 3 mixfix as "{_}" var "MinCovDer" var "IntersectE" hide 2 infix as "Ç" with symbolfont var "Base" hide 2 as "F" with symbolfont var "MonoFS" hide 2 var "SubGenSE" hide 2 infix as "¯" with symbolfont var "small" hide 2 var "smallG" hide 2 var "big" hide 3 postfix as "#" var "makebigE" hide 2 var "SubGen" hide 2 infix as "¯" with symbolfont var "ForAll" hide 1 quantifier domain on as "\"" with symbolfont var "SubclassEE" hide 2 infix as "Í" with symbolfont var "Exists" hide 1 quantifier domain on as "\$" with symbolfont con "cross" infix as "´" with symbolfont var "Kv" infix as "<|" var "EL" infix as "»" with symbolfont var "Inhabited" hide 2 #-}