definition F_comp :
∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀o1,o2,o3.
- binary_morphism2 (Fm ?? F o1 o2) (Fm ?? F o2 o3) (Fm ?? F o1 o3).
+ (Fm ?? F o1 o2) × (Fm ?? F o2 o3) ⇒_2 (Fm ?? F o1 o3).
intros; constructor 1;
[ intros (f g); constructor 1;
[ apply (comp2 C2 ??? (ℳ_2 f) (ℳ_2 g));
lapply (FmP ????? a) as H1; lapply (FmP ????? a') as H2;
cut (REW ????? (map_arrows2 ?? F ?? (ℳ_1 a)) =
REW ????? (map_arrows2 ?? F ?? (ℳ_1 a')));[2:
- apply (.= H1); apply (.= e); apply H2^-1;]
+ apply (.= H1); apply (.= e); apply (H2^-1);]
clear H1 H2 e; cases S in a a' Hcut; cases T;
cases H; cases H1; simplify; intros; assumption;]
| intro; apply rule #;
∀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).
+definition BPext: ∀o: BP. (form o) ⇒_1 Ω^(concr o).
intros; constructor 1;
[ apply (ext ? ? (rel o));
| intros;
apply refl1]
qed.
-definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o).
+definition BPextS: ∀o: BP. Ω^(form o) ⇒_1 Ω^(concr o).
intros; constructor 1;
[ apply (minus_image ?? (rel o));
| intros; apply (#‡e); ]
qed.
-definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
+definition fintersects: ∀o: BP. (form o) × (form o) ⇒_1 Ω^(form o).
intros (o); constructor 1;
[ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
intros; simplify; apply (.= (†e)‡#); apply refl1
interpretation "fintersects" 'fintersects U V = (fun21 ??? (fintersects ?) U V).
definition fintersectsS:
- ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
+ ∀o:BP. Ω^(form o) × Ω^(form o) ⇒_1 Ω^(form o).
intros (o); constructor 1;
- [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
+ [ apply (λo: basic_pair.λa,b: Ω^(form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
intros; simplify; apply (.= (†e)‡#); apply refl1
| intros; split; simplify; intros;
[ apply (. #‡((†e^-1)‡(†e1^-1))); assumption
interpretation "fintersectsS" 'fintersects U V = (fun21 ??? (fintersectsS ?) U V).
-definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
+definition relS: ∀o: BP. (concr o) × Ω^(form o) ⇒_1 CPROP.
intros (o); constructor 1;
- [ apply (λx:concr o.λS: Ω \sup (form o).∃y:form o.y ∈ S ∧ x ⊩⎽o y);
+ [ apply (λx:concr o.λS: Ω^(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]]
record basic_topology: Type1 ≝
{ carrbt:> REL;
- A: unary_morphism1 (Ω \sup carrbt) (Ω \sup carrbt);
- J: unary_morphism1 (Ω \sup carrbt) (Ω \sup carrbt);
+ A: Ω^carrbt ⇒_1 Ω^carrbt;
+ J: Ω^carrbt ⇒_1 Ω^carrbt;
A_is_saturation: is_saturation ? A;
J_is_reduction: is_reduction ? J;
- compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V)
+ compatibility: ∀U,V. (A U ≬ J V) =_1 (U ≬ J V)
}.
record continuous_relation (S,T: basic_topology) : Type1 ≝
eq3: equivalence_relation3 carr3
}.
-
interpretation "setoid3 eq" 'eq t x y = (eq_rel3 ? (eq3 t) x y).
interpretation "setoid2 eq" 'eq t x y = (eq_rel2 ? (eq2 t) x y).
interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
∀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).
+notation > "A × term 74 B ⇒_1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}.
+notation > "A × term 74 B ⇒_2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}.
+notation > "A × term 74 B ⇒_3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
+notation > "B ⇒_1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
+notation > "B ⇒_1. C" right associative with precedence 72 for @{'arrows1_SETlow $B $C}.
+notation > "B ⇒_2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
+notation > "B ⇒_2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}.
+
+notation "A × term 74 B ⇒\sub 1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}.
+notation "A × term 74 B ⇒\sub 2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}.
+notation "A × term 74 B ⇒\sub 3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
+notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
+notation "B ⇒\sub 2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
+
+interpretation "'binary_morphism1" 'binary_morphism1 A B C = (binary_morphism1 A B C).
+interpretation "'binary_morphism2" 'binary_morphism2 A B C = (binary_morphism2 A B C).
+interpretation "'binary_morphism3" 'binary_morphism3 A B C = (binary_morphism3 A B C).
+interpretation "'arrows1_SET low" 'arrows1_SET A B = (unary_morphism1 A B).
+interpretation "'arrows1_SETlow" 'arrows1_SETlow A B = (unary_morphism1 A B).
+interpretation "'arrows1_SET" 'arrows1_SET A B = (arrows1 SET A B).
definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
intros;
]
qed.
+interpretation "'arrows2_SET1 low" 'arrows2_SET1 A B = (unary_morphism2 A B).
+interpretation "'arrows2_SET1low" 'arrows2_SET1low A B = (unary_morphism2 A B).
+interpretation "'arrows2_SET1" 'arrows2_SET1 A B = (arrows2 SET1 A B).
+
definition setoid1_of_SET1: objs2 SET1 → setoid1 ≝ λx.x.
coercion setoid1_of_SET1.
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).
include "o-concrete_spaces.ma".
include "basic_pairs_to_o-basic_pairs.ma".
+(*
(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
definition o_concrete_space_of_concrete_space: cic:/matita/formal_topology/concrete_spaces/concrete_space.ind#xpointer(1/1) → concrete_space.
intro;
apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r)));
apply (orelation_of_relation_preserves_composition ?? (form BP2) (rel BP1) ?); ]
qed.
+
+*)
\ No newline at end of file
-basic_pairs_to_basic_topologies.ma basic_pairs.ma basic_pairs_to_o-basic_pairs.ma basic_topologies.ma o-basic_pairs_to_o-basic_topologies.ma
o-basic_pairs.ma notation.ma o-algebra.ma
+basic_pairs_to_basic_topologies.ma basic_pairs.ma basic_pairs_to_o-basic_pairs.ma basic_topologies.ma o-basic_pairs_to_o-basic_topologies.ma
o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma
-basic_pairs.ma notation.ma relations.ma
-saturations.ma relations.ma
o-saturations.ma o-algebra.ma
-o-algebra.ma categories.ma
-categories.ma cprop_connectives.ma
+saturations.ma relations.ma
+basic_pairs.ma notation.ma relations.ma
formal_topologies.ma basic_topologies.ma
o-formal_topologies.ma o-basic_topologies.ma
+o-algebra.ma categories.ma
+categories.ma cprop_connectives.ma
saturations_to_o-saturations.ma o-saturations.ma relations_to_o-algebra.ma saturations.ma
+subsets.ma categories.ma
basic_topologies.ma relations.ma saturations.ma
concrete_spaces.ma basic_pairs.ma
-subsets.ma categories.ma
relations.ma subsets.ma
r-o-basic_pairs.ma apply_functor.ma basic_pairs_to_o-basic_pairs.ma o-basic_pairs_to_o-basic_topologies.ma
concrete_spaces_to_o-concrete_spaces.ma basic_pairs_to_o-basic_pairs.ma concrete_spaces.ma o-concrete_spaces.ma
o-basic_topologies.ma o-algebra.ma o-saturations.ma
+basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma
notation.ma
basic_topologies_to_o-basic_topologies.ma basic_topologies.ma o-basic_topologies.ma relations_to_o-algebra.ma
-basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma
-apply_functor.ma categories.ma notation.ma
cprop_connectives.ma logic/connectives.ma
-o-basic_pairs_to_o-basic_topologies.ma notation.ma o-basic_pairs.ma o-basic_topologies.ma
+apply_functor.ma categories.ma notation.ma
relations_to_o-algebra.ma o-algebra.ma relations.ma
+o-basic_pairs_to_o-basic_topologies.ma notation.ma o-basic_pairs.ma o-basic_topologies.ma
logic/connectives.ma
include "basic_topologies.ma".
-
+(*
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)});
apply prop1; assumption]
qed.
+*)
\ No newline at end of file
(* USARE L'ESISTENZIALE DEBOLE *)
-notation > "A × B ⇉2,1 C" non associative with precedence 70 for @{binary_morphism1 $A $B $C}.
-notation > "A × B ⇉2,2 C" non associative with precedence 70 for @{binary_morphism2 $A $B $C}.
-notation > "B ⇉1,1 C" non associative with precedence 80 for @{arrows1 SET $B $C}.
-notation > "B ⇉1,2 C" non associative with precedence 80 for @{unary_morphism2 $B $C}.
notation > "hvbox(a break ≤ b)" non associative with precedence 45 for @{oa_leq $a $b}.
notation > "a >< b" non associative with precedence 45 for @{oa_overlap $a $b}.
notation > "⋁ p" non associative with precedence 45 for @{oa_join ? $p}.
notation > "⋀ p" non associative with precedence 45 for @{oa_meet ? $p}.
+notation > "𝟙" non associative with precedence 90 for @{oa_one}.
+notation > "𝟘" non associative with precedence 90 for @{oa_zero}.
record OAlgebra : Type2 := {
oa_P :> SET1;
- oa_leq : oa_P Ã\97 oa_P â\87\892,1 CPROP;
- oa_overlap: oa_P Ã\97 oa_P â\87\892,1 CPROP;
- oa_meet: ∀I:SET.(I ⇒ oa_P) ⇉1,2 oa_P;
- oa_join: ∀I:SET.(I ⇒ oa_P) ⇉1,2 oa_P;
+ oa_leq : oa_P Ã\97 oa_P â\87\92_1 CPROP;
+ oa_overlap: oa_P Ã\97 oa_P â\87\92_1 CPROP;
+ oa_meet: ∀I:SET.(I ⇒_2 oa_P) ⇒_2. oa_P;
+ oa_join: ∀I:SET.(I ⇒_2 oa_P) ⇒_2. oa_P;
oa_one: oa_P;
oa_zero: oa_P;
oa_leq_refl: ∀a:oa_P. a ≤ a;
oa_leq_antisym: ∀a,b:oa_P.a ≤ b → b ≤ a → a = b;
oa_leq_trans: ∀a,b,c:oa_P.a ≤ b → b ≤ c → a ≤ c;
oa_overlap_sym: ∀a,b:oa_P.a >< b → b >< a;
- oa_meet_inf: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.p ≤ (⋀ p_i) = (∀i:I.p ≤ (p_i i));
- oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.(⋁ p_i) ≤ p = (∀i:I.p_i i ≤ p);
- oa_zero_bot: ∀p:oa_P.oa_zero ≤ p;
- oa_one_top: ∀p:oa_P.p ≤ oa_one;
- oa_overlap_preserves_meet_:
- ∀p,q:oa_P.p >< q →
+ oa_meet_inf: ∀I:SET.∀p_i:I ⇒_2 oa_P.∀p:oa_P.p ≤ (⋀ p_i) = (∀i:I.p ≤ (p_i i));
+ oa_join_sup: ∀I:SET.∀p_i:I ⇒_2 oa_P.∀p:oa_P.(⋁ p_i) ≤ p = (∀i:I.p_i i ≤ p);
+ oa_zero_bot: ∀p:oa_P.𝟘 ≤ p;
+ oa_one_top: ∀p:oa_P.p ≤ 𝟙;
+ oa_overlap_preserves_meet_: ∀p,q:oa_P.p >< q →
p >< (⋀ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q });
- oa_join_split: ∀I:SET.∀p.∀q:I ⇒ oa_P.p >< (⋁ q) = (∃i:I.p >< (q i));
+ oa_join_split: ∀I:SET.∀p.∀q:I ⇒_2 oa_P.p >< (⋁ q) = (∃i:I.p >< (q i));
(*oa_base : setoid;
1) enum non e' il nome giusto perche' non e' suriettiva
2) manca (vedere altro capitolo) la "suriettivita'" come immagine di insiemi di oa_base
interpretation "o-algebra join with explicit function" 'oa_join_mk f =
(fun12 ?? (oa_join ??) (mk_unary_morphism ?? f ?)).
-definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
+definition binary_meet : ∀O:OAlgebra. O × O ⇒_1 O.
intros; split;
[ intros (p q);
apply (∧ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
prefer coercion Type1_OF_OAlgebra.
-definition binary_join : ∀O:OAlgebra. binary_morphism1 O O O.
+definition binary_join : ∀O:OAlgebra. O × O ⇒_1 O.
intros; split;
[ intros (p q);
apply (∨ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
(fun12 ?? (oa_join ??) (mk_unary_morphism ?? f ?)).
record ORelation (P,Q : OAlgebra) : Type2 ≝ {
- 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_f_ : carr2 (P ⇒_2 Q);
+ or_f_minus_star_ : carr2(P ⇒_2 Q);
+ or_f_star_ : carr2(Q ⇒_2 P);
+ or_f_minus_ : carr2(Q ⇒_2 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)
coercion ORelation_of_ORelation_setoid.
definition or_f_minus_star:
- ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (P ⇒ Q).
+ ∀P,Q:OAlgebra.(ORelation_setoid P Q) ⇒_2 (P ⇒_2 Q).
intros; constructor 1;
[ apply or_f_minus_star_;
| intros; cases e; assumption]
qed.
-definition or_f: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (P ⇒ Q).
+definition or_f: ∀P,Q:OAlgebra.(ORelation_setoid P Q) ⇒_2 (P ⇒_2 Q).
intros; constructor 1;
[ apply or_f_;
| intros; cases e; assumption]
qed.
-definition or_f_minus: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (Q ⇒ P).
+definition or_f_minus: ∀P,Q:OAlgebra.(ORelation_setoid P Q) ⇒_2 (Q ⇒_2 P).
intros; constructor 1;
[ apply or_f_minus_;
| intros; cases e; assumption]
qed.
-definition or_f_star: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (Q ⇒ P).
+definition or_f_star: ∀P,Q:OAlgebra.(ORelation_setoid P Q) ⇒_2 (Q ⇒_2 P).
intros; constructor 1;
[ apply or_f_star_;
| intros; cases e; assumption]
qed.
-lemma arrows1_of_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → (P ⇒ Q).
+lemma arrows1_of_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → (P ⇒_2 Q).
intros; apply (or_f ?? c);
qed.
coercion arrows1_of_ORelation_setoid.
lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
intros; split; intro; apply oa_overlap_sym; assumption.
-qed.
\ No newline at end of file
+qed.
record Obasic_topology: Type2 ≝
{ Ocarrbt:> OA;
- oA: Ocarrbt ⇒ Ocarrbt;
- oJ: Ocarrbt ⇒ Ocarrbt;
+ oA: Ocarrbt ⇒_2 Ocarrbt;
+ oJ: Ocarrbt ⇒_2 Ocarrbt;
oA_is_saturation: is_o_saturation ? oA;
oJ_is_reduction: is_o_reduction ? oJ;
- Ocompatibility: ∀U,V. (oA U >< oJ V) = (U >< oJ V)
+ Ocompatibility: ∀U,V. (oA U >< oJ V) =_1 (U >< oJ V)
}.
record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝
change in e1 with (b⎻* ∘ oA o2 = b'⎻* ∘ oA o2);
apply (.= e‡#);
intro x;
- change with (eq1 ? (b⎻* (a'⎻* (oA o1 x))) (b'⎻*(a'⎻* (oA o1 x))));
+ change with (b⎻* (a'⎻* (oA o1 x)) =_1 b'⎻*(a'⎻* (oA o1 x)));
apply (.= †(Osaturated o1 o2 a' (oA o1 x) ?)); [
apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
apply (.= (e1 (a'⎻* (oA o1 x))));
- change with (eq1 ? (b'⎻* (oA o2 (a'⎻* (oA o1 x)))) (b'⎻*(a'⎻* (oA o1 x))));
+ change with (b'⎻* (oA o2 (a'⎻* (oA o1 x))) =_1 b'⎻*(a'⎻* (oA o1 x)));
apply (.= †(Osaturated o1 o2 a' (oA o1 x):?)^-1); [
apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
apply rule #;]
| 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').
+lemma down_p : ∀S:SET1.∀I:SET.∀u:S ⇒_1 S.∀c:arrows2 SET1 I S.∀a:I.∀a':I.a =_1 a'→u (c a) =_1 u (c a').
intros; apply (†(†e));
qed.
include "o-basic_topologies.ma".
+(*
(*
definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
intros; constructor 1;
change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
apply prop1; assumption]
qed.
-
+*)
clear Hletin Hletin1; cases Hletin2; whd in x2;
qed.
*)
-lemma curry: ∀A,B,C.binary_morphism1 A B C → A → B ⇒ C.
+lemma curry: ∀A,B,C.(A × B ⇒_1 C) → A → (B ⇒_1 C).
intros;
constructor 1;
[ apply (b c);
notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
-definition preserve_sup : ∀S,T.∀ f:Ω \sup S ⇒ Ω \sup T. CProp1.
-intros (S T f); apply (∀X:Ω \sup S. (f X) = ?);
+definition preserve_sup : ∀S,T.∀ f:Ω^S ⇒_1 Ω^T. CProp1.
+intros (S T f); apply (∀X:Ω \sup S. (f X) =_1 ?);
constructor 1; constructor 1;
[ intro y; alias symbol "singl" = "singleton". alias symbol "and" = "and_morphism".
apply (∃x:S. x ∈ X ∧ y ∈ f {(x)});
definition composition:
∀A,B,C.
- binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C).
+ (binary_relation_setoid A B) × (binary_relation_setoid B C) ⇒_1 (binary_relation_setoid A C).
intros;
constructor 1;
[ intros (R12 R23);
∀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.
+definition full_subset: ∀s:REL. Ω^s.
apply (λs.{x | True});
intros; simplify; split; intro; assumption.
qed.
coercion full_subset.
-definition comprehension: ∀b:REL. (unary_morphism1 b CPROP) → Ω \sup b.
- apply (λb:REL. λP: b ⇒ CPROP. {x | P x});
+alias symbol "arrows1_SET" (instance 2) = "'arrows1_SET low".
+definition comprehension: ∀b:REL. (b ⇒_1 CPROP) → Ω^b.
+ apply (λb:REL. λP: b ⇒_1 CPROP. {x | P x});
intros; simplify;
- alias symbol "trans" = "trans1".
- alias symbol "prop1" = "prop11".
apply (.= †e); apply refl1.
qed.
interpretation "subset comprehension" 'comprehension s p =
(comprehension s (mk_unary_morphism1 ?? p ?)).
-definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
+definition ext: ∀X,S:REL. (arrows1 ? X S) × S ⇒_1 (Ω^X).
apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 REL X S.λf:S.{x ∈ X | x ♮r f}) ?);
[ intros; simplify; apply (.= (e‡#)); apply refl1
| intros; simplify; split; intros; simplify;
*)
(* the same as ⋄ for a basic pair *)
-definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
+definition image: ∀U,V:REL. (arrows1 ? U V) × Ω^U ⇒_1 Ω^V.
intros; constructor 1;
[ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S });
intros; simplify; split; intro; cases e1; exists [1,3: apply w]
qed.
(* the same as □ for a basic pair *)
-definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
+definition minus_star_image: ∀U,V:REL. (arrows1 ? U V) × Ω^U ⇒_1 Ω^V.
intros; constructor 1;
[ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S});
intros; simplify; split; intros; apply f;
qed.
(* the same as Rest for a basic pair *)
-definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
+definition star_image: ∀U,V:REL. (arrows1 ? U V) × Ω^V ⇒_1 Ω^U.
intros; constructor 1;
[ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | ∀y:V. x ♮r y → y ∈ S});
intros; simplify; split; intros; apply f;
qed.
(* the same as Ext for a basic pair *)
-definition minus_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
+definition minus_image: ∀U,V:REL. (arrows1 ? U V) × Ω^V ⇒_1 Ω^U.
intros; constructor 1;
[ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | (*∃x:U. x ♮r y ∧ x ∈ S*)
exT ? (λy:V.x ♮r y ∧ y ∈ S) });
definition POW': objs1 SET → OAlgebra.
intro A; constructor 1;
- [ apply (Ω \sup A);
+ [ apply (Ω^A);
| apply subseteq;
| apply overlaps;
| apply big_intersects;
assumption]]
qed.
-definition powerset_of_POW': ∀A.oa_P (POW' A) → Ω \sup A ≝ λA,x.x.
+definition powerset_of_POW': ∀A.oa_P (POW' A) → Ω^A ≝ λA,x.x.
coercion powerset_of_POW'.
definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA (POW' o1) (POW' o2).
qed.
lemma orelation_of_relation_preserves_equality:
- ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2. t = t' → eq2 ? (orelation_of_relation ?? t) (orelation_of_relation ?? t').
+ ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2.
+ t = t' → orelation_of_relation ?? t =_2 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);
qed.
lemma orelation_of_relation_preserves_identity:
- ∀o1:REL. eq2 ? (orelation_of_relation ?? (id1 ? o1)) (id2 OA (POW' o1)).
+ ∀o1:REL. orelation_of_relation ?? (id1 ? o1) =_2 id2 OA (POW' 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;
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) =
- comp2 OA (POW' o1) (POW' o2) (POW' o3)
- ?? (*(orelation_of_relation ?? F) (orelation_of_relation ?? G)*).
- [ apply (orelation_of_relation ?? F); | apply (orelation_of_relation ?? G); ]
+ orelation_of_relation ?? (G ∘ F) =
+ comp2 OA ??? (orelation_of_relation ?? F) (orelation_of_relation ?? G).
intros; split; intro; split; whd; intro; whd in ⊢ (% → %); intros;
[ whd; intros; apply f; exists; [ apply x] split; assumption;
| cases f1; clear f1; cases x1; clear x1; apply (f w); assumption;
theorem POW_faithful:
∀S,T.∀f,g:arrows2 (category2_of_category1 REL) S T.
- map_arrows2 ?? POW ?? f = map_arrows2 ?? POW ?? g → f=g.
+ map_arrows2 ?? POW ?? f = map_arrows2 ?? POW ?? g → f = g.
intros; unfold POW in e; simplify in e; cases e;
unfold orelation_of_relation in e3; simplify in e3; clear e e1 e2 e4;
intros 2; cases (e3 {(x)});
qed.
-lemma currify: ∀A,B,C. binary_morphism1 A B C → A → unary_morphism1 B C.
+lemma currify: ∀A,B,C. (A × B ⇒_1 C) → A → (B ⇒_1 C).
intros; constructor 1; [ apply (b c); | intros; apply (#‡e);]
qed.
(*
-alias symbol "singl" = "singleton".
-alias symbol "eq" = "setoid eq".
-lemma in_singleton_to_eq : ∀A:setoid.∀y,x:A.y ∈ {(x)} → (eq1 A) y x.
-intros; apply sym1; apply f;
-qed.
-
-lemma eq_to_in_singleton : ∀A:setoid.∀y,x:A.eq1 A y x → y ∈ {(x)}.
-intros; apply (e^-1);
-qed.
-*)
-
interpretation "lifting singl" 'singl x =
(fun11 ? (objs2 (POW ?)) (singleton ?) x).
+*)
+
theorem POW_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? POW S T g = f).
intros; exists;
lapply (#‡prop11 ?? f ?? (†e)); [6: apply Hletin; |*:skip ]]
| whd; split; whd; intro; simplify; unfold map_arrows2; simplify;
[ split;
- [ change with (∀a1.(∀x. a1 ∈ f (singleton S x) → x ∈ a) → a1 ∈ f⎻* a);
- | change with (∀a1.a1 ∈ f⎻* a → (∀x.a1 ∈ f (singleton S x) → x ∈ a)); ]
+ [ change with (∀a1.(∀x. a1 ∈ (f {(x):S}) → x ∈ a) → a1 ∈ f⎻* a);
+ | change with (∀a1.a1 ∈ f⎻* a → (∀x.a1 ∈ f {(x):S} → x ∈ a)); ]
| split;
- [ change with (∀a1.(∃y:carr T. y ∈ f (singleton S a1) ∧ y ∈ a) → a1 ∈ f⎻ a);
- | change with (∀a1.a1 ∈ f⎻ a → (∃y:carr T.y ∈ f (singleton S a1) ∧ y ∈ a)); ]
+ [ change with (∀a1.(∃y:carr T. y ∈ f {(a1):S} ∧ y ∈ a) → a1 ∈ f⎻ a);
+ | change with (∀a1.a1 ∈ f⎻ a → (∃y:carr T.y ∈ f {(a1):S} ∧ y ∈ a)); ]
| split;
- [ change with (∀a1.(∃x:carr S. a1 ∈ f (singleton S x) ∧ x ∈ a) → a1 ∈ f a);
- | change with (∀a1.a1 ∈ f a → (∃x:carr S. a1 ∈ f (singleton S x) ∧ x ∈ a)); ]
+ [ change with (∀a1.(∃x:carr S. a1 ∈ f {(x):S} ∧ x ∈ a) → a1 ∈ f a);
+ | change with (∀a1.a1 ∈. f a → (∃x:carr S. a1 ∈ f {(x):S} ∧ x ∈ a)); ]
| split;
- [ change with (∀a1.(∀y. y ∈ f (singleton S a1) → y ∈ a) → a1 ∈ f* a);
- | change with (∀a1.a1 ∈ f* a → (∀y. y ∈ f (singleton S a1) → y ∈ a)); ]]
+ [ change with (∀a1.(∀y. y ∈ f {(a1):S} → y ∈ a) → a1 ∈ f* a);
+ | change with (∀a1.a1 ∈ f* a → (∀y. y ∈ f {(a1):S} → y ∈ a)); ]]
[ intros; apply ((. (or_prop2 ?? f (singleton ? a1) a)^-1) ? a1);
[ intros 2; apply (f1 a2); change in f2 with (a2 ∈ f⎻ (singleton ? a1));
lapply (. (or_prop3 ?? f (singleton ? a2) (singleton ? a1)));
include "relations.ma".
-definition is_saturation: ∀C:REL. unary_morphism1 (Ω \sup C) (Ω \sup C) → CProp1 ≝
- λC:REL.λA:unary_morphism1 (Ω \sup C) (Ω \sup C).
- ∀U,V. (U ⊆ A V) = (A U ⊆ A V).
+definition is_saturation: ∀C:REL. Ω^C ⇒_1 Ω^C → CProp1 ≝
+ λC:REL.λA:Ω^C ⇒_1 Ω^C. ∀U,V. (U ⊆ A V) =_1 (A U ⊆ A V).
-definition is_reduction: ∀C:REL. unary_morphism1 (Ω \sup C) (Ω \sup C) → CProp1 ≝
- λC:REL.λJ:unary_morphism1 (Ω \sup C) (Ω \sup C).
- ∀U,V. (J U ⊆ V) = (J U ⊆ J V).
+definition is_reduction: ∀C:REL. Ω^C ⇒_1 Ω^C → CProp1 ≝
+ λC:REL.λJ: Ω^C ⇒_1 Ω^C. ∀U,V. (J U ⊆ V) =_1 (J U ⊆ J V).
theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ⊆ A U.
intros; apply (fi ?? (i ??)); apply subseteq_refl.
(* These are only conversions :-) *)
-definition o_operator_of_operator:
- ∀C:REL. (Ω \sup C => Ω \sup C) → (POW C ⇒ POW C).
+definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)).
intros (C t);apply t;
qed.
-definition is_o_saturation_of_is_saturation:
- ∀C:REL.∀R: unary_morphism1 (Ω \sup C) (Ω \sup C).
+definition is_o_saturation_of_is_saturation: ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.
is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
intros; apply i;
qed.
-definition is_o_reduction_of_is_reduction:
- ∀C:REL.∀R: unary_morphism1 (Ω \sup C) (Ω \sup C).
+definition is_o_reduction_of_is_reduction: ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.
is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R).
intros; apply i;
qed.
\ No newline at end of file
include "categories.ma".
-record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: unary_morphism1 A CPROP }.
+record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: A ⇒_1 CPROP }.
+interpretation "powerset low" 'powerset A = (powerset_carrier A).
+notation "hvbox(a break ∈. b)" non associative with precedence 45 for @{ 'mem_low $a $b }.
+interpretation "memlow" 'mem_low a S = (mem_operator ? S a).
-definition subseteq_operator: ∀A: SET. powerset_carrier A → powerset_carrier A → CProp0 ≝
- λA:objs1 SET.λU,V.∀a:A. mem_operator ? U a → mem_operator ? V a.
+definition subseteq_operator: ∀A: objs1 SET. Ω^A → Ω^A → CProp0 ≝
+ λA:objs1 SET.λU,V.∀a:A. a ∈. U → a ∈. V.
theorem transitive_subseteq_operator: ∀A. transitive2 ? (subseteq_operator A).
intros 6; intros 2;
interpretation "subset construction" 'subset \eta.x =
(mk_powerset_carrier ? (mk_unary_morphism1 ? CPROP x ?)).
-definition mem: ∀A. binary_morphism1 A (Ω \sup A) CPROP.
+definition mem: ∀A. A × Ω^A ⇒_1 CPROP.
intros;
constructor 1;
[ apply (λx,S. mem_operator ? S x)
interpretation "mem" 'mem a S = (fun21 ??? (mem ?) a S).
-definition subseteq: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
+definition subseteq: ∀A. Ω^A × Ω^A ⇒_1 CPROP.
intros;
constructor 1;
[ apply (λU,V. subseteq_operator ? U V)
interpretation "subseteq" 'subseteq U V = (fun21 ??? (subseteq ?) U V).
-
-
-theorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S.
+theorem subseteq_refl: ∀A.∀S:Ω^A.S ⊆ S.
intros 4; assumption.
qed.
-theorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
+theorem subseteq_trans: ∀A.∀S1,S2,S3: Ω^A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
intros; apply transitive_subseteq_operator; [apply S2] assumption.
qed.
-definition overlaps: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
+definition overlaps: ∀A. Ω^A × Ω^A ⇒_1 CPROP.
intros;
constructor 1;
- (* Se metto x al posto di ? ottengo una universe inconsistency *)
- [ apply (λA:objs1 SET.λU,V:Ω \sup A.(exT2 ? (λx:A.?(*x*) ∈ U) (λx:A.?(*x*) ∈ V) : CProp0))
+ [ apply (λA:objs1 SET.λU,V:Ω^A.(exT2 ? (λx:A.x ∈ U) (λx:A.x ∈ V) : CProp0))
| intros;
constructor 1; intro; cases e2; exists; [1,4: apply w]
[ apply (. #‡e^-1); assumption
interpretation "overlaps" 'overlaps U V = (fun21 ??? (overlaps ?) U V).
-definition intersects:
- ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) (Ω \sup A).
+definition intersects: ∀A. Ω^A × Ω^A ⇒_1 Ω^A.
intros;
constructor 1;
[ apply rule (λU,V. {x | x ∈ U ∧ x ∈ V });
interpretation "intersects" 'intersects U V = (fun21 ??? (intersects ?) U V).
-definition union:
- ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) (Ω \sup A).
+definition union: ∀A. Ω^A × Ω^A ⇒_1 Ω^A.
intros;
constructor 1;
[ apply (λU,V. {x | x ∈ U ∨ x ∈ V });
interpretation "union" 'union U V = (fun21 ??? (union ?) U V).
(* qua non riesco a mettere set *)
-definition singleton: ∀A:setoid. unary_morphism1 A (Ω \sup A).
+definition singleton: ∀A:setoid. A ⇒_1 Ω^A.
intros; constructor 1;
[ apply (λa:A.{b | a =_0 b}); unfold setoid1_of_setoid; simplify;
intros; simplify;
qed.
interpretation "singleton" 'singl a = (fun11 ?? (singleton ?) a).
+notation > "{ term 19 a : S }" with precedence 90 for @{fun11 ?? (singleton $S) $a}.
-definition big_intersects:
- ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
+definition big_intersects: ∀A:SET.∀I:SET.(I ⇒_2 Ω^A) ⇒_2 Ω^A.
intros; constructor 1;
[ intro; whd; whd in I;
apply ({x | ∀i:I. x ∈ c i});
| apply (. (#‡e i)); apply f]]
qed.
-definition big_union:
- ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
+definition big_union: ∀A:SET.∀I:SET.(I ⇒_2 Ω^A) ⇒_2 Ω^A.
intros; constructor 1;
[ intro; whd; whd in A; whd in I;
apply ({x | ∃i:I. x ∈ c i });
projects / helm.git / commitdiff