Some more progress, fighting universe inconsistencies.

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
index 3653d3a643e3d4912a4d6bdffee62c260545366a..88af2926367242ba18372fd91060b8af9e81fe8b 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
@@ -58,15 +58,17 @@ definition composition:
     exists; try assumption;
     split; assumption]
 qed.
-axiom daemon: False.
+
 definition REL: category1.
  constructor 1;
   [ apply setoid
   | intros (T T1); apply (binary_relation_setoid T T1)
   | intros; constructor 1;
     constructor 1; unfold setoid1_of_setoid; simplify;
-     [ change with (carr o → carr o → CProp); intros; apply (eq1 ? c c1) ]] cases daemon; qed.
-     | intros; split; intro;
+     [ (* changes required to avoid universe inconsistency *)
+       change with (carr o → carr o → CProp); intros; apply (eq ? c c1)
+     | intros; split; intro; change in a a' b b' with (carr o);
+       change in e with (eq ? a a'); change in e1 with (eq ? b b');
         [ apply (.= (e ^ -1));
           apply (.= e2);
           apply e1
@@ -88,7 +90,10 @@ definition REL: category1.
         [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold;
           [ apply (. (e ^ -1 : eq1 ? w x)‡#); assumption
           | apply (. #‡(e : eq1 ? w y)); assumption]
-        |2,4: exists; try assumption; split; first [apply refl1 | assumption]]]
+        |2,4: exists; try assumption; split;
+          (* change required to avoid universe inconsistency *)
+          change in x with (carr o1); change in y with (carr o2);
+          first [apply refl | assumption]]]
 qed.
 
 definition full_subset: ∀s:REL. Ω \sup s.