discipline of declaring hints for carrier of structures (setoids and categories) and no
other hints simplified many passages
rel: arrows1 ? concr form
}.
-notation "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y}.
-notation "⊩" with precedence 60 for @{'Vdash}.
-
-interpretation "basic pair relation" 'Vdash2 x y = (rel _ x y).
-interpretation "basic pair relation (non applied)" 'Vdash = (rel _).
+interpretation "basic pair relation" 'Vdash2 x y c = (fun21 ___ (rel c) x y).
+interpretation "basic pair relation (non applied)" 'Vdash c = (rel c).
alias symbol "eq" = "setoid1 eq".
alias symbol "compose" = "category1 composition".
]
qed.
-lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
+definition relation_pair_of_relation_pair_setoid :
+ ∀P,Q. relation_pair_setoid P Q → relation_pair P Q ≝ λP,Q,x.x.
+coercion relation_pair_of_relation_pair_setoid.
+
+lemma eq_to_eq':
+ ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
intros 7 (o1 o2 r r' H c1 f2);
split; intro H1;
[ lapply (fi ?? (commute ?? r c1 f2) H1) as H2;
apply ((id_neutral_left1 ????)‡#);]
qed.
+definition basic_pair_of_BP : objs1 BP → basic_pair ≝ λx.x.
+coercion basic_pair_of_BP.
+
+definition relation_pair_setoid_of_arrows1_BP :
+ ∀P,Q. arrows1 BP P Q → relation_pair_setoid P Q ≝ λP,Q,x.x.
+coercion relation_pair_setoid_of_arrows1_BP.
+
definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
intros; constructor 1;
[ apply (ext ? ? (rel o));
definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
intros (o); constructor 1;
- [ apply (λx:concr o.λS: Ω \sup (form o).∃y:form o.y ∈ S ∧ x ⊩ y);
+ [ apply (λx:concr o.λS: Ω \sup (form o).∃y:form o.y ∈ S ∧ x ⊩_o y);
| intros; split; intros; cases e2; exists [1,3: apply w]
[ apply (. (#‡e1^-1)‡(e^-1‡#)); assumption
| apply (. (#‡e1)‡(e‡#)); assumption]]
compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V)
}.
-lemma hint: basic_topology → objs1 REL.
- intro; apply (carrbt b);
-qed.
-coercion hint.
-
record continuous_relation (S,T: basic_topology) : Type1 ≝
{ cont_rel:> arrows1 ? S T;
reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U);
| simplify; intros; apply trans1; [2: apply H |3: apply H1; |1: skip]]]
qed.
-definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel.
-
-coercion cont_rel'.
-
-definition cont_rel'': ∀S,T: basic_topology. continuous_relation_setoid S T → binary_relation S T ≝ cont_rel.
-
-coercion cont_rel''.
-
theorem continuous_relation_eq':
∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
a = a' → ∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X).
[ apply (f2 (f x1)) | apply (f1 (f3 z1))]]]
qed.
+definition CProp0_of_CPROP: carr1 CPROP → CProp0 ≝ λx.x.
+coercion CProp0_of_CPROP.
+
alias symbol "eq" = "setoid1 eq".
definition fi': ∀A,B:CPROP. A = B → B → A.
intros; apply (fi ?? e); assumption.
| apply (fi ?? e1); apply f; apply (if ?? e); assumption]]
qed.
+
record category : Type1 ≝
{ objs:> Type0;
arrows: objs → objs → setoid;
id: ∀o:objs. arrows o o;
- comp: ∀o1,o2,o3. binary_morphism1 (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
+ comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
definition SET: category1.
constructor 1;
[ apply setoid;
- | apply rule (λS,T:setoid.unary_morphism_setoid S T);
+ | apply rule (λS,T:setoid.setoid1_of_setoid (unary_morphism_setoid S T));
| intros; constructor 1; [ apply (λx:carr o.x); | intros; assumption ]
- | intros; constructor 1; [ intros; constructor 1; [ apply (λx. t1 (t x)); | intros;
+ | intros; constructor 1; [ intros; constructor 1; [ apply (λx. c1 (c x)); | intros;
apply († (†e));]
| intros; whd; intros; simplify; whd in H1; whd in H;
apply trans; [ apply (b (a' a1)); | lapply (prop1 ?? b (a a1) (a' a1));
]
qed.
-definition setoid_of_SET: objs1 SET → setoid.
- intros; apply o; qed.
+definition setoid_of_SET: objs1 SET → setoid ≝ λx.x.
coercion setoid_of_SET.
+definition unary_morphism_setoid_of_arrows1_SET:
+ ∀P,Q.arrows1 SET P Q → unary_morphism_setoid P Q ≝ λP,Q,x.x.
+coercion unary_morphism_setoid_of_arrows1_SET.
+
notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
interpretation "unary morphism" 'Imply a b = (arrows1 SET a b).
| simplify; intros; apply trans1; [2: apply f; | skip | apply f1]]]
qed.
+definition unary_morphism1_of_unary_morphism1_setoid1 :
+ ∀S,T. unary_morphism1_setoid1 S T → unary_morphism1 S T ≝ λP,Q,x.x.
+coercion unary_morphism1_of_unary_morphism1_setoid1.
+
definition SET1: category2.
constructor 1;
[ apply setoid1;
- | apply rule (λS,T.unary_morphism1_setoid1 S T);
+ | apply rule (λS,T.setoid2_of_setoid1 (unary_morphism1_setoid1 S T));
| intros; constructor 1; [ apply (λx.x); | intros; assumption ]
- | intros; constructor 1; [ intros; constructor 1; [ apply (λx. t1 (t x)); | intros;
+ | intros; constructor 1; [ intros; constructor 1; [ apply (λx. c1 (c x)); | intros;
apply († (†e));]
| intros; whd; intros; simplify; whd in H1; whd in H;
apply trans1; [ apply (b (a' a1)); | lapply (prop11 ?? b (a a1) (a' a1));
]
qed.
-definition setoid1_OF_SET1: objs2 SET1 → setoid1.
- intros; apply o; qed.
+definition setoid1_of_SET1: objs2 SET1 → setoid1 ≝ λx.x.
+coercion setoid1_of_SET1.
-coercion setoid1_OF_SET1.
+definition unary_morphism1_setoid1_of_arrows2_SET1:
+ ∀P,Q.arrows2 SET1 P Q → unary_morphism1_setoid1 P Q ≝ λP,Q,x.x.
+coercion unary_morphism1_setoid1_of_arrows2_SET1.
-definition setoid2_OF_category2: Type_OF_category2 SET1 → setoid2.
- intro; apply (setoid2_of_setoid1 t); qed.
-coercion setoid2_OF_category2.
-
-definition objs2_OF_category1: Type_OF_category1 SET → objs2 SET1.
- intro; apply (setoid1_of_setoid t); qed.
-coercion objs2_OF_category1.
+variant objs2_of_category1: objs1 SET → objs2 SET1 ≝ setoid1_of_setoid.
+coercion objs2_of_category1.
-definition Type1_OF_SET1: Type_OF_category2 SET1 → Type1.
- intro; whd in t; apply (carr1 t);
-qed.
-coercion Type1_OF_SET1.
-
-definition Type_OF_setoid1_of_carr: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*).
- [ apply rule U;
- | intros; apply c;]
-qed.
-coercion Type_OF_setoid1_of_carr.
-
-definition carr' ≝ λx:Type_OF_category1 SET.Type_OF_Type0 (carr x).
-coercion carr'. (* we prefer the lower carrier projection *)
+prefer coercion Type_OF_setoid. (* we prefer the lower carrier projection *)
+prefer coercion Type_OF_objs1.
interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b).
-
-lemma unary_morphism1_of_arrows1_SET1: ∀S,T. (S ⇒ T) → unary_morphism1 S T.
- intros; apply t;
-qed.
-coercion unary_morphism1_of_arrows1_SET1.
all_covered: ∀x: concr bp. x ⊩ full_subset (form bp)
}.
-definition bp': concrete_space → basic_pair ≝ λc.bp c.
-coercion bp'.
-
-definition bp'': concrete_space → objs1 BP ≝ λc.bp c.
-coercion bp''.
-
record convergent_relation_pair (CS1,CS2: concrete_space) : Type1 ≝
{ rp:> arrows1 ? CS1 CS2;
respects_converges:
minus_image ?? rp\sub\c (BPextS CS2 (full_subset (form CS2))) = BPextS CS1 (full_subset (form CS1))
}.
(*
-definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝
- λCS1,CS2,c. rp CS1 CS2 c.
-
-coercion rp'.
-
definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1.
intros;
constructor 1;
| intros 3; apply trans1]]
qed.
-definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝
- λCS1,CS2,c.rp ?? c.
-
-coercion rp''.
-
definition convergent_relation_space_composition:
∀o1,o2,o3: concrete_space.
binary_morphism1
definition Type1 : Type2 := Type.
definition Type0 : Type1 := Type.
-definition Type_OF_Type0: Type0 → Type := λx.x.
-definition Type_OF_Type1: Type1 → Type := λx.x.
-definition Type_OF_Type2: Type2 → Type := λx.x.
-definition Type_OF_Type3: Type3 → Type := λx.x.
-coercion Type_OF_Type0.
-coercion Type_OF_Type1.
-coercion Type_OF_Type2.
-coercion Type_OF_Type3.
+definition Type_of_Type0: Type0 → Type := λx.x.
+definition Type_of_Type1: Type1 → Type := λx.x.
+definition Type_of_Type2: Type2 → Type := λx.x.
+definition Type_of_Type3: Type3 → Type := λx.x.
+coercion Type_of_Type0.
+coercion Type_of_Type1.
+coercion Type_of_Type2.
+coercion Type_of_Type3.
definition CProp0 : Type1 := Type0.
definition CProp1 : Type2 := Type1.
definition reflexive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x:A.R x x.
-definition transitive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x,y,z:A.R x y → R y z → R x z.
\ No newline at end of file
+definition transitive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x,y,z:A.R x y → R y z → R x z.
include "basic_topologies.ma".
-definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).
-
-coercion btop_carr.
-
-definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o.
-
-coercion btop_carr'.
definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
intros; constructor 1;
converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
}.
-definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
-
-coercion bt'.
definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
intros; constructor 1;
C2: extS ?? cr T = S
}.
-definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
- λFT1,FT2,c. cr FT1 FT2 c.
-
-coercion cr'.
-
definition formal_map_setoid: formal_topology → formal_topology → setoid1.
intros (S T); constructor 1;
[ apply (formal_map S T);
| simplify; intros 3; apply trans1]]
qed.
-definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
- λFT1,FT2,c.cr ?? c.
-
-coercion cr''.
-
-definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
- λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
-
-coercion cr'''.
-
axiom C1':
∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
- oa_meet_inf: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq p (oa_meet I p_i) = ∀i:I.oa_leq p (p_i i);
+ oa_meet_inf:
+ ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.
+ oa_leq p (oa_meet I p_i) = ∀i:I.oa_leq p (p_i i);
oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq (oa_join I p_i) p = ∀i:I.oa_leq (p_i i) p;
oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
oa_one_top: ∀p:oa_P.oa_leq p oa_one;
interpretation "o-algebra join with explicit function" 'oa_join_mk f =
(fun12 __ (oa_join __) (mk_unary_morphism _ _ f _)).
-definition hint3: OAlgebra → setoid1.
- intro; apply (oa_P o);
-qed.
-coercion hint3.
-
-definition hint4: ∀A. setoid2_OF_OAlgebra A → hint3 A.
- intros; apply t;
-qed.
-coercion hint4.
-
definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
intros; split;
[ intros (p q);
interpretation "o-algebra join with explicit function" 'oa_join_mk f =
(fun12 __ (oa_join __) (mk_unary_morphism _ _ f _)).
-definition hint5: OAlgebra → objs2 SET1.
- intro; apply (oa_P o);
-qed.
-coercion hint5.
-
record ORelation (P,Q : OAlgebra) : Type2 ≝ {
- or_f_ : P ⇒ Q;
- or_f_minus_star_ : P ⇒ Q;
- or_f_star_ : Q ⇒ P;
- or_f_minus_ : Q ⇒ P;
+ or_f_ : carr2 (P ⇒ Q);
+ or_f_minus_star_ : carr2(P ⇒ Q);
+ or_f_star_ : carr2(Q ⇒ P);
+ or_f_minus_ : carr2(Q ⇒ P);
or_prop1_ : ∀p,q. (or_f_ p ≤ q) = (p ≤ or_f_star_ q);
or_prop2_ : ∀p,q. (or_f_minus_ p ≤ q) = (p ≤ or_f_minus_star_ q);
or_prop3_ : ∀p,q. (or_f_ p >< q) = (p >< or_f_minus_ q)
| apply (.= (e3 a)); apply e7;]]]
qed.
+definition ORelation_of_ORelation_setoid :
+ ∀P,Q.ORelation_setoid P Q → ORelation P Q ≝ λP,Q,x.x.
+coercion ORelation_of_ORelation_setoid.
+
definition or_f_minus_star:
∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (P ⇒ Q).
intros; constructor 1;
| intros; cases e; assumption]
qed.
-coercion or_f.
-
definition or_f_minus: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (Q ⇒ P).
intros; constructor 1;
[ apply or_f_minus_;
| intros; cases e; assumption]
qed.
-lemma arrows1_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → (P ⇒ Q).
-intros; apply (or_f ?? t);
-qed.
-
-coercion arrows1_OF_ORelation_setoid.
-
-lemma umorphism_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → unary_morphism1 P Q.
-intros; apply (or_f ?? t);
+lemma arrows1_of_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → (P ⇒ Q).
+intros; apply (or_f ?? c);
qed.
-
-coercion umorphism_OF_ORelation_setoid.
-
-lemma umorphism_setoid_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → unary_morphism1_setoid1 P Q.
-intros; apply (or_f ?? t);
-qed.
-
-coercion umorphism_setoid_OF_ORelation_setoid.
-
-lemma uncurry_arrows : ∀B,C. ORelation_setoid B C → B → C.
-intros; apply (t t1);
-qed.
-
-coercion uncurry_arrows 1.
-
-(*
-lemma hint6: ∀P,Q. Type_OF_setoid2 (hint5 P ⇒ hint5 Q) → unary_morphism1 P Q.
- intros; apply t;
-qed.
-coercion hint6.
-*)
+coercion arrows1_of_ORelation_setoid.
notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
apply or_prop3;
]
| intros; split; simplify;
- [1,3: unfold umorphism_setoid_OF_ORelation_setoid; unfold arrows1_OF_ORelation_setoid; apply ((†e)‡(†e1));
+ [3: unfold arrows1_of_ORelation_setoid;
+ apply ((†e)‡(†e1));
+ |1: apply ((†e)‡(†e1));
|2,4: apply ((†e1)‡(†e));]]
qed.
| intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;]
qed.
-lemma setoid1_of_OA: OA → setoid1.
- intro; apply (oa_P t);
-qed.
-coercion setoid1_of_OA.
-
-lemma SET1_of_OA: OA → SET1.
- intro; whd; apply (setoid1_of_OA t);
-qed.
-coercion SET1_of_OA.
+definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x.
+coercion OAlgebra_of_objs2_OA.
-lemma objs2_SET1_OF_OA: OA → objs2 SET1.
- intro; whd; apply (setoid1_of_OA t);
-qed.
-coercion objs2_SET1_OF_OA.
+definition ORelation_setoid_of_arrows2_OA:
+ ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c.
+coercion ORelation_setoid_of_arrows2_OA.
-lemma Type_OF_category2_OF_SET1_OF_OA: OA → Type_OF_category2 SET1.
- intro; apply (oa_P t);
-qed.
-coercion Type_OF_category2_OF_SET1_OF_OA.
+prefer coercion Type_OF_objs2.
\ No newline at end of file
rel: arrows2 ? concr form
}.
-notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
-notation < "x (⊩ \below c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
-notation < "⊩ \sub c" with precedence 60 for @{'Vdash $c}.
-notation > "⊩ " with precedence 60 for @{'Vdash ?}.
-
interpretation "basic pair relation indexed" 'Vdash2 x y c = (rel c x y).
interpretation "basic pair relation (non applied)" 'Vdash c = (rel c).
alias symbol "eq" = "setoid1 eq".
alias symbol "compose" = "category1 composition".
+(*DIFFER*)
+
+alias symbol "eq" = "setoid2 eq".
+alias symbol "compose" = "category2 composition".
record relation_pair (BP1,BP2: basic_pair): Type2 ≝
{ concr_rel: arrows2 ? (concr BP1) (concr BP2);
form_rel: arrows2 ? (form BP1) (form BP2);
]
qed.
+definition relation_pair_of_relation_pair_setoid:
+ ∀P,Q. relation_pair_setoid P Q → relation_pair P Q ≝ λP,Q,x.x.
+coercion relation_pair_of_relation_pair_setoid.
+
lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
intros 5 (o1 o2 r r' H); change in H with (⊩ ∘ r\sub\c = ⊩ ∘ r'\sub\c);
apply (.= ((commute ?? r) \sup -1));
apply ((id_neutral_left2 ????)‡#);]
qed.
+definition basic_pair_of_objs2_BP: objs2 BP → basic_pair ≝ λx.x.
+coercion basic_pair_of_objs2_BP.
+
+definition relation_pair_setoid_of_arrows2_BP:
+ ∀P,Q.arrows2 BP P Q → relation_pair_setoid P Q ≝ λP,Q,c.c.
+coercion relation_pair_setoid_of_arrows2_BP.
(*
definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
include "o-basic_pairs.ma".
include "o-basic_topologies.ma".
+alias symbol "eq" = "setoid1 eq".
+
(* qui la notazione non va *)
-lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = binary_join ? p q.
+lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = (binary_join ? p q).
intros;
apply oa_leq_antisym;
[ apply oa_density; intros;
qed.
lemma lemma_10_4_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
- intros;
- (* BAD *)
- lapply (†(lemma_10_3_a ?? R p)); [2: apply (R⎻* ); | skip | apply Hletin ]
+ intros; apply (†(lemma_10_3_a ?? R p));
qed.
-(* VEERY BAD! *)
-axiom lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
-(*
- intros;
- (* BAD *)
- lapply (†(lemma_10_3_b ?? R p)); [2: apply rule R; | skip | apply Hletin ]
-qed. *)
+lemma lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
+intros; unfold in ⊢ (? ? ? % %); apply (†(lemma_10_3_b ?? R p));
+qed.
lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
intros; split; intro; apply oa_overlap_sym; assumption.
(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
definition o_basic_topology_of_o_basic_pair: BP → BTop.
- intro;
+ intro t;
constructor 1;
[ apply (form t);
| apply (□_t ∘ Ext⎽t);
definition o_continuous_relation_of_o_relation_pair:
∀BP1,BP2.arrows2 BP BP1 BP2 →
arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
- intros;
+ intros (BP1 BP2 t);
constructor 1;
[ apply (t \sub \f);
| unfold o_basic_topology_of_o_basic_pair; simplify; intros;
apply sym1;
- alias symbol "refl" = "refl1".
- apply (.= †?); [1: apply (t \sub \f (((◊_BP1∘(⊩)* ) U))); |
- lapply (†e); [2: apply rule t \sub \f; | skip | apply Hletin]]
- change in ⊢ (? ? ? % ?) with ((◊_BP2 ∘(⊩)* ) ((t \sub \f ∘ (◊_BP1∘(⊩)* )) U));
- lapply (comp_assoc2 ????? (⊩)* (⊩) t \sub \f);
- apply (.= †(Hletin ?)); clear Hletin;
+ unfold in ⊢ (? ? ? (? ? ? ? %) ?);
+ apply (.= †(†e));
change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
- cut ?;
- [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e3 ^ -1 ((⊩)* U));] | 2,4: skip]
- apply (.= †Hcut);
+ cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
+ cases (commute ?? t); apply (e3 ^ -1 ((⊩)* U));]
+ apply (.= †COM);
change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
- apply (.= Hcut ^ -1);
+ apply (.= COM ^ -1);
change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
- apply (prop11 ?? t \sub \f);
- apply (e ^ -1);
+ change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
+ unfold in ⊢ (? ? ? % %); apply (†e^-1);
| unfold o_basic_topology_of_o_basic_pair; simplify; intros;
apply sym1;
- apply (.= †?); [1: apply (t \sub \f⎻* ((((⊩)⎻* ∘ (⊩)⎻) U))); |
- lapply (†e); [2: apply rule (t \sub \f⎻* ); | skip | apply Hletin]]
- change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘(⊩)⎻ ) ((t \sub \f⎻* ∘ ((⊩)⎻*∘(⊩)⎻ )) U));
- lapply (comp_assoc2 ????? (⊩)⎻ (⊩)⎻* t \sub \f⎻* );
- apply (.= †(Hletin ?)); clear Hletin;
+ unfold in ⊢ (? ? ? (? ? ? ? %) ?);
+ apply (.= †(†e));
change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
- cut ?;
- [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e1 ^ -1 ((⊩)⎻ U));] | 2,4: skip]
- apply (.= †Hcut);
+ cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
+ cases (commute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
+ apply (.= †COM);
change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
- apply (.= Hcut ^ -1);
+ apply (.= COM ^ -1);
change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
- apply (prop11 ?? t \sub \f⎻* );
- apply (e ^ -1); ]
+ change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
+ unfold in ⊢ (? ? ? % %); apply (†e^-1);]
qed.
\ No newline at end of file
-(**************************************************************************)
+ (**************************************************************************)
(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
compatibility: ∀U,V. (A U >< J V) = (U >< J V)
}.
-lemma hint: OA → objs2 OA.
- intro; apply t;
-qed.
-coercion hint.
-
record continuous_relation (S,T: basic_topology) : Type2 ≝
{ cont_rel:> arrows2 OA S T;
(* reduces uses eq1, saturated uses eq!!! *)
intros (S T); constructor 1;
[ apply (continuous_relation S T)
| constructor 1;
- [ (*apply (λr,s:continuous_relation S T.∀b. eq1 (oa_P (carrbt S)) (A ? (r⎻ b)) (A ? (s⎻ b)));*)
- apply (λr,s:continuous_relation S T.r⎻* ∘ (A S) = s⎻* ∘ (A ?));
+ [ alias symbol "eq" = "setoid2 eq".
+ alias symbol "compose" = "category2 composition".
+ apply (λr,s:continuous_relation S T. (r⎻* ) ∘ (A S) = (s⎻* ∘ (A ?)));
| simplify; intros; apply refl2;
| simplify; intros; apply sym2; apply e
| simplify; intros; apply trans2; [2: apply e |3: apply e1; |1: skip]]]
qed.
-definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows2 ? S T ≝ cont_rel.
-
-coercion cont_rel'.
-
-definition cont_rel'':
- ∀S,T: basic_topology.
- carr2 (continuous_relation_setoid S T) → ORelation_setoid (carrbt S) (carrbt T).
- intros; apply rule cont_rel; apply c;
-qed.
-
-coercion cont_rel''.
+definition continuous_relation_of_continuous_relation_setoid:
+ ∀P,Q. continuous_relation_setoid P Q → continuous_relation P Q ≝ λP,Q,c.c.
+coercion continuous_relation_of_continuous_relation_setoid.
(*
theorem continuous_relation_eq':
| intros;
apply sym1;
change in match ((s ∘ r) U) with (s (r U));
- (*<BAD>*) unfold FunClass_1_OF_Type_OF_setoid21;
- unfold objs2_OF_basic_topology1; unfold hint;
- letin reduced := reduced; clearbody reduced;
- unfold uncurry_arrows in reduced ⊢ %; (*</BAD>*)
- apply (.= (reduced : ?)\sup -1);
+ (*<BAD>*) unfold FunClass_1_OF_carr2;
+ apply (.= (reduced : ?)\sup -1);
[ (*BAD*) change with (eq1 ? (r U) (J ? (r U)));
(* BAD U *) apply (.= (reduced ??? U ?)); [ assumption | apply refl1 ]
| apply refl1]
change in e with (a⎻* ∘ A o1 = a'⎻* ∘ A o1);
change in e1 with (b⎻* ∘ A o2 = b'⎻* ∘ A o2);
apply (.= e‡#);
- intro x;
- change with (b⎻* (a'⎻* (A o1 x)) = b'⎻*(a'⎻* (A o1 x)));
- alias symbol "trans" = "trans1".
- alias symbol "prop1" = "prop11".
- alias symbol "invert" = "setoid1 symmetry".
- lapply (.= †(saturated o1 o2 a' (A o1 x) : ?));
- [3: apply (b⎻* ); | 5: apply Hletin; |1,2: skip;
- |apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1); ]
- change in e1 with (∀x.b⎻* (A o2 x) = b'⎻* (A o2 x));
+ intro x;
+ change with (eq1 ? (b⎻* (a'⎻* (A o1 x))) (b'⎻*(a'⎻* (A o1 x))));
+ apply (.= †(saturated o1 o2 a' (A o1 x) ?)); [
+ apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);]
apply (.= (e1 (a'⎻* (A o1 x))));
- alias symbol "invert" = "setoid1 symmetry".
- lapply (†((saturated ?? a' (A o1 x) : ?) ^ -1));
- [2: apply (b'⎻* ); |4: apply Hletin; | skip;
- |apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);]]
+ change with (eq1 ? (b'⎻* (A o2 (a'⎻* (A o1 x)))) (b'⎻*(a'⎻* (A o1 x))));
+ apply (.= †(saturated o1 o2 a' (A o1 x):?)^-1); [
+ apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);]
+ apply rule #;]
| intros; simplify;
change with (((a34⎻* ∘ a23⎻* ) ∘ a12⎻* ) ∘ A o1 = ((a34⎻* ∘ (a23⎻* ∘ a12⎻* )) ∘ A o1));
apply rule (#‡ASSOC ^ -1);
apply (#‡(id_neutral_left2 : ?));]
qed.
-definition btop_carr: BTop → Type1 ≝ λo:BTop. carr1 (oa_P (carrbt o)).
-coercion btop_carr.
+definition basic_topology_of_BTop: objs2 BTop → basic_topology ≝ λx.x.
+coercion basic_topology_of_BTop.
+
+definition continuous_relation_setoid_of_arrows2_BTop :
+ ∀P,Q. arrows2 BTop P Q → continuous_relation_setoid P Q ≝ λP,Q,x.x.
+coercion continuous_relation_setoid_of_arrows2_BTop.
(*
(*CSC: unused! *)
definition A : ∀b:BP. unary_morphism1 (form b) (form b).
intros; constructor 1;
[ apply (λx.□_b (Ext⎽b x));
- | do 2 unfold FunClass_1_OF_Type_OF_setoid21; intros; apply (†(†e));]
+ | intros; apply (†(†e));]
qed.
lemma down_p : ∀S:SET1.∀I:SET.∀u:S⇒S.∀c:arrows2 SET1 I S.∀a:I.∀a':I.a=a'→u (c a)=u (c a').
interpretation "o-concrete space downarrow" 'downarrow x =
(fun11 __ (downarrow _) x).
-definition bp': concrete_space → basic_pair ≝ λc.bp c.
-coercion bp'.
-
-definition bp'': concrete_space → objs2 BP.
- intro; apply (bp' c);
-qed.
-coercion bp''.
-
definition binary_downarrow :
∀C:concrete_space.binary_morphism1 (form C) (form C) (form C).
intros; constructor 1;
-[ intros; apply (↓ t ∧ ↓ t1);
+[ intros; apply (↓ c ∧ ↓ c1);
| intros;
alias symbol "prop2" = "prop21".
alias symbol "prop1" = "prop11".
(Ext⎽CS1 (oa_one (form CS1)))
}.
-definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝
- λCS1,CS2,c. rp CS1 CS2 c.
-coercion rp'.
-
definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid2.
intros;
constructor 1;
| intros 3; apply trans2]]
qed.
-
-definition rp'': ∀CS1,CS2.carr2 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝
- λCS1,CS2,c.rp ?? c.
-coercion rp''.
-
-
-definition rp''': ∀CS1,CS2.Type_OF_setoid21 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝
- λCS1,CS2,c.rp ?? c.
-coercion rp'''.
-
-definition rp'''': ∀CS1,CS2.Type_OF_setoid21 (convergent_relation_space_setoid CS1 CS2) → carr2 (arrows2 BP CS1 CS2) ≝
- λCS1,CS2,c.rp ?? c.
-coercion rp''''.
+definition convergent_relation_space_of_convergent_relation_space_setoid:
+ ∀CS1,CS2.carr2 (convergent_relation_space_setoid CS1 CS2) →
+ convergent_relation_pair CS1 CS2 ≝ λP,Q,c.c.
+coercion convergent_relation_space_of_convergent_relation_space_setoid.
definition convergent_relation_space_composition:
∀o1,o2,o3: concrete_space.
intros; constructor 1;
[ intros; whd in t t1 ⊢ %;
constructor 1;
- [ apply (t1 ∘ t);
+ [ apply (c1 ∘ c);
| intros;
- change in ⊢ (? ? ? % ?) with (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (b↓c))));
- unfold FunClass_1_OF_Type_OF_setoid21;
+ change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (b↓c2))));
alias symbol "trans" = "trans1".
apply (.= († (respects_converges : ?)));
- apply (respects_converges ?? t (t1\sub\f⎻ b) (t1\sub\f⎻ c));
- | change in ⊢ (? ? ? % ?) with (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (oa_one (form o3)))));
- unfold FunClass_1_OF_Type_OF_setoid21;
+ apply (respects_converges ?? c (c1\sub\f⎻ b) (c1\sub\f⎻ c2));
+ | change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (oa_one (form o3)))));
apply (.= (†(respects_all_covered :?)));
- apply rule (respects_all_covered ?? t);]
+ apply rule (respects_all_covered ?? c);]
| intros;
change with (b ∘ a = b' ∘ a');
- change in e with (rp'' ?? a = rp'' ?? a');
- change in e1 with (rp'' ?? b = rp ?? b');
+ change in e with (rp ?? a = rp ?? a');
+ change in e1 with (rp ?? b = rp ?? b');
apply (e‡e1);]
qed.
change with (id2 ? o2 ∘ a = a);
apply (id_neutral_left2 : ?);]
qed.
+
+definition concrete_space_of_CSPA : objs2 CSPA → concrete_space ≝ λx.x.
+coercion concrete_space_of_CSPA.
+
+definition convergent_relation_space_setoid_of_arrows2_CSPA :
+ ∀P,Q. arrows2 CSPA P Q → convergent_relation_space_setoid P Q ≝ λP,Q,x.x.
+coercion convergent_relation_space_setoid_of_arrows2_CSPA.
+
include "o-basic_topologies.ma".
(*
-definition btop_carr': BTop → setoid1 ≝ λo:BTop. carrbt o.
-
-coercion btop_carr'.
-
definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
intros; constructor 1;
[ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
}.
(*
-definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
-
-coercion bt'.
definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
intros; constructor 1;
C2: extS ?? cr T = S
}.
-definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
- λFT1,FT2,c. cr FT1 FT2 c.
-
-coercion cr'.
-
definition formal_map_setoid: formal_topology → formal_topology → setoid1.
intros (S T); constructor 1;
[ apply (formal_map S T);
| simplify; intros 3; apply trans1]]
qed.
-definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
- λFT1,FT2,c.cr ?? c.
-
-coercion cr''.
-
-definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
- λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
-
-coercion cr'''.
-
axiom C1':
∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}.
interpretation "relation applied" 'satisfy r x y = (fun21 ___ (satisfy __ r) x y).
-definition binary_relation_setoid: SET → SET → SET1.
+definition binary_relation_setoid: SET → SET → setoid1.
intros (A B);
constructor 1;
[ apply (binary_relation A B)
assumption]]
qed.
+definition binary_relation_of_binary_relation_setoid :
+ ∀A,B.binary_relation_setoid A B → binary_relation A B ≝ λA,B,c.c.
+coercion binary_relation_of_binary_relation_setoid.
+
definition composition:
∀A,B,C.
binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C).
first [apply refl | assumption]]]
qed.
+(*
+definition setoid_of_REL : objs1 REL → setoid ≝ λx.x.
+coercion setoid_of_REL.
+*)
+
+definition binary_relation_setoid_of_arrow1_REL :
+ ∀P,Q. arrows1 REL P Q → binary_relation_setoid P Q ≝ λP,Q,x.x.
+coercion binary_relation_setoid_of_arrow1_REL.
+
definition full_subset: ∀s:REL. Ω \sup s.
apply (λs.{x | True});
intros; simplify; split; intro; assumption.
coercion full_subset.
-definition setoid1_of_REL: REL → setoid ≝ λS. S.
-coercion setoid1_of_REL.
-
-lemma Type_OF_setoid1_of_REL: ∀o1:Type_OF_category1 REL. Type_OF_objs1 o1 → Type_OF_setoid1 ?(*(setoid1_of_SET o1)*).
- [ apply rule o1;
- | intros; apply t;]
-qed.
-coercion Type_OF_setoid1_of_REL.
-
definition comprehension: ∀b:REL. (unary_morphism1 b CPROP) → Ω \sup b.
apply (λb:REL. λP: b ⇒ CPROP. {x | P x});
intros; simplify;
intros;
constructor 1;
[ constructor 1;
- [ apply (λU.image ?? t U);
+ [ apply (λU.image ?? c U);
| intros; apply (#‡e); ]
| constructor 1;
- [ apply (λU.minus_star_image ?? t U);
+ [ apply (λU.minus_star_image ?? c U);
| intros; apply (#‡e); ]
| constructor 1;
- [ apply (λU.star_image ?? t U);
+ [ apply (λU.star_image ?? c U);
| intros; apply (#‡e); ]
| constructor 1;
- [ apply (λU.minus_image ?? t U);
+ [ apply (λU.minus_image ?? c U);
| intros; apply (#‡e); ]
| intros; split; intro;
- [ change in f with (∀a. a ∈ image ?? t p → a ∈ q);
- change with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
+ [ change in f with (∀a. a ∈ image ?? c p → a ∈ q);
+ change with (∀a:o1. a ∈ p → a ∈ star_image ?? c q);
intros 4; apply f; exists; [apply a] split; assumption;
- | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
- change with (∀a. a ∈ image ?? t p → a ∈ q);
+ | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? c q);
+ change with (∀a. a ∈ image ?? c p → a ∈ q);
intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
| intros; split; intro;
- [ change in f with (∀a. a ∈ minus_image ?? t p → a ∈ q);
- change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
+ [ change in f with (∀a. a ∈ minus_image ?? c p → a ∈ q);
+ change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? c q);
intros 4; apply f; exists; [apply a] split; assumption;
- | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
- change with (∀a. a ∈ minus_image ?? t p → a ∈ q);
+ | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? c q);
+ change with (∀a. a ∈ minus_image ?? c p → a ∈ q);
intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
| intros; split; intro; cases f; clear f;
[ cases x; cases x2; clear x x2; exists; [apply w1]
qed.
lemma orelation_of_relation_preserves_equality:
- ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2. eq1 ? t t' → orelation_of_relation ?? t = orelation_of_relation ?? t'.
+ ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2. t = t' → eq2 ? (orelation_of_relation ?? t) (orelation_of_relation ?? t').
intros; split; unfold orelation_of_relation; simplify; intro; split; intro;
simplify; whd in o1 o2;
[ change with (a1 ∈ minus_star_image ?? t a → a1 ∈ minus_star_image ?? t' a);
apply (. #‡(e‡#)); ]
qed.
-lemma hint: ∀o1,o2:OA. Type_OF_setoid21 (arrows2 ? o1 o2) → carr2 (arrows2 OA o1 o2).
- intros; apply t;
-qed.
-coercion hint.
-
lemma orelation_of_relation_preserves_identity:
- ∀o1:REL. orelation_of_relation ?? (id1 ? o1) = id2 OA (SUBSETS o1).
+ ∀o1:REL. eq2 ? (orelation_of_relation ?? (id1 ? o1)) (id2 OA (SUBSETS o1)).
intros; split; intro; split; whd; intro;
[ change with ((∀x. x ♮(id1 REL o1) a1→x∈a) → a1 ∈ a); intros;
apply (f a1); change with (a1 = a1); apply refl1;
| change with (a1 ∈ a → ∀y.a1 ♮(id1 REL o1) y→y∈a); intros;
change in f1 with (a1 = y); apply (. f1^-1‡#); apply f;]
qed.
-(*
-lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid21 (arrows2 OA S T).
- intros; apply c;
-qed.
-coercion hint2.
-*)
+
(* CSC: ???? forse un uncertain mancato *)
+alias symbol "eq" = "setoid2 eq".
+alias symbol "compose" = "category1 composition".
lemma orelation_of_relation_preserves_composition:
∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3.
orelation_of_relation ?? (G ∘ F) =
split; [ assumption | exists; [apply w] split; assumption ]
| cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ]
split; [ exists; [apply w] split; assumption | assumption ]
- | unfold arrows1_OF_ORelation_setoid;
+ | unfold arrows1_of_ORelation_setoid;
cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ]
split; [ assumption | exists; [apply w] split; assumption ]
- | unfold arrows1_OF_ORelation_setoid in e;
+ | unfold arrows1_of_ORelation_setoid in e;
cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ]
split; [ exists; [apply w] split; assumption | assumption ]
| whd; intros; apply f; exists; [ apply y] split; assumption;
definition o_operator_of_operator:
∀C:REL. (Ω \sup C => Ω \sup C) → (SUBSETS C ⇒ SUBSETS C).
- intros;apply t;
+ intros (C t);apply t;
qed.
definition is_o_saturation_of_is_saturation:
∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
intros; constructor 1;
[ intro; whd; whd in I;
- apply ({x | ∀i:I. x ∈ t i});
+ apply ({x | ∀i:I. x ∈ c i});
simplify; intros; split; intros; [ apply (. (e^-1‡#)); | apply (. e‡#); ]
apply f;
| intros; split; intros 2; simplify in f ⊢ %; intro;
∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
intros; constructor 1;
[ intro; whd; whd in A; whd in I;
- apply ({x | ∃i:I. x ∈ t i });
+ apply ({x | ∃i:I. x ∈ c i });
simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
[ apply (. (e^-1‡#)); | apply (. (e‡#)); ]
apply x;
projects / helm.git / commitdiff