eq: equivalence_relation carr
}.
+definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
+definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
+definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
+
+record equivalence_relation1 (A:Type) : Type ≝
+ { eq_rel1:2> A → A → CProp;
+ refl1: reflexive1 ? eq_rel1;
+ sym1: symmetric1 ? eq_rel1;
+ trans1: transitive1 ? eq_rel1
+ }.
+
+record setoid1: Type ≝
+ { carr1:> Type;
+ eq1: equivalence_relation1 carr1
+ }.
+
+definition setoid1_of_setoid: setoid → setoid1.
+ intro;
+ constructor 1;
+ [ apply (carr s)
+ | constructor 1;
+ [ apply (eq_rel s);
+ apply (eq s)
+ | apply (refl s)
+ | apply (sym s)
+ | apply (trans s)]]
+qed.
+
+coercion setoid1_of_setoid.
+
+(*
+definition Leibniz: Type → setoid.
+ intro;
+ constructor 1;
+ [ apply T
+ | constructor 1;
+ [ apply (λx,y:T.cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y)
+ | alias id "refl_eq" = "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)".
+ apply refl_eq
+ | alias id "sym_eq" = "cic:/matita/logic/equality/sym_eq.con".
+ apply sym_eq
+ | alias id "trans_eq" = "cic:/matita/logic/equality/trans_eq.con".
+ apply trans_eq ]]
+qed.
+
+coercion Leibniz.
+*)
+
+interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y).
interpretation "setoid eq" 'eq x y = (eq_rel _ (eq _) x y).
-notation ".= r" with precedence 50 for @{trans ????? $r}.
+interpretation "setoid1 symmetry" 'invert r = (sym1 ____ r).
interpretation "setoid symmetry" 'invert r = (sym ____ r).
+notation ".= r" with precedence 50 for @{'trans $r}.
+interpretation "trans1" 'trans r = (trans1 _____ r).
+interpretation "trans" 'trans r = (trans _____ r).
-record binary_morphism (A,B,C: setoid) : Type ≝
+record unary_morphism (A,B: setoid1) : Type ≝
+ { fun_1:1> A → B;
+ prop_1: ∀a,a'. eq1 ? a a' → eq1 ? (fun_1 a) (fun_1 a')
+ }.
+
+record binary_morphism (A,B,C:setoid) : Type ≝
{ fun:2> A → B → C;
prop: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun a b) (fun a' b')
}.
-notation "# r" with precedence 60 for @{prop ???????? (refl ???) $r}.
-notation "r #" with precedence 60 for @{prop ???????? $r (refl ???)}.
+record binary_morphism1 (A,B,C:setoid1) : Type ≝
+ { fun1:2> A → B → C;
+ prop1: ∀a,a',b,b'. eq1 ? a a' → eq1 ? b b' → eq1 ? (fun1 a b) (fun1 a' b')
+ }.
-definition CPROP: setoid.
+notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
+interpretation "unary morphism" 'Imply a b = (unary_morphism a b).
+
+notation "† c" with precedence 90 for @{'prop1 $c }.
+notation "l ‡ r" with precedence 90 for @{'prop $l $r }.
+notation "#" with precedence 90 for @{'refl}.
+interpretation "prop_1" 'prop1 c = (prop_1 _____ c).
+interpretation "prop1" 'prop l r = (prop1 ________ l r).
+interpretation "prop" 'prop l r = (prop ________ l r).
+interpretation "refl1" 'refl = (refl1 ___).
+interpretation "refl" 'refl = (refl ___).
+
+definition CPROP: setoid1.
constructor 1;
[ apply CProp
| constructor 1;
[ apply (H4 (H2 H6)) | apply (H3 (H5 H6))]]]
qed.
+definition if': ∀A,B:CPROP. A = B → A → B.
+ intros; apply (if ?? H); assumption.
+qed.
+
+notation ". r" with precedence 50 for @{'if $r}.
+interpretation "if" 'if r = (if' __ r).
+
+definition and_morphism: binary_morphism1 CPROP CPROP CPROP.
+ constructor 1;
+ [ apply And
+ | intros; split; intro; cases H2; split;
+ [ apply (if ?? H a1)
+ | apply (if ?? H1 b1)
+ | apply (fi ?? H a1)
+ | apply (fi ?? H1 b1)]]
+qed.
+
+interpretation "and_morphism" 'and a b = (fun1 ___ and_morphism a b).
+
+definition or_morphism: binary_morphism1 CPROP CPROP CPROP.
+ constructor 1;
+ [ apply Or
+ | intros; split; intro; cases H2; [1,3:left |2,4: right]
+ [ apply (if ?? H a1)
+ | apply (fi ?? H a1)
+ | apply (if ?? H1 b1)
+ | apply (fi ?? H1 b1)]]
+qed.
+
+interpretation "or_morphism" 'or a b = (fun1 ___ or_morphism a b).
+
+definition if_morphism: binary_morphism1 CPROP CPROP CPROP.
+ constructor 1;
+ [ apply (λA,B. A → B)
+ | intros; split; intros;
+ [ apply (if ?? H1); apply H2; apply (fi ?? H); assumption
+ | apply (fi ?? H1); apply H2; apply (if ?? H); assumption]]
+qed.
+
+(*
definition eq_morphism: ∀S:setoid. binary_morphism S S CPROP.
intro;
constructor 1;
apply (.= H2);
apply (H1 \sup -1)]]
qed.
+*)
record category : Type ≝
{ objs:> Type;
id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
}.
+record category1 : Type ≝
+ { objs1:> Type;
+ arrows1: objs1 → objs1 → setoid1;
+ id1: ∀o:objs1. arrows1 o o;
+ comp1: ∀o1,o2,o3. binary_morphism1 (arrows1 o1 o2) (arrows1 o2 o3) (arrows1 o1 o3);
+ comp_assoc1: ∀o1,o2,o3,o4. ∀a12,a23,a34.
+ comp1 o1 o3 o4 (comp1 o1 o2 o3 a12 a23) a34 = comp1 o1 o2 o4 a12 (comp1 o2 o3 o4 a23 a34);
+ id_neutral_left1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? (id1 o1) a = a;
+ id_neutral_right1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? a (id1 o2) = a
+ }.
+
+notation "'ASSOC'" with precedence 90 for @{'assoc}.
+notation "'ASSOC1'" with precedence 90 for @{'assoc1}.
+
+interpretation "category1 composition" 'compose x y = (fun1 ___ (comp1 ____) x y).
+interpretation "category1 assoc" 'assoc1 = (comp_assoc1 ________).
interpretation "category composition" 'compose x y = (fun ___ (comp ____) x y).
-notation "'ASSOC'" with precedence 90 for @{comp_assoc ????????}.
\ No newline at end of file
+interpretation "category assoc" 'assoc = (comp_assoc ________).
include "logic/cprop_connectives.ma".
include "datatypes/categories.ma".
-record powerset (A: Type) : Type ≝ { char: A → CProp }.
-
-interpretation "powerset" 'powerset A = (powerset A).
-
-interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
-
-definition mem ≝ λA.λS:Ω \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
-
-interpretation "mem" 'mem a S = (mem _ S a).
-
-definition overlaps ≝ λA:Type.λU,V:Ω \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
-
-interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
-
-definition subseteq ≝ λA:Type.λU,V:Ω \sup A.∀a:A. a ∈ U → a ∈ V.
-
-interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
-
-definition intersects ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∧ a ∈ V}.
-
-interpretation "intersects" 'intersects U V = (intersects _ U V).
-
-definition union ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∨ a ∈ V}.
-
-interpretation "union" 'union U V = (union _ U V).
-
-include "logic/equality.ma".
-
-definition singleton ≝ λA:Type.λa:A.{b | a=b}.
-
-interpretation "singleton" 'singl a = (singleton _ a).
\ No newline at end of file
+record powerset_carrier (A: setoid) : Type ≝ { mem_operator: A ⇒ CPROP }.
+
+definition subseteq_operator ≝
+ λA:setoid.λU,V.∀a:A. mem_operator ? U a → mem_operator ? V a.
+
+theorem transitive_subseteq_operator: ∀A. transitive ? (subseteq_operator A).
+ intros 6; intros 2;
+ apply s1; apply s;
+ assumption.
+qed.
+
+definition powerset_setoid: setoid → setoid1.
+ intros (T);
+ constructor 1;
+ [ apply (powerset_carrier T)
+ | constructor 1;
+ [ apply (λU,V. subseteq_operator ? U V ∧ subseteq_operator ? V U)
+ | simplify; intros; split; intros 2; assumption
+ | simplify; intros (x y H); cases H; split; assumption
+ | simplify; intros (x y z H H1); cases H; cases H1; split;
+ apply transitive_subseteq_operator; [1,4: apply y ]
+ assumption ]]
+qed.
+
+interpretation "powerset" 'powerset A = (powerset_setoid A).
+
+interpretation "subset construction" 'subset \eta.x =
+ (mk_powerset_carrier _ (mk_unary_morphism _ CPROP x _)).
+
+definition mem: ∀A. binary_morphism1 A (Ω \sup A) CPROP.
+ intros;
+ constructor 1;
+ [ apply (λx,S. mem_operator ? S x)
+ | intros 5;
+ cases b; clear b; cases b'; clear b'; simplify; intros;
+ apply (trans1 ????? (prop_1 ?? u ?? H));
+ cases H1; whd in s s1;
+ split; intro;
+ [ apply s; assumption
+ | apply s1; assumption]]
+qed.
+
+interpretation "mem" 'mem a S = (fun1 ___ (mem _) a S).
+
+definition subseteq: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
+ intros;
+ constructor 1;
+ [ apply (λU,V. subseteq_operator ? U V)
+ | intros;
+ cases H; cases H1;
+ split; intros 1;
+ [ apply (transitive_subseteq_operator ????? s2);
+ apply (transitive_subseteq_operator ???? s1 s4)
+ | apply (transitive_subseteq_operator ????? s3);
+ apply (transitive_subseteq_operator ???? s s4) ]]
+qed.
+
+interpretation "subseteq" 'subseteq U V = (fun1 ___ (subseteq _) U V).
+
+definition overlaps: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
+ intros;
+ constructor 1;
+ [ apply (λA.λU,V:Ω \sup A.exT2 ? (λx:A.x ∈ U) (λx:A.x ∈ V))
+ | intros;
+ constructor 1; intro; cases H2; exists; [1,4: apply w]
+ [ apply (. #‡H); assumption
+ | apply (. #‡H1); assumption
+ | apply (. #‡(H \sup -1)); assumption;
+ | apply (. #‡(H1 \sup -1)); assumption]]
+qed.
+
+interpretation "overlaps" 'overlaps U V = (fun1 ___ (overlaps _) U V).
+
+definition intersects:
+ ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
+ intros;
+ constructor 1;
+ [ apply (λU,V. {x | x ∈ U ∧ x ∈ V });
+ intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1;
+ | intros;
+ split; intros 2; simplify in f ⊢ %;
+ [ apply (. (#‡H)‡(#‡H1)); assumption
+ | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
+qed.
+
+interpretation "intersects" 'intersects U V = (fun1 ___ (intersects _) U V).
+
+definition union:
+ ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
+ intros;
+ constructor 1;
+ [ apply (λU,V. {x | x ∈ U ∨ x ∈ V });
+ intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1
+ | intros;
+ split; intros 2; simplify in f ⊢ %;
+ [ apply (. (#‡H)‡(#‡H1)); assumption
+ | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
+qed.
+
+interpretation "union" 'union U V = (fun1 ___ (union _) U V).
+
+definition singleton: ∀A:setoid. A → Ω \sup A.
+ apply (λA:setoid.λa:A.{b | a=b});
+ intros; simplify;
+ split; intro;
+ apply (.= H1);
+ [ apply H | apply (H \sup -1) ]
+qed.
+
+interpretation "singleton" 'singl a = (singleton _ a).
record basic_pair: Type ≝
{ concr: REL;
form: REL;
- rel: arrows ? concr form
+ rel: arrows1 ? concr form
}.
notation "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y}.
interpretation "basic pair relation (non applied)" 'Vdash = (rel _).
record relation_pair (BP1,BP2: basic_pair): Type ≝
- { concr_rel: arrows ? (concr BP1) (concr BP2);
- form_rel: arrows ? (form BP1) (form BP2);
+ { concr_rel: arrows1 ? (concr BP1) (concr BP2);
+ form_rel: arrows1 ? (form BP1) (form BP2);
commute: concr_rel ∘ ⊩ = ⊩ ∘ form_rel
}.
interpretation "formal relation" 'form_rel r = (form_rel __ r).
definition relation_pair_equality:
- ∀o1,o2. equivalence_relation (relation_pair o1 o2).
+ ∀o1,o2. equivalence_relation1 (relation_pair o1 o2).
intros;
constructor 1;
[ apply (λr,r'. r \sub\c ∘ ⊩ = r' \sub\c ∘ ⊩);
| simplify;
intros;
- apply refl;
+ apply refl1;
| simplify;
intros 2;
- apply sym;
+ apply sym1;
| simplify;
intros 3;
- apply trans;
+ apply trans1;
]
qed.
-definition relation_pair_setoid: basic_pair → basic_pair → setoid.
+definition relation_pair_setoid: basic_pair → basic_pair → setoid1.
intros;
constructor 1;
[ apply (relation_pair b b1)
lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → ⊩ \circ r \sub\f = ⊩ \circ r'\sub\f.
intros 7 (o1 o2 r r' H c1 f2);
- split; intro;
+ split; intro H1;
[ lapply (fi ?? (commute ?? r c1 f2) H1) as H2;
lapply (if ?? (H c1 f2) H2) as H3;
apply (if ?? (commute ?? r' c1 f2) H3);
definition id: ∀o:basic_pair. relation_pair o o.
intro;
constructor 1;
- [1,2: apply id;
- | lapply (id_neutral_left ? (concr o) ? (⊩)) as H;
- lapply (id_neutral_right ?? (form o) (⊩)) as H1;
+ [1,2: apply id1;
+ | lapply (id_neutral_left1 ? (concr o) ? (⊩)) as H;
+ lapply (id_neutral_right1 ?? (form o) (⊩)) as H1;
apply (.= H);
apply (H1 \sup -1);]
qed.
definition relation_pair_composition:
- ∀o1,o2,o3. binary_morphism (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
+ ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
intros;
constructor 1;
[ intros (r r1);
| apply (r \sub\f ∘ r1 \sub\f)
| lapply (commute ?? r) as H;
lapply (commute ?? r1) as H1;
- apply (.= ASSOC);
- apply (.= #H1);
- apply (.= ASSOC\sup -1);
- apply (.= H#);
- apply comp_assoc]
+ apply (.= ASSOC1);
+ apply (.= #‡H1);
+ apply (.= ASSOC1\sup -1);
+ apply (.= H‡#);
+ apply ASSOC1]
| intros;
change with (a\sub\c ∘ b\sub\c ∘ ⊩ = a'\sub\c ∘ b'\sub\c ∘ ⊩);
change in H with (a \sub\c ∘ ⊩ = a' \sub\c ∘ ⊩);
change in H1 with (b \sub\c ∘ ⊩ = b' \sub\c ∘ ⊩);
- apply (.= ASSOC);
- apply (.= #H1);
- apply (.= #(commute ?? b'));
- apply (.= ASSOC \sup -1);
- apply (.= H#);
- apply (.= ASSOC);
- apply (.= #(commute ?? b')\sup -1);
- apply (ASSOC \sup -1)]
+ apply (.= ASSOC1);
+ apply (.= #‡H1);
+ apply (.= #‡(commute ?? b'));
+ apply (.= ASSOC1 \sup -1);
+ apply (.= H‡#);
+ apply (.= ASSOC1);
+ apply (.= #‡(commute ?? b')\sup -1);
+ apply (ASSOC1 \sup -1)]
qed.
-definition BP: category.
+definition BP: category1.
constructor 1;
[ apply basic_pair
| apply relation_pair_setoid
| intros;
change with (a12\sub\c ∘ a23\sub\c ∘ a34\sub\c ∘ ⊩ =
(a12\sub\c ∘ (a23\sub\c ∘ a34\sub\c) ∘ ⊩));
- apply (ASSOC#);
+ apply (ASSOC1‡#);
| intros;
change with ((id o1)\sub\c ∘ a\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
- apply ((id_neutral_left ????)#);
+ apply ((id_neutral_left1 ????)‡#);
| intros;
change with (a\sub\c ∘ (id o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
- apply ((id_neutral_right ????)#);
+ apply ((id_neutral_right1 ????)‡#);
]
qed.
\ No newline at end of file
include "formal_topology/basic_pairs.ma".
-interpretation "REL carrier" 'card c = (carrier c).
-
-definition comprehension: ∀b:REL. (b → CProp) → Ω \sup |b| ≝
- λb:REL.λP.{x | ∃p: x ∈ b. P (mk_ssigma ?? x p)}.
+definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b.
+ apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x});
+ intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1.
+qed.
interpretation "subset comprehension" 'comprehension s p =
- (comprehension s p).
+ (comprehension s (mk_unary_morphism __ p _)).
+
+definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
+ apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
+ [ intros; simplify; apply (.= (H‡#)); apply refl1
+ | intros; simplify; split; intros; simplify; intros;
+ [ apply (. #‡(#‡H)); assumption
+ | apply (. #‡(#‡H\sup -1)); assumption]]
+qed.
-definition ext: ∀o: basic_pair. form o → Ω \sup |(concr o)| ≝
- λo,f.{x ∈ (concr o) | x ♮(rel o) f}.
+definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
+ (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
+ intros (X S r); constructor 1;
+ [ intro F; constructor 1; constructor 1;
+ [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
+ | intros; split; intro; cases f (H1 H2); clear f; split;
+ [ apply (. (H‡#)); assumption
+ |3: apply (. (H\sup -1‡#)); assumption
+ |2,4: cases H2 (w H3); exists; [1,3: apply w]
+ [ apply (. (#‡(H‡#))); assumption
+ | apply (. (#‡(H \sup -1‡#))); assumption]]]
+ | intros; split; simplify; intros; cases f; cases H1; split;
+ [1,3: assumption
+ |2,4: exists; [1,3: apply w]
+ [ apply (. (#‡H)‡#); assumption
+ | apply (. (#‡H\sup -1)‡#); assumption]]]
+qed.
-definition fintersects ≝
- λo: basic_pair.λa,b: form o.
- {c | ext ? c ⊆ ext ? a ∩ ext ? b }.
+definition fintersects: ∀o: basic_pair. form o → form o → Ω \sup (form o).
+ apply
+ (λo: basic_pair.λa,b: form o.
+ {c | ext ?? (rel o) c ⊆ ext ?? (rel o) a ∩ ext ?? (rel o) b });
+ intros; simplify; apply (.= (†H)‡#); apply refl1.
+qed.
interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
+(*
+definition fintersectsS ≝
+ λo: basic_pair.λa,b: Ω \sup (form o).
+ {c | ext ?? (rel o) c ⊆ extS ?? (rel o) a ∩ extS ?? (rel o) b }.
+
+interpretation "fintersectsS" 'fintersects U V = (fintersectsS _ U V).
definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp ≝
- λo,x,S. ∃y. y ∈ S ∧ x ⊩ y.
+ λo,x,S. ∃y.y ∈ S ∧ x ⊩ y.
interpretation "basic pair relation for subsets" 'Vdash2 x y = (relS _ x y).
interpretation "basic pair relation for subsets (non applied)" 'Vdash = (relS _).
-definition convergence ≝
- λo: basic_pair.∀a: concr o.∀U,V: form o. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V).
\ No newline at end of file
+record concrete_space : Type ≝
+ { bp:> basic_pair;
+ converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
+ all_covered: ∀x: concr bp. x ⊩ form bp
+ }.
+
+record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
+ { rp:> relation_pair CS1 CS2;
+ respects_converges:
+ ∀b,c.
+ extS ?? rp \sub\c (extS ?? (rel CS2) (b ↓ c)) =
+ extS ?? (rel CS1) ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
+ respects_all_covered:
+ extS ?? rp\sub\c (extS ?? (rel CS2) (form CS2)) =
+ extS ?? (rel CS1) (form CS1)
+ }.
+
+definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid.
+ intros;
+ constructor 1;
+ [ apply (convergent_relation_pair c c1)
+ | constructor 1;
+ [ intros;
+ apply (relation_pair_equality c c1 c2 c3);
+ | intros 1; apply refl;
+ | intros 2; apply sym;
+ | intros 3; apply trans]]
+qed.
+
+lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id ? o) X = X.
+ intros;
+ unfold extS;
+ split;
+ [ intros 2;
+ cases m; clear m;
+ cases H; clear H;
+ cases H1; clear H1;
+ whd in H;
+ apply (eq_elim_r'' ????? H);
+ assumption
+ | intros 2;
+ constructor 1;
+ [ whd; exact I
+ | exists; [ apply a ]
+ split;
+ [ assumption
+ | whd; constructor 1]]]
+qed.
+
+definition CSPA: category.
+ constructor 1;
+ [ apply concrete_space
+ | apply convergent_relation_space_setoid
+ | intro; constructor 1;
+ [ apply id
+ | intros;
+ unfold id; simplify;
+ apply (.= (equalset_extS_id_X_X ??));
+
+ |
+ ]
+ |*)
\ No newline at end of file
include "datatypes/subsets.ma".
-record binary_relation (A,B: Type) : Type ≝
- { satisfy:2> A → B → CProp }.
+record binary_relation (A,B: setoid) : Type ≝
+ { satisfy:> binary_morphism1 A B CPROP }.
notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{'satisfy $r $x $y}.
notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}.
-interpretation "relation applied" 'satisfy r x y = (satisfy __ r x y).
+interpretation "relation applied" 'satisfy r x y = (fun1 ___ (satisfy __ r) x y).
-definition composition:
- ∀A,B,C.
- binary_relation A B → binary_relation B C →
- binary_relation A C.
- intros (A B C R12 R23);
+definition binary_relation_setoid: setoid → setoid → setoid1.
+ intros (A B);
constructor 1;
- intros (s1 s3);
- apply (∃s2. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
-qed.
-
-interpretation "binary relation composition" 'compose x y = (composition ___ x y).
-
-definition equal_relations ≝
- λA,B.λr,r': binary_relation A B.
- ∀x,y. r x y ↔ r' x y.
-
-interpretation "equal relation" 'eq x y = (equal_relations __ x y).
-
-lemma refl_equal_relations: ∀A,B. reflexive ? (equal_relations A B).
- intros 3; intros 2; split; intro; assumption.
-qed.
-
-lemma sym_equal_relations: ∀A,B. symmetric ? (equal_relations A B).
- intros 5; intros 2; split; intro;
- [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption.
-qed.
-
-lemma trans_equal_relations: ∀A,B. transitive ? (equal_relations A B).
- intros 7; intros 2; split; intro;
- [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
- [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
- assumption.
-qed.
-
-lemma associative_composition:
- ∀A,B,C,D.
- ∀r1:binary_relation A B.
- ∀r2:binary_relation B C.
- ∀r3:binary_relation C D.
- (r1 ∘ r2) ∘ r3 = r1 ∘ (r2 ∘ r3).
- intros 9;
- split; intro;
- cases H; clear H; cases H1; clear H1;
- [cases H; clear H | cases H2; clear H2]
- cases H1; clear H1;
- exists; try assumption;
- split; try assumption;
- exists; try assumption;
- split; assumption.
+ [ apply (binary_relation A B)
+ | constructor 1;
+ [ apply (λA,B.λr,r': binary_relation A B. ∀x,y. r x y ↔ r' x y)
+ | simplify; intros 3; split; intro; assumption
+ | simplify; intros 5; split; intro;
+ [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption
+ | simplify; intros 7; split; intro;
+ [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
+ [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
+ assumption]]
qed.
-lemma composition_morphism:
+definition composition:
∀A,B,C.
- ∀r1,r1':binary_relation A B.
- ∀r2,r2':binary_relation B C.
- r1 = r1' → r2 = r2' → r1 ∘ r2 = r1' ∘ r2'.
- intros 11; split; intro;
- cases H2; clear H2; cases H3; clear H3;
- [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
- [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
- exists; try assumption;
- split; assumption.
-qed.
-
-definition binary_relation_setoid: Type → Type → setoid.
- intros (A B);
+ binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C).
+ intros;
constructor 1;
- [ apply (binary_relation A B)
- | constructor 1;
- [ apply equal_relations
- | apply refl_equal_relations
- | apply sym_equal_relations
- | apply trans_equal_relations
- ]]
+ [ intros (R12 R23);
+ constructor 1;
+ constructor 1;
+ [ apply (λs1:A.λs3:C.∃s2:B. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
+ | intros;
+ split; intro; cases H2 (w H3); clear H2; exists; [1,3: apply w ]
+ [ apply (. (H‡#)‡(#‡H1)); assumption
+ | apply (. ((H \sup -1)‡#)‡(#‡(H1 \sup -1))); assumption]]
+ | intros 8; split; intro H2; simplify in H2 ⊢ %;
+ cases H2 (w H3); clear H2; exists [1,3: apply w] cases H3 (H2 H4); clear H3;
+ [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
+ [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
+ exists; try assumption;
+ split; assumption]
qed.
-definition REL: category.
+definition REL: category1.
constructor 1;
- [ apply Type
- | intros; apply (binary_relation_setoid T T1)
- | intros; constructor 1; intros; apply (eq ? o1 o2);
+ [ apply setoid
+ | intros (T T1); apply (binary_relation_setoid T T1)
| intros; constructor 1;
- [ apply composition
- | apply composition_morphism
- ]
- | intros; unfold mk_binary_morphism; simplify;
- apply associative_composition
- |6,7: intros 5; simplify; split; intro;
- [1,3: cases H; clear H; cases H1; clear H1;
- [ alias id "eq_elim_r''" = "cic:/matita/logic/equality/eq_elim_r''.con".
- apply (eq_elim_r'' ? w ?? x H); assumption
- | alias id "eq_rect" = "cic:/matita/logic/equality/eq_rect.con".
- apply (eq_rect ? w ?? y H2); assumption ]
- assumption
- |*: exists; try assumption; split;
- alias id "refl_eq" = "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)".
- first [ apply refl_eq | assumption ]]]
+ constructor 1; unfold setoid1_of_setoid; simplify;
+ [ intros; apply (c = c1)
+ | intros; split; intro;
+ [ apply (trans ????? (H \sup -1));
+ apply (trans ????? H2);
+ apply H1
+ | apply (trans ????? H);
+ apply (trans ????? H2);
+ apply (H1 \sup -1)]]
+ | apply composition
+ | intros 9;
+ split; intro;
+ cases f (w H); clear f; cases H; clear H;
+ [cases f (w1 H); clear f | cases f1 (w1 H); clear f1]
+ cases H; clear H;
+ exists; try assumption;
+ split; try assumption;
+ exists; try assumption;
+ split; assumption
+ |6,7: intros 5; unfold composition; simplify; split; intro;
+ unfold setoid1_of_setoid in x y; simplify in x y;
+ [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold;
+ [ apply (. (H \sup -1 : eq1 ? w x)‡#); assumption
+ | apply (. #‡(H : eq1 ? w y)); assumption]
+ |2,4: exists; try assumption; split; first [apply refl | assumption]]]
qed.
-definition full_subset: ∀s:REL. Ω \sup s ≝ λs.{x | True}.
+definition full_subset: ∀s:REL. Ω \sup s.
+ apply (λs.{x | True});
+ intros; simplify; split; intro; assumption.
+qed.
+
+coercion full_subset.
+
+definition setoid1_of_REL: REL → setoid ≝ λS. S.
-coercion full_subset.
\ No newline at end of file
+coercion setoid1_of_REL.
\ No newline at end of file
projects / helm.git / commitdiff