Concrete spaces do form a category, after all :-)

diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma
index 3ee8649374e598918cfb24477a439f09089c62fd..63aedcd61d728befe28b0cc89795dc8a0a9a82ea 100644 (file)
--- a/helm/software/matita/library/formal_topology/basic_pairs.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs.ma
@@ -76,7 +76,7 @@ lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → ⊩ \cir
   ]
 qed.
 
-definition id: ∀o:basic_pair. relation_pair o o.
+definition id_relation_pair: ∀o:basic_pair. relation_pair o o.
  intro;
  constructor 1;
   [1,2: apply id1;
@@ -119,17 +119,17 @@ definition BP: category1.
  constructor 1;
   [ apply basic_pair
   | apply relation_pair_setoid
-  | apply id
+  | apply id_relation_pair
   | apply relation_pair_composition
   | intros;
     change with (a12\sub\c ∘ a23\sub\c ∘ a34\sub\c ∘ ⊩ =
                  (a12\sub\c ∘ (a23\sub\c ∘ a34\sub\c) ∘ ⊩));
     apply (ASSOC1‡#);
   | intros;
-    change with ((id o1)\sub\c ∘ a\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
+    change with ((id_relation_pair o1)\sub\c ∘ a\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
     apply ((id_neutral_left1 ????)‡#);
   | intros;
-    change with (a\sub\c ∘ (id o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
+    change with (a\sub\c ∘ (id_relation_pair o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
     apply ((id_neutral_right1 ????)‡#);
   ]
 qed.
\ No newline at end of file

diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index 175f9fbb8e71b4ebc69bb873ebefd2b127f8757f..462eefd00588a0bc2c436c04135ffddec976e44b 100644 (file)
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -124,7 +124,7 @@ definition convergent_relation_space_setoid: concrete_space → concrete_space 
      | intros 3; apply trans1]]
 qed.
 
-definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 ? CS1 CS2 ≝
+definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝
  λCS1,CS2,c.rp ?? c.
 
 coercion rp''.
@@ -149,7 +149,7 @@ lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
         | change with (a = a); apply refl]]]
 qed.
 
-lemma extS_id: ∀o:basic_pair.∀X.extS (concr o) (concr o) (id o) \sub \c X = X.
+lemma extS_id: ∀o:BP.∀X.extS (concr o) (concr o) (id1 ? o) \sub \c X = X.
  intros;
  unfold extS; simplify;
  split; simplify; intros;
@@ -163,13 +163,59 @@ lemma extS_id: ∀o:basic_pair.∀X.extS (concr o) (concr o) (id o) \sub \c X =
      | exists; [apply a]
        split; [ assumption | change with (a = a); apply refl]]]
 qed.
-(*
+
+lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c1 ∘ c2) S = extS o1 o2 c1 (extS o2 o3 c2 S).
+ intros; unfold extS; simplify; split; intros; simplify; intros;
+  [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
+    cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6;
+    exists; [apply w1] split [2: assumption] constructor 1; [assumption]
+    exists; [apply w] split; assumption
+  | cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
+    cases H3 (H4 H5); cases H4 (w1 H6); clear H3 H4; cases H6 (w2 H7); clear H6;
+    cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split;
+    assumption]
+qed.
+
+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 (c \sub \c ∘ c1 \sub \c);
+          change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
+            with (c \sub \f ∘ c1 \sub \f);
+          change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
+            with (c \sub \f ∘ c1 \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 (c \sub \c ∘ c1 \sub \c);
+          apply (.= (extS_com ??????));
+          apply (.= (†(respects_all_covered ???)));
+          apply (.= respects_all_covered ???);
+          apply refl1]
+     | 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]
+qed.
+
 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 ??));
@@ -178,22 +224,17 @@ definition CSPA: category1.
        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]
+  | apply convergent_relation_space_composition
   | 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
+    change with (id1 ? o1 ∘ a = a);
+    apply (.= id_neutral_left1 ????);
+    apply refl1
+  | intros; simplify;
+    change with (a ∘ id1 ? o2 = a);
+    apply (.= id_neutral_right1 ????);
+    apply refl1]
+qed.
\ No newline at end of file