refactor(builtin/heq): cleanup universes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/cast.lean

@@ -1,10 +1,10 @@
 import heq
 
-variable cast {A B : TypeH} : A = B → A → B
+variable cast {A B : TypeM} : A = B → A → B
 
-axiom cast_heq {A B : TypeH} (H : A = B) (a : A) : cast H a == a
+axiom cast_heq {A B : TypeM} (H : A = B) (a : A) : cast H a == a
 
-theorem cast_app {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} (f : ∀ x, B x) (a : A) (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) :
+theorem cast_app {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} (f : ∀ x, B x) (a : A) (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) :
       cast Hb f (cast Ha a) == f a
 := let s1 : cast Hb f == f  := cast_heq Hb f,
        s2 : cast Ha a == a  := cast_heq Ha a
@@ -12,24 +12,18 @@ theorem cast_app {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} (f : ∀ x
 
 -- The following theorems can be used as rewriting rules
 
-theorem cast_eq {A : TypeH} (H : A = A) (a : A) : cast H a = a
+theorem cast_eq {A : TypeM} (H : A = A) (a : A) : cast H a = a
 := to_eq (cast_heq H a)
 
-theorem cast_trans {A B C : TypeH} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a
+theorem cast_trans {A B C : TypeM} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a
 := let s1 : cast Hbc (cast Hab a)  == cast Hab a              :=  cast_heq Hbc (cast Hab a),
        s2 : cast Hab a             == a                       :=  cast_heq Hab a,
        s3 : cast (trans Hab Hbc) a == a                       :=  cast_heq (trans Hab Hbc) a,
        s4 : cast Hbc (cast Hab a)  == cast (trans Hab Hbc) a  :=  htrans (htrans s1 s2) (hsymm s3)
    in to_eq s4
 
-theorem cast_pull {A : TypeH} {B B' : A → TypeH} (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) :
+theorem cast_pull {A : TypeM} {B B' : A → TypeM} (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) :
       cast Hb f a = cast Hba (f a)
 := let s1 : cast Hb f a    == f a    :=  hcongr (cast_heq Hb f) (hrefl a),
        s2 : cast Hba (f a) == f a    :=  cast_heq Hba (f a)
    in to_eq (htrans s1 (hsymm s2))
-
-
-
-
-
-

src/builtin/heq.lean

@@ -4,33 +4,38 @@ import macros
 variable heq {A B : TypeU} : A → B → Bool
 infixl 50 == : heq
 
-universe H ≥ 1
-universe U ≥ H + 1
-definition TypeH := (Type H)
+axiom heq_eq {A : TypeU} (a b : A) : a == b ↔ a = b
 
-axiom heq_eq {A : TypeH} (a b : A) : a == b ↔ a = b
-
-definition to_eq {A : TypeH} {a b : A} (H : a == b) : a = b
+definition to_eq {A : TypeU} {a b : A} (H : a == b) : a = b
 := (heq_eq a b) ◂ H
 
-definition to_heq {A : TypeH} {a b : A} (H : a = b) : a == b
+definition to_heq {A : TypeU} {a b : A} (H : a = b) : a == b
 := (symm (heq_eq a b)) ◂ H
 
-theorem hrefl {A : TypeH} (a : A) : a == a
+theorem hrefl {A : TypeU} (a : A) : a == a
 := to_heq (refl a)
 
-axiom hsymm {A B : TypeH} {a : A} {b : B} : a == b → b == a
+axiom hsymm {A B : TypeU} {a : A} {b : B} : a == b → b == a
 
-axiom htrans {A B C : TypeH} {a : A} {b : B} {c : C} : a == b → b == c → a == c
+axiom htrans {A B C : TypeU} {a : A} {b : B} {c : C} : a == b → b == c → a == c
 
-axiom hcongr {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} :
+axiom hcongr {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} :
       f == f' → a == a' → f a == f' a'
 
-axiom hfunext {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} {f : ∀ x, B x} {f' : ∀ x, B' x} :
+universe M ≥ 1
+universe U ≥ M + 1
+definition TypeM := (Type M)
+
+-- In the following definitions the type of A and A' cannot be TypeU
+-- because A = A' would be @eq (Type U+1) A A', and
+-- the type of eq is (∀T : (Type U), T → T → bool).
+-- So, we define M a universe smaller than U.
+
+axiom hfunext {A A' : TypeM} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} :
       A = A' → (∀ x x', x == x' → f x == f' x') → f == f'
 
-axiom hpiext {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} :
+axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} :
       A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x)
 
-axiom hallext {A A' : TypeH} {B : A → Bool} {B' : A' → Bool} :
+axiom hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} :
       A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x)