o-algebra defined again

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-algebra.ma

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 }.