more composites to make all happy!

[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 6be19d92c31ac4518d402650c362e85dc4b3fd9b..6f58f53b242e931e37555f3f2bf3ad6d56b31985 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -48,6 +48,9 @@ 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 carr' ≝ λx:Type_OF_category1 SET.Type_OF_Type0 (carr x).
+coercion carr'. (* we prefer the lower carrier projection *)
+
 (* per il set-indexing vedere capitolo BPTools (foundational tools), Sect. 0.3.4 complete
    lattices, Definizione 0.9 *)
 (* USARE L'ESISTENZIALE DEBOLE *)
@@ -56,8 +59,8 @@ 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_meet: ∀I:SET.unary_morphism2 (I ⇒ oa_P) oa_P;
+  oa_join: ∀I:SET.unary_morphism2 (I ⇒ oa_P) oa_P;
   oa_one: oa_P;
   oa_zero: oa_P;
   oa_leq_refl: ∀a:oa_P. oa_leq a a; 
@@ -65,8 +68,8 @@ record OAlgebra : Type2 := {
   oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
   oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
   (* Errore: = in oa_meet_inf e oa_join_sup *)
-  oa_meet_inf: ∀I.∀p_i.∀p:oa_P.oa_leq p (oa_meet I p_i) → ∀i:I.oa_leq p (p_i i);
-  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_meet_inf: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq p (oa_meet I p_i) = ∀i:I.oa_leq p (p_i i);
+  oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀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;
   oa_overlap_preserves_meet_: 
@@ -74,8 +77,8 @@ record OAlgebra : Type2 := {
        (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:arrows2 SET1 I oa_P.
-       oa_overlap p (oa_join I q) ⇔ ∃i:carr I.oa_overlap p (q i);
+      ∀I:SET.∀p.∀q: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
@@ -168,7 +171,7 @@ definition hint5: OAlgebra → objs2 SET1.
 qed.
 coercion hint5.
 
-record ORelation (P,Q : OAlgebra) : Type ≝ {
+record ORelation (P,Q : OAlgebra) : Type2 ≝ {
   or_f_ : P ⇒ Q;
   or_f_minus_star_ : P ⇒ Q;
   or_f_star_ : Q ⇒ P;