o-algebra defined again

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 0d5d02afbdae7fd9fef16c9d0b495ae697e974b2..655c5076034328872447c628855bf65b1479dba9 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -100,6 +100,20 @@ record setoid2: Type3 ≝
    eq2: equivalence_relation2 carr2
  }.
 
+definition setoid2_of_setoid1: setoid1 → setoid2.
+ intro;
+ constructor 1;
+  [ apply (carr1 s)
+  | constructor 1;
+    [ apply (eq_rel1 s);
+      apply (eq1 s)
+    | apply (refl1 s)
+    | apply (sym1 s)
+    | apply (trans1 s)]]
+qed.
+
+coercion setoid2_of_setoid1.
+
 (*
 definition Leibniz: Type → setoid.
  intro;
@@ -182,6 +196,7 @@ definition CPROP: setoid1.
         [ apply (H4 (H2 x1)) | apply (H3 (H5 z1))]]]
 qed.
 
+alias symbol "eq" = "setoid1 eq".
 definition if': ∀A,B:CPROP. A = B → A → B.
  intros; apply (if ?? e); assumption.
 qed.
@@ -287,7 +302,7 @@ definition unary_morphism_setoid: setoid → setoid → setoid.
  constructor 1;
   [ apply (unary_morphism s s1);
   | constructor 1;
-     [ intros (f g); apply (∀a:s. f a = g a);
+     [ intros (f g); apply (∀a:s. eq ? (f a) (g a));
      | intros 1; simplify; intros; apply refl;
      | simplify; intros; apply sym; apply H;
      | simplify; intros; apply trans; [2: apply H; | skip | apply H1]]]
@@ -336,7 +351,9 @@ definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid2.
  constructor 1;
   [ apply (unary_morphism1 s s1);
   | constructor 1;
-     [ intros (f g); apply (∀a: carr1 s. f a = g a);
+     [ intros (f g);
+       alias symbol "eq" = "setoid1 eq".
+       apply (∀a: carr1 s. f a = g a);
      | intros 1; simplify; intros; apply refl1;
      | simplify; intros; apply sym1; apply H;
      | simplify; intros; apply trans1; [2: apply H; | skip | apply H1]]]
@@ -378,4 +395,4 @@ coercion hint.
 interpretation "SET dagger" 'prop1 h = (prop11_SET1 _ _ _ _ _ h).
 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
 interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b).
-interpretation "SET1 eq" 'eq x y = (eq_rel1 _ (eq'' _) x y).
\ No newline at end of file
+interpretation "SET1 eq" 'eq x y = (eq_rel1 _ (eq'' _) x y).

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index 617c58b602c12c06431457c4fad0d984bb162dbc..5f99153ba85d6a477b05b7280a888d112678afcb 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -27,12 +27,12 @@ constructor 1; [apply bool] constructor 1;
 qed.
 
 lemma IF_THEN_ELSE_p :
-  ∀S:setoid.∀a,b:S.∀x,y:BOOL.x = y → 
+  ∀S:setoid1.∀a,b:S.∀x,y:BOOL.x = y → 
     (λm.match m with [ true ⇒ a | false ⇒ b ]) x =
     (λm.match m with [ true ⇒ a | false ⇒ b ]) y.
 whd in ⊢ (?→?→?→%→?);
-intros; cases x in H; cases y; simplify; intros; try apply refl; whd in H; cases H;
-qed. 
+intros; cases x in e; cases y; simplify; intros; try apply refl1; whd in e; cases e;
+qed.
 
 interpretation "unary morphism comprehension with no proof" 'comprehension T P = 
   (mk_unary_morphism T _ P _).
@@ -49,20 +49,25 @@ interpretation "unary morphism comprehension with proof" 'comprehension_by s \et
 interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \eta.f p = 
   (mk_unary_morphism1 s _ f p).
 
-definition Type_of_SET: SET → Type0 := λS.carr S.
-coercion Type_of_SET.
+definition hint: Type_OF_category2 SET1 → setoid2.
+ intro; apply (setoid2_of_setoid1 t); qed.
+coercion hint.
+
+definition hint2: Type_OF_category1 SET → objs2 SET1.
+ intro; apply (setoid1_of_setoid t); qed.
+coercion hint2.
 
 (* per il set-indexing vedere capitolo BPTools (foundational tools), Sect. 0.3.4 complete
    lattices, Definizione 0.9 *)
 (* USARE L'ESISTENZIALE DEBOLE *)
 (* Far salire SET usando setoidi1 *)
-alias symbol "comprehension_by" = "unary morphism comprehension with proof".
-record OAlgebra : Type1 := {
-  oa_P :> SET;
-  oa_leq : binary_morphism1 (setoid1_of_setoid oa_P) (setoid1_of_setoid oa_P) CPROP; (* CPROP is setoid1, CPROP importante che sia small *)
-  oa_overlap: binary_morphism1 (setoid1_of_setoid oa_P) (setoid1_of_setoid oa_P) CPROP;
-  oa_meet: ∀I:SET.unary_morphism1 (arrows1 SET I oa_P) (setoid1_of_setoid oa_P);
-  oa_join: ∀I:SET.unary_morphism1 (arrows1 SET I oa_P) (setoid1_of_setoid oa_P);
+(*alias symbol "comprehension_by" = "unary morphism comprehension with proof".*)
+record OAlgebra : Type2 := {
+  oa_P :> SET1;
+  oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1, CPROP importante che sia small *)
+  oa_overlap: binary_morphism1 oa_P oa_P CPROP;
+  oa_meet: ∀I:SET.unary_morphism2 (arrows2 SET1 I oa_P) oa_P;
+  oa_join: ∀I:SET.unary_morphism2 (arrows2 SET1 I oa_P) oa_P;
   oa_one: oa_P;
   oa_zero: oa_P;
   oa_leq_refl: ∀a:oa_P. oa_leq a a; 
@@ -74,13 +79,13 @@ record OAlgebra : Type1 := {
   oa_join_sup: ∀I.∀p_i.∀p:oa_P.oa_leq (oa_join I p_i) p → ∀i:I.oa_leq (p_i i) p;
   oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
   oa_one_top: ∀p:oa_P.oa_leq p oa_one;
-  (* preservers!! (typo) *)
-  oa_overlap_preservers_meet_: 
+  oa_overlap_preserves_meet_: 
       ∀p,q:oa_P.oa_overlap p q → oa_overlap p 
        (oa_meet ? { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q });
   (* ⇔ deve essere =, l'esiste debole *)
   oa_join_split:
-      ∀I:SET.∀p.∀q:arrows1 SET I oa_P.oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i);
+      ∀I:SET.∀p.∀q:arrows2 SET1 I oa_P.
+       oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i);
   (*oa_base : setoid;
   1) enum non e' il nome giusto perche' non e' suriettiva
   2) manca (vedere altro capitolo) la "suriettivita'" come immagine di insiemi di oa_base
@@ -91,11 +96,11 @@ record OAlgebra : Type1 := {
       ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
 }.
 
-interpretation "o-algebra leq" 'leq a b = (fun1 ___ (oa_leq _) a b).
+interpretation "o-algebra leq" 'leq a b = (fun21 ___ (oa_leq _) a b).
 
 notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
 for @{ 'overlap $a $b}.
-interpretation "o-algebra overlap" 'overlap a b = (fun1 ___ (oa_overlap _) a b).
+interpretation "o-algebra overlap" 'overlap a b = (fun22 ___ (oa_overlap _) a b).
 
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" 
 non associative with precedence 50 for @{ 'oa_meet $p }.