From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 28 Dec 2008 14:32:18 +0000 (+0000)
Subject: Categories and subsets compile again, hopefully with better universe levels.
X-Git-Tag: make_still_working~4318
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2972fbccd5da862610f1bfa61973b997ce6eed7b;p=helm.git

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 5afda73d9..0d5d02afb 100644
--- 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 17128ae6a..7eb2d1e94 100644
--- 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;