Many universe inconsistency avoided here and there.

[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 5f99153ba85d6a477b05b7280a888d112678afcb..bcd1aae1bcf6fcba2541e417fb91b4b4ed0b3677 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -60,7 +60,6 @@ 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 : Type2 := {
   oa_P :> SET1;
@@ -122,6 +121,8 @@ interpretation "o-algebra meet" 'oa_meet f =
 interpretation "o-algebra meet with explicit function" 'oa_meet_mk f = 
   (fun11 __ (oa_meet __) (mk_unary_morphism _ _ f _)).
 
+(*
+
 definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
 intros; split;
 [ intros (p q); 
@@ -316,3 +317,4 @@ split;
 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_left1;
 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_right1;]
 qed.
+*)
\ No newline at end of file