(**************************************************************************)
include "relations.ma".
+include "notation.ma".
record basic_pair: Type1 ≝
{ concr: REL;
commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩
}.
-notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}.
-notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}.
interpretation "concrete relation" 'concr_rel r = (concr_rel __ r).
interpretation "formal relation" 'form_rel r = (form_rel __ r).
include "relations_to_o-algebra.ma".
(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
-definition o_basic_pair_of_basic_pair: cic:/matita/formal_topology/basic_pairs/basic_pair.ind#xpointer(1/1) → basic_pair.
- intro;
+definition o_basic_pair_of_basic_pair: basic_pair → Obasic_pair.
+ intro b;
constructor 1;
- [ apply (SUBSETS (concr b));
- | apply (SUBSETS (form b));
- | apply (orelation_of_relation ?? (rel b)); ]
+ [ apply (map_objs2 ?? SUBSETS' (concr b));
+ | apply (map_objs2 ?? SUBSETS' (form b));
+ | apply (map_arrows2 ?? SUBSETS' (concr b) (form b) (rel b)); ]
qed.
definition o_relation_pair_of_relation_pair:
- ∀BP1,BP2.cic:/matita/formal_topology/basic_pairs/relation_pair.ind#xpointer(1/1) BP1 BP2 →
- relation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2).
+ ∀BP1,BP2. relation_pair BP1 BP2 →
+ Orelation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2).
intros;
constructor 1;
- [ apply (orelation_of_relation ?? (r \sub \c));
- | apply (orelation_of_relation ?? (r \sub \f));
- | lapply (commute ?? r);
- lapply (orelation_of_relation_preserves_equality ???? Hletin);
- apply (.= (orelation_of_relation_preserves_composition (concr BP1) ??? (rel BP2)) ^ -1);
- apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r)));
- apply (orelation_of_relation_preserves_composition ?? (form BP2) (rel BP1) ?); ]
+ [ apply (map_arrows2 ?? SUBSETS' (concr BP1) (concr BP2) (r \sub \c));
+ | apply (map_arrows2 ?? SUBSETS' (form BP1) (form BP2) (r \sub \f));
+ | apply (.= (respects_comp2 ?? SUBSETS' (concr BP1) (concr BP2) (form BP2) r\sub\c (⊩\sub BP2) )^-1);
+ cut (⊩ \sub BP2∘r \sub \c = r\sub\f ∘ ⊩ \sub BP1) as H;
+ [ apply (.= †H);
+ apply (respects_comp2 ?? SUBSETS' (concr BP1) (form BP1) (form BP2) (⊩\sub BP1) r\sub\f);
+ | apply commute;]]
qed.
-(*
-definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 cic:/matita/formal_topology/basic_pairs/BP.con) BP).
+definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP).
constructor 1;
[ apply o_basic_pair_of_basic_pair;
| intros; constructor 1;
[ apply (o_relation_pair_of_relation_pair S T);
- | intros; split; unfold o_relation_pair_of_relation_pair; simplify;
- unfold o_basic_pair_of_basic_pair; simplify; ]
- | simplify; intros; whd; split; unfold o_relation_pair_of_relation_pair; simplify;
- unfold o_basic_pair_of_basic_pair;
-simplify in ⊢ (? ? ? (? % ? ?) ?);
-simplify in ⊢ (? ? ? (? ? % ?) ?);
-simplify in ⊢ (? ? ? ? (? % ? ?));
-simplify in ⊢ (? ? ? ? (? ? % ?));
- | simplify; intros; whd; split;unfold o_relation_pair_of_relation_pair; simplify;
- unfold o_basic_pair_of_basic_pair;simplify;
+ | intros (a b Eab); split; unfold o_relation_pair_of_relation_pair; simplify;
+ unfold o_basic_pair_of_basic_pair; simplify;
+ [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x);
+ | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x);
+ | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x);
+ | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);]
+ simplify;
+ apply (prop12);
+ apply (.= (respects_comp2 ?? SUBSETS' (concr S) (concr T) (form T) (a\sub\c) (⊩\sub T))^-1);
+ apply sym2;
+ apply (.= (respects_comp2 ?? SUBSETS' (concr S) (concr T) (form T) (b\sub\c) (⊩\sub T))^-1);
+ apply sym2;
+ apply prop12;
+ apply Eab;
+ ]
+ | simplify; intros; whd; split;
+ [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x);
+ | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x);
+ | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x);
+ | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);]
+ simplify;
+ apply prop12;
+ apply prop22;[2,4,6,8: apply rule #;]
+ apply (respects_id2 ?? SUBSETS' (concr o));
+ | simplify; intros; whd; split;
+ [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x);
+ | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x);
+ | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x);
+ | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);]
+ simplify;
+ apply prop12;
+ apply prop22;[2,4,6,8: apply rule #;]
+ apply (respects_comp2 ?? SUBSETS' (concr o1) (concr o2) (concr o3) f1\sub\c f2\sub\c);]
+qed.
+
+
+(*
+theorem BP_to_OBP_faithful:
+ ∀S,T.∀f,g:arrows2 (category2_of_category1 BP) S T.
+ map_arrows2 ?? BP_to_OBP ?? f = map_arrows2 ?? BP_to_OBP ?? g → f=g.
+ intros; unfold BP_to_OBP in e; simplify in e; cases e;
+ unfold orelation_of_relation in e3; simplify in e3; clear e e1 e2 e4;
+ intros 2; change in match or_f_ in e3 with (λq,w,x.fun12 ?? (or_f q w) x);
+ simplify in e3; STOP lapply (e3 (singleton ? x)); cases Hletin;
+ split; intro; [ lapply (s y); | lapply (s1 y); ]
+ [2,4: exists; [1,3:apply x] split; [1,3: assumption |*: change with (x=x); apply rule #]
+ |*: cases Hletin1; cases x1; change in f3 with (eq1 ? x w); apply (. f3‡#); assumption;]
+qed.
+*)
+
+(*
+theorem SUBSETS_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BP_to_OBP S T g = f).
+ intros; exists;
+
*)
\ No newline at end of file
inductive exT2 (A:Type0) (P,Q:A→CProp0) : CProp0 ≝
ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
+inductive exT22 (A:Type2) (P:A→CProp2) : CProp2 ≝
+ ex_introT22: ∀w:A. P w → exT22 A P.
+
definition Not : CProp0 → Prop ≝ λx:CProp.x → False.
interpretation "constructive not" 'not x = (Not x).
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
o-saturations.ma o-algebra.ma
-basic_pairs.ma relations.ma
saturations.ma relations.ma
+basic_pairs.ma notation.ma relations.ma
o-algebra.ma categories.ma
o-formal_topologies.ma o-basic_topologies.ma
-categories.ma cprop_connectives.ma
formal_topologies.ma basic_topologies.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
+subsets.ma categories.ma
concrete_spaces.ma basic_pairs.ma
relations.ma subsets.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
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
+notation.ma
cprop_connectives.ma logic/connectives.ma
relations_to_o-algebra.ma o-algebra.ma relations.ma
o-basic_pairs_to_o-basic_topologies.ma o-basic_pairs.ma o-basic_topologies.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}.
+notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}.
(**************************************************************************)
include "o-algebra.ma".
+include "notation.ma".
-record basic_pair: Type2 ≝
- { concr: OA;
- form: OA;
- rel: arrows2 ? concr form
+record Obasic_pair: Type2 ≝
+ { Oconcr: OA;
+ Oform: OA;
+ Orel: arrows2 ? Oconcr Oform
}.
-interpretation "basic pair relation indexed" 'Vdash2 x y c = (rel c x y).
-interpretation "basic pair relation (non applied)" 'Vdash c = (rel c).
+interpretation "basic pair relation indexed" 'Vdash2 x y c = (Orel c x y).
+interpretation "basic pair relation (non applied)" 'Vdash c = (Orel c).
alias symbol "eq" = "setoid1 eq".
alias symbol "compose" = "category1 composition".
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);
- commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩
+record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝
+ { Oconcr_rel: arrows2 ? (Oconcr BP1) (Oconcr BP2);
+ Oform_rel: arrows2 ? (Oform BP1) (Oform BP2);
+ Ocommute: ⊩ ∘ Oconcr_rel = Oform_rel ∘ ⊩
}.
-notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}.
-notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}.
+interpretation "concrete relation" 'concr_rel r = (Oconcr_rel __ r).
+interpretation "formal relation" 'form_rel r = (Oform_rel __ r).
-interpretation "concrete relation" 'concr_rel r = (concr_rel __ r).
-interpretation "formal relation" 'form_rel r = (form_rel __ r).
-
-definition relation_pair_equality:
- ∀o1,o2. equivalence_relation2 (relation_pair o1 o2).
+definition Orelation_pair_equality:
+ ∀o1,o2. equivalence_relation2 (Orelation_pair o1 o2).
intros;
constructor 1;
[ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c);
qed.
(* qui setoid1 e' giusto: ma non lo e'!!! *)
-definition relation_pair_setoid: basic_pair → basic_pair → setoid2.
+definition Orelation_pair_setoid: Obasic_pair → Obasic_pair → setoid2.
intros;
constructor 1;
- [ apply (relation_pair b b1)
- | apply relation_pair_equality
+ [ apply (Orelation_pair o o1)
+ | apply Orelation_pair_equality
]
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.
+definition Orelation_pair_of_Orelation_pair_setoid:
+ ∀P,Q. Orelation_pair_setoid P Q → Orelation_pair P Q ≝ λP,Q,x.x.
+coercion Orelation_pair_of_Orelation_pair_setoid.
-lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
+lemma eq_to_eq': ∀o1,o2.∀r,r': Orelation_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 (.= ((Ocommute ?? r) ^ -1));
apply (.= H);
- apply (.= (commute ?? r'));
+ apply (.= (Ocommute ?? r'));
apply refl2;
qed.
-definition id_relation_pair: ∀o:basic_pair. relation_pair o o.
+definition Oid_relation_pair: ∀o:Obasic_pair. Orelation_pair o o.
intro;
constructor 1;
[1,2: apply id2;
- | lapply (id_neutral_right2 ? (concr o) ? (⊩)) as H;
- lapply (id_neutral_left2 ?? (form o) (⊩)) as H1;
+ | lapply (id_neutral_right2 ? (Oconcr o) ? (⊩)) as H;
+ lapply (id_neutral_left2 ?? (Oform o) (⊩)) as H1;
apply (.= H);
apply (H1 \sup -1);]
qed.
-definition relation_pair_composition:
- ∀o1,o2,o3. binary_morphism2 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
+definition Orelation_pair_composition:
+ ∀o1,o2,o3. binary_morphism2 (Orelation_pair_setoid o1 o2) (Orelation_pair_setoid o2 o3) (Orelation_pair_setoid o1 o3).
intros;
constructor 1;
[ intros (r r1);
constructor 1;
[ apply (r1 \sub\c ∘ r \sub\c)
| apply (r1 \sub\f ∘ r \sub\f)
- | lapply (commute ?? r) as H;
- lapply (commute ?? r1) as H1;
+ | lapply (Ocommute ?? r) as H;
+ lapply (Ocommute ?? r1) as H1;
apply rule (.= ASSOC);
apply (.= #‡H1);
apply rule (.= ASSOC ^ -1);
change in e1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c);
apply rule (.= ASSOC);
apply (.= #‡e1);
- apply (.= #‡(commute ?? b'));
+ apply (.= #‡(Ocommute ?? b'));
apply rule (.= ASSOC \sup -1);
apply (.= e‡#);
apply rule (.= ASSOC);
- apply (.= #‡(commute ?? b')\sup -1);
+ apply (.= #‡(Ocommute ?? b')\sup -1);
apply rule (ASSOC \sup -1)]
qed.
-definition BP: category2.
+definition OBP: category2.
constructor 1;
- [ apply basic_pair
- | apply relation_pair_setoid
- | apply id_relation_pair
- | apply relation_pair_composition
+ [ apply Obasic_pair
+ | apply Orelation_pair_setoid
+ | apply Oid_relation_pair
+ | apply Orelation_pair_composition
| intros;
change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) =
⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c));
apply rule (ASSOC‡#);
| intros;
- change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c);
+ change with (⊩ ∘ (a\sub\c ∘ (Oid_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c);
apply ((id_neutral_right2 ????)‡#);
| intros;
- change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c);
+ change with (⊩ ∘ ((Oid_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c);
apply ((id_neutral_left2 ????)‡#);]
qed.
-definition basic_pair_of_objs2_BP: objs2 BP → basic_pair ≝ λx.x.
-coercion basic_pair_of_objs2_BP.
+definition Obasic_pair_of_objs2_OBP: objs2 OBP → Obasic_pair ≝ λx.x.
+coercion Obasic_pair_of_objs2_OBP.
-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 Orelation_pair_setoid_of_arrows2_OBP:
+ ∀P,Q.arrows2 OBP P Q → Orelation_pair_setoid P Q ≝ λP,Q,c.c.
+coercion Orelation_pair_setoid_of_arrows2_OBP.
(*
definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
notation "□ \sub b" non associative with precedence 90 for @{'box $b}.
notation > "□_term 90 b" non associative with precedence 90 for @{'box $b}.
-interpretation "Universal image ⊩⎻*" 'box x = (fun12 _ _ (or_f_minus_star _ _) (rel x)).
+interpretation "Universal image ⊩⎻*" 'box x = (fun12 _ _ (or_f_minus_star _ _) (Orel x)).
notation "◊ \sub b" non associative with precedence 90 for @{'diamond $b}.
notation > "◊_term 90 b" non associative with precedence 90 for @{'diamond $b}.
-interpretation "Existential image ⊩" 'diamond x = (fun12 _ _ (or_f _ _) (rel x)).
+interpretation "Existential image ⊩" 'diamond x = (fun12 _ _ (or_f _ _) (Orel x)).
notation "'Rest' \sub b" non associative with precedence 90 for @{'rest $b}.
notation > "'Rest'⎽term 90 b" non associative with precedence 90 for @{'rest $b}.
-interpretation "Universal pre-image ⊩*" 'rest x = (fun12 _ _ (or_f_star _ _) (rel x)).
+interpretation "Universal pre-image ⊩*" 'rest x = (fun12 _ _ (or_f_star _ _) (Orel x)).
notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}.
notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}.
-interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 _ _ (or_f_minus _ _) (rel x)).
\ No newline at end of file
+interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 _ _ (or_f_minus _ _) (Orel x)).
\ No newline at end of file
alias symbol "eq" = "setoid1 eq".
(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
-definition o_basic_topology_of_o_basic_pair: BP → BTop.
+definition o_basic_topology_of_o_basic_pair: OBP → BTop.
intro t;
constructor 1;
- [ apply (form t);
+ [ apply (Oform t);
| apply (□_t ∘ Ext⎽t);
| apply (◊_t ∘ Rest⎽t);
| intros 2; split; intro;
qed.
definition o_continuous_relation_of_o_relation_pair:
- ∀BP1,BP2.arrows2 BP BP1 BP2 →
+ ∀BP1,BP2.arrows2 OBP BP1 BP2 →
arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
intros (BP1 BP2 t);
constructor 1;
apply (.= †(†e));
change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
- cases (commute ?? t); apply (e3 ^ -1 ((⊩)* U));]
+ cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩)* U));]
apply (.= †COM);
change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
apply (.= †(†e));
change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
- cases (commute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
+ cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
apply (.= †COM);
change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
include "o-basic_pairs.ma".
include "o-saturations.ma".
-definition A : ∀b:BP. unary_morphism1 (form b) (form b).
+definition A : ∀b:OBP. unary_morphism1 (Oform b) (Oform b).
intros; constructor 1;
[ apply (λx.□_b (Ext⎽b x));
| intros; apply (†(†e));]
intros; apply (†(†e));
qed.
-record concrete_space : Type2 ≝
- { bp:> BP;
+record Oconcrete_space : Type2 ≝
+ { Obp:> OBP;
(*distr : is_distributive (form bp);*)
- downarrow: unary_morphism1 (form bp) (form bp);
- downarrow_is_sat: is_o_saturation ? downarrow;
- converges: ∀q1,q2.
- (Ext⎽bp q1 ∧ (Ext⎽bp q2)) = (Ext⎽bp ((downarrow q1) ∧ (downarrow q2)));
- all_covered: Ext⎽bp (oa_one (form bp)) = oa_one (concr bp);
- il2: ∀I:SET.∀p:arrows2 SET1 I (form bp).
- downarrow (∨ { x ∈ I | downarrow (p x) | down_p ???? }) =
- ∨ { x ∈ I | downarrow (p x) | down_p ???? };
- il1: ∀q.downarrow (A ? q) = A ? q
+ Odownarrow: unary_morphism1 (Oform Obp) (Oform Obp);
+ Odownarrow_is_sat: is_o_saturation ? Odownarrow;
+ Oconverges: ∀q1,q2.
+ (Ext⎽Obp q1 ∧ (Ext⎽Obp q2)) = (Ext⎽Obp ((Odownarrow q1) ∧ (Odownarrow q2)));
+ Oall_covered: Ext⎽Obp (oa_one (Oform Obp)) = oa_one (Oconcr Obp);
+ Oil2: ∀I:SET.∀p:arrows2 SET1 I (Oform Obp).
+ Odownarrow (∨ { x ∈ I | Odownarrow (p x) | down_p ???? }) =
+ ∨ { x ∈ I | Odownarrow (p x) | down_p ???? };
+ Oil1: ∀q.Odownarrow (A ? q) = A ? q
}.
interpretation "o-concrete space downarrow" 'downarrow x =
- (fun11 __ (downarrow _) x).
+ (fun11 __ (Odownarrow _) x).
-definition binary_downarrow :
- ∀C:concrete_space.binary_morphism1 (form C) (form C) (form C).
+definition Obinary_downarrow :
+ ∀C:Oconcrete_space.binary_morphism1 (Oform C) (Oform C) (Oform C).
intros; constructor 1;
[ intros; apply (↓ c ∧ ↓ c1);
| intros;
apply ((†e)‡(†e1));]
qed.
-interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 _ _ _ (binary_downarrow _) a b).
+interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 _ _ _ (Obinary_downarrow _) a b).
-record convergent_relation_pair (CS1,CS2: concrete_space) : Type2 ≝
- { rp:> arrows2 ? CS1 CS2;
- respects_converges:
- ∀b,c. eq1 ? (rp\sub\c⎻ (Ext⎽CS2 (b ↓ c))) (Ext⎽CS1 (rp\sub\f⎻ b ↓ rp\sub\f⎻ c));
- respects_all_covered:
- eq1 ? (rp\sub\c⎻ (Ext⎽CS2 (oa_one (form CS2))))
- (Ext⎽CS1 (oa_one (form CS1)))
+record Oconvergent_relation_pair (CS1,CS2: Oconcrete_space) : Type2 ≝
+ { Orp:> arrows2 ? CS1 CS2;
+ Orespects_converges:
+ ∀b,c. eq1 ? (Orp\sub\c⎻ (Ext⎽CS2 (b ↓ c))) (Ext⎽CS1 (Orp\sub\f⎻ b ↓ Orp\sub\f⎻ c));
+ Orespects_all_covered:
+ eq1 ? (Orp\sub\c⎻ (Ext⎽CS2 (oa_one (Oform CS2))))
+ (Ext⎽CS1 (oa_one (Oform CS1)))
}.
-definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid2.
- intros;
+definition Oconvergent_relation_space_setoid: Oconcrete_space → Oconcrete_space → setoid2.
+ intros (c c1);
constructor 1;
- [ apply (convergent_relation_pair c c1)
+ [ apply (Oconvergent_relation_pair c c1)
| constructor 1;
- [ intros;
- apply (relation_pair_equality c c1 c2 c3);
+ [ intros (c2 c3);
+ apply (Orelation_pair_equality c c1 c2 c3);
| intros 1; apply refl2;
| intros 2; apply sym2;
| intros 3; apply trans2]]
qed.
-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 Oconvergent_relation_space_of_Oconvergent_relation_space_setoid:
+ ∀CS1,CS2.carr2 (Oconvergent_relation_space_setoid CS1 CS2) →
+ Oconvergent_relation_pair CS1 CS2 ≝ λP,Q,c.c.
+coercion Oconvergent_relation_space_of_Oconvergent_relation_space_setoid.
-definition convergent_relation_space_composition:
- ∀o1,o2,o3: concrete_space.
+definition Oconvergent_relation_space_composition:
+ ∀o1,o2,o3: Oconcrete_space.
binary_morphism2
- (convergent_relation_space_setoid o1 o2)
- (convergent_relation_space_setoid o2 o3)
- (convergent_relation_space_setoid o1 o3).
+ (Oconvergent_relation_space_setoid o1 o2)
+ (Oconvergent_relation_space_setoid o2 o3)
+ (Oconvergent_relation_space_setoid o1 o3).
intros; constructor 1;
[ intros; whd in t t1 ⊢ %;
constructor 1;
| intros;
change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (b↓c2))));
alias symbol "trans" = "trans1".
- apply (.= († (respects_converges : ?)));
- 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 ?? c);]
+ apply (.= († (Orespects_converges : ?)));
+ apply (Orespects_converges ?? c (c1\sub\f⎻ b) (c1\sub\f⎻ c2));
+ | change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (oa_one (Oform o3)))));
+ apply (.= (†(Orespects_all_covered :?)));
+ apply rule (Orespects_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 (Orp ?? a = Orp ?? a');
+ change in e1 with (Orp ?? b = Orp ?? b');
apply (e‡e1);]
qed.
-definition CSPA: category2.
+definition OCSPA: category2.
constructor 1;
- [ apply concrete_space
- | apply convergent_relation_space_setoid
+ [ apply Oconcrete_space
+ | apply Oconvergent_relation_space_setoid
| intro; constructor 1;
[ apply id2
| intros; apply refl1;
| apply refl1]
- | apply convergent_relation_space_composition
+ | apply Oconvergent_relation_space_composition
| intros; simplify; whd in a12 a23 a34;
change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
apply rule ASSOC;
| intros; simplify;
- change with (a ∘ id2 BP o1 = a);
+ change with (a ∘ id2 OBP o1 = a);
apply (id_neutral_right2 : ?);
| intros; simplify;
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 Oconcrete_space_of_OCSPA : objs2 OCSPA → Oconcrete_space ≝ λx.x.
+coercion Oconcrete_space_of_OCSPA.
-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.
+definition Oconvergent_relation_space_setoid_of_arrows2_OCSPA :
+ ∀P,Q. arrows2 OCSPA P Q → Oconvergent_relation_space_setoid P Q ≝ λP,Q,x.x.
+coercion Oconvergent_relation_space_setoid_of_arrows2_OCSPA.
|*: cases Hletin1; cases x1; change in f3 with (eq1 ? x w); apply (. f3‡#); assumption;]
qed.
-inductive exT2 (A:Type2) (P:A→CProp2) : CProp2 ≝
- ex_introT2: ∀w:A. P w → exT2 A P.
-theorem SUBSETS_full: ∀S,T.∀f. exT2 ? (λg. map_arrows2 ?? SUBSETS' S T g = f).
+theorem SUBSETS_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? SUBSETS' S T g = f).
intros; exists;
[ constructor 1; constructor 1;
[ apply (λx:carr S.λy:carr T. y ∈ f (singleton S x));
projects / helm.git / commitdiff