| apply (. #‡(#‡H\sup -1)); assumption]]
qed.
+definition BPext: ∀o: BP. 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;
| apply (. (#‡H\sup -1)‡#); assumption]]]
qed.
-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.
+definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
+ λo.extS ?? (rel o).
+
+definition fintersects: ∀o: BP. 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 = (fintersects _ U V).
+interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
definition fintersectsS:
- ∀o:basic_pair. Ω \sup (form o) → Ω \sup (form o) → Ω \sup (form o).
- apply (λo: basic_pair.λa,b: Ω \sup (form o).
- {c | ext ?? (rel o) c ⊆ extS ?? (rel o) a ∩ extS ?? (rel o) b });
- intros; simplify; apply (.= (†H)‡#); apply refl1.
+ ∀o:BP. 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 = (fintersectsS _ U V).
-
-(*
-definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp.
-
+interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
- apply (λo:basic_pair.λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧
- (* OK: FunClass_2_OF_binary_relation (concr o) (form o) (rel o) x y *)
- ?);
- change in x with (carr1 (setoid1_of_setoid (concr o)));
- apply (FunClass_2_OF_binary_relation ?? (rel ?) x y);
-x ⊩ y);
-
- rel (concr o) o -> binary_relation ...
- rel ? = seotid1_OF_setoid ?
- carr rel ? = Type_OF_objs1 (concr o) ->
- carr (setoid1_of_REL (concr 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);
+ | intros; split; intros; cases H2; exists [1,3: apply w]
+ [ apply (. (#‡H1)‡(H‡#)); assumption
+ | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]]
+qed.
-interpretation "basic pair relation for subsets" 'Vdash2 x y = (relS _ x y).
-interpretation "basic pair relation for subsets (non applied)" 'Vdash = (relS _).
+interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
record concrete_space : Type ≝
- { bp:> basic_pair;
+ { bp:> BP;
converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
all_covered: ∀x: concr bp. x ⊩ form bp
}.
+definition bp': concrete_space → basic_pair ≝ λc.bp c.
+
+coercion bp'.
+
record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
- { rp:> relation_pair CS1 CS2;
+ { 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));
+ extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
+ BPextS 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)
+ extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1)
}.
-definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid.
+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;
[ 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.
+definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 ? CS1 CS2 ≝
+ λCS1,CS2,c.rp ?? c.
+
+coercion rp''.
+
+lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
intros;
- unfold extS;
- split;
- [ intros 2;
- cases m; clear m;
+ unfold extS; simplify;
+ split; simplify;
+ [ intros 2; change with (a ∈ X);
+ cases f; clear f;
cases H; clear H;
- cases H1; clear H1;
- whd in H;
- apply (eq_elim_r'' ????? H);
+ cases x; clear x;
+ change in f2 with (eq1 ? a w);
+ apply (. (f2\sup -1‡#));
assumption
- | intros 2;
- constructor 1;
+ | intros 2; change in f with (a ∈ X);
+ split;
[ whd; exact I
| exists; [ apply a ]
split;
[ assumption
- | whd; constructor 1]]]
+ | change with (a = a); apply refl]]]
qed.
-definition CSPA: category.
+lemma extS_id: ∀o:basic_pair.∀X.extS (concr o) (concr o) (id o) \sub \c X = X.
+ intros;
+ unfold extS; simplify;
+ split; simplify; intros;
+ [ change with (a ∈ X);
+ cases f; cases H; cases x; change in f3 with (eq1 ? a w);
+ apply (. (f3\sup -1‡#));
+ assumption
+ | change in f with (a ∈ X);
+ split;
+ [ apply I
+ | exists; [apply a]
+ split; [ assumption | change with (a = a); apply refl]]]
+qed.
+(*
+definition CSPA: category1.
constructor 1;
[ apply concrete_space
| apply convergent_relation_space_setoid
| 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 (.= (extS_id ??));
+ apply refl1]
+ | intros; constructor 1;
+ [ intros; whd in c c1 ⊢ %;
+ constructor 1;
+ [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
+ | intros;
+ |
+ ]
+ | intros;
+ change with (a ∘ b = a' ∘ b');
+ change in H with (rp'' ?? a = rp'' ?? a');
+ change in H1 with (rp'' ?? b = rp ?? b');
+ apply (.= (H‡H1));
+ apply refl1]
+ | intros; simplify;
+ change with ((a12 ∘ a23) ∘ a34 = a12 ∘ (a23 ∘ a34));
+ apply (.= ASSOC1);
+ apply refl1
+ | intros; simplify;
+ change with (id o1 ∘ a = a);*)
\ No newline at end of file
projects / helm.git / blobdiff