Categories and subsets compile again, hopefully with better universe levels.

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 5afda73d99865ae143aa257d93a1e4e006996dc4..0d5d02afbdae7fd9fef16c9d0b495ae697e974b2 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -370,6 +370,11 @@ definition prop11_SET1 :
 intros; apply (prop11 A B w a b e);
 qed.
 
+definition hint: Type_OF_category2 SET1 → Type1.
+ intro; whd in t; apply (carr1 t);
+qed.
+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).

diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index 17128ae6a97942fe7831a06baede3ce05443b1dc..7eb2d1e9423bc88f1026ccf38c1a3ac88193b8f7 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -15,10 +15,10 @@
 include "logic/cprop_connectives.ma".
 include "categories.ma".
 
-record powerset_carrier (A: SET) : Type1 ≝ { mem_operator: unary_morphism1 A CPROP }.
+record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: unary_morphism1 A CPROP }.
 
-definition subseteq_operator: ∀A: SET. powerset_carrier A → powerset_carrier A → CProp2 ≝
- λA:SET.λU,V.∀a:A. mem_operator ? U a → mem_operator ? V a.
+definition subseteq_operator: ∀A: SET. powerset_carrier A → powerset_carrier A → CProp1 ≝
+ λA:objs1 SET.λU,V.∀a:A. mem_operator ? U a → mem_operator ? V a.
 
 theorem transitive_subseteq_operator: ∀A. transitive2 ? (subseteq_operator A).
  intros 6; intros 2;
@@ -74,6 +74,8 @@ qed.
 
 interpretation "subseteq" 'subseteq U V = (fun21 ___ (subseteq _) U V).
 
+
+
 theorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S.
  intros 4; assumption.
 qed.
@@ -85,9 +87,10 @@ qed.
 definition overlaps: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
  intros;
  constructor 1;
-  [ apply (λA.λU,V:Ω \sup A.exT2 ? (λx:A.x ∈ U) (λx:A.x ∈ V))
+  (* Se metto x al posto di ? ottengo una universe inconsistency *)
+  [ apply (λA:objs1 SET.λU,V:Ω \sup A.(exT2 ? (λx:A.?(*x*) ∈ U) (λx:A.?(*x*) ∈ V) : CProp0))
   | intros;
-    constructor 1; intro; cases H; exists; [1,4: apply w]
+    constructor 1; intro; cases e2; exists; [1,4: apply w]
      [ apply (. #‡e); assumption
      | apply (. #‡e1); assumption
      | apply (. #‡(e \sup -1)); assumption;
@@ -124,6 +127,7 @@ qed.
 
 interpretation "union" 'union U V = (fun21 ___ (union _) U V).
 
+(* qua non riesco a mettere set *)
 definition singleton: ∀A:setoid. unary_morphism1 A (Ω \sup A).
  intros; constructor 1;
   [ apply (λa:A.{b | eq ? a b}); unfold setoid1_of_setoid; simplify;