include "formal_topology/basic_pairs.ma".
-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 (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 BPext: ∀o: basic_pair. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o).
-
-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 BPextS: ∀o: basic_pair. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
- λo.extS ?? (rel o).
-
-definition fintersects: ∀o: basic_pair. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
- intros (o); constructor 1;
- [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
- intros; simplify; apply (.= (†H)‡#); apply refl1
- | intros; split; simplify; intros;
- [ apply (. #‡((†H)‡(†H1))); assumption
- | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
-qed.
-
-interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
-
-definition fintersectsS:
- ∀o:basic_pair. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (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 });
- intros; simplify; apply (.= (†H)‡#); apply refl1
- | intros; split; simplify; intros;
- [ apply (. #‡((†H)‡(†H1))); assumption
- | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
-qed.
-
-interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
-
-definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp ≝
- λo:basic_pair.λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y.
-
-interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 ___ (relS _) x y).
-interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
-
-(*
-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
+(* carr1 e' necessario perche' ci sega via la coercion per gli oggetti di REL!
+ (confondendola con la coercion per gli oggetti di SET
+record concrete_space : Type1 ≝
+ { bp:> BP;
+ converges: ∀a: carr1 (concr bp).∀U,V: carr1 (form bp). a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
+ all_covered: ∀x: carr1 (concr bp). x ⊩ form bp
}.
-record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
- { rp:> relation_pair CS1 CS2;
+record convergent_relation_pair (CS1,CS2: concrete_space) : Type1 ≝
+ { rp:> arrows1 ? 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));
+ minus_image ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
+ BPextS CS1 ((minus_image ?? rp \sub\f b) ↓ (minus_image ?? rp \sub\f c));
respects_all_covered:
- extS ?? rp\sub\c (extS ?? (rel CS2) (form CS2)) =
- extS ?? (rel CS1) (form CS1)
+ minus_image ?? rp\sub\c (BPextS CS2 (full_subset (form CS2))) = BPextS CS1 (full_subset (form CS1))
}.
-(*
-definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid.
+definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1.
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]]
+ | intros 1; apply refl1;
+ | intros 2; apply sym1;
+ | intros 3; apply trans1]]
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]]]
+definition convergent_relation_space_composition:
+ ∀o1,o2,o3: concrete_space.
+ binary_morphism1
+ (convergent_relation_space_setoid o1 o2)
+ (convergent_relation_space_setoid o2 o3)
+ (convergent_relation_space_setoid o1 o3).
+ intros; constructor 1;
+ [ intros; whd in c c1 ⊢ %;
+ constructor 1;
+ [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
+ | intros;
+ change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
+ change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
+ with (c1 \sub \f ∘ c \sub \f);
+ change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
+ with (c1 \sub \f ∘ c \sub \f);
+ apply (.= (extS_com ??????));
+ apply (.= (†(respects_converges ?????)));
+ apply (.= (respects_converges ?????));
+ apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
+ apply refl1;
+ | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
+ apply (.= (extS_com ??????));
+ apply (.= (†(respects_all_covered ???)));
+ apply (.= respects_all_covered ???);
+ apply refl1]
+ | intros;
+ change with (b ∘ a = b' ∘ a');
+ change in H with (rp'' ?? a = rp'' ?? a');
+ change in H1 with (rp'' ?? b = rp ?? b');
+ apply (.= (H‡H1));
+ apply refl1]
qed.
-definition CSPA: category.
+definition CSPA: category1.
constructor 1;
[ apply concrete_space
| apply convergent_relation_space_setoid
| intro; constructor 1;
- [ apply id
+ [ apply id1
| intros;
unfold id; simplify;
apply (.= (equalset_extS_id_X_X ??));
-
- |
- ]
- |*)
+ apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡
+ (equalset_extS_id_X_X ??)\sup -1)));
+ apply refl1;
+ | apply (.= (equalset_extS_id_X_X ??));
+ apply refl1]
+ | apply convergent_relation_space_composition
+ | intros; simplify;
+ change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
+ apply (.= ASSOC1);
+ apply refl1
+ | intros; simplify;
+ change with (a ∘ id1 ? o1 = a);
+ apply (.= id_neutral_right1 ????);
+ apply refl1
+ | intros; simplify;
+ change with (id1 ? o2 ∘ a = a);
+ apply (.= id_neutral_left1 ????);
+ apply refl1]
+qed.
+*)
\ No newline at end of file