From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 20 Oct 2011 13:58:55 +0000 (+0000)
Subject: JMeq lifted to work on Type[1].
X-Git-Tag: make_still_working~2168
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2343da541bb828ac61079d7811c0fe5613b04fb6;p=helm.git

JMeq lifted to work on Type[1].
---

diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma
index a520ca96f..05c13498e 100644
--- a/matita/matita/lib/basics/jmeq.ma
+++ b/matita/matita/lib/basics/jmeq.ma
@@ -11,10 +11,10 @@
 
 include "basics/logic.ma".
 
-inductive Sigma: Type[1] ≝
- mk_Sigma: ∀p1: Type[0]. p1 → Sigma.
+inductive Sigma: Type[2] ≝
+ mk_Sigma: ∀p1: Type[1]. p1 → Sigma.
 
-definition p1: Sigma → Type[0].
+definition p1: Sigma → Type[1].
  #S cases S #Y #_ @Y
 qed.
 
@@ -22,7 +22,7 @@ definition p2: ∀S:Sigma. p1 S.
  #S cases S #Y #x @x
 qed.
 
-inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝
+inductive jmeq (A:Type[1]) (x:A) : ∀B:Type[1]. B →Prop ≝
 refl_jmeq : jmeq A x A x.
 
 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
@@ -43,7 +43,7 @@ lemma K : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
 qed.
 
 definition cast:
- ∀A,B:Type[0].∀E:A=B. A → B.
+ ∀A,B:Type[1].∀E:A=B. A → B.
  #A #B #E cases E #X @X
 qed.
 
@@ -100,14 +100,14 @@ qed.
 lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
  P x (refl_jmeq A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E.
 
-lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
+lemma jmeq_to_eq: ∀A:Type[1]. ∀x,y:A. x≃y → x=y.
  #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
 qed.
 
-coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
+coercion jmeq_to_eq: ∀A:Type[1]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
 
 lemma eq_to_jmeq:
-  ∀A: Type[0].
+  ∀A: Type[1].
   ∀x, y: A.
     x = y → x ≃ y.
   //
diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index b090a8de8..a3858dfb7 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -14,14 +14,14 @@ include "hints_declaration.ma".
 
 (* propositional equality *)
 
-inductive eq (A:Type[1]) (x:A) : A → Prop ≝
+inductive eq (A:Type[2]) (x:A) : A → Prop ≝
     refl: eq A x x. 
     
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 interpretation "leibniz reflexivity" 'refl = refl.
 
 lemma eq_rect_r:
- ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → P x p.
  #A #a #x #p (cases p) // qed.
 
 lemma eq_ind_r :
@@ -38,13 +38,18 @@ lemma eq_rect_Type2_r:
   #A #a #P #H #x #p (generalize in match H) (generalize in match P)
   cases p; //; qed.
 
-theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x = y → P y.
+lemma eq_rect_Type3_r:
+  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+  cases p; //; qed.
+
+theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y.
 #A #x #P #Hx #y #Heq (cases Heq); //; qed.
 
 theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
 #A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed.
 
-theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y = x → P y.
+theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y.
 #A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
 
 theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
@@ -236,6 +241,6 @@ example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
 #A #x #h @(refl ? h: eqProp ? ? ?).
 qed.
 
-theorem streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
- #T #t #P #H #p >(lemmaK ?? p) @H
+theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
+ #T #t #P #H #p >(lemmaK T t p) @H
 qed.
diff --git a/matita/matita/lib/basics/pts.ma b/matita/matita/lib/basics/pts.ma
index 94f49fc5c..446305ecf 100644
--- a/matita/matita/lib/basics/pts.ma
+++ b/matita/matita/lib/basics/pts.ma
@@ -18,3 +18,4 @@ universe constraint Type[0] < Type[1].
 universe constraint Type[1] < Type[2].
 universe constraint Type[2] < Type[3].
 universe constraint Type[3] < Type[4].
+universe constraint Type[4] < Type[5].