From: Claudio Sacerdoti Coen Date: Sun, 4 Jan 2009 16:45:36 +0000 (+0000) Subject: Some more progress, fighting universe inconsistencies. X-Git-Tag: make_still_working~4297 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=32d2bb73b2ed863c988c61ce9d15404bb9d800ad;p=helm.git 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 3653d3a64..88af29263 100644 --- 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.