From a01c3b573865dbebd3fb43c37ffeb6b7f464b4c1 Mon Sep 17 00:00:00 2001
From: Siegmentation Fault <siegmentationfault@yandex.ru>
Date: Sun, 17 Dec 2023 16:44:12 +0700
Subject: [PATCH] fix universe level of some HITs

---
 GroundZero/Algebra/EilenbergMacLane.lean |  8 ++---
 GroundZero/Exercises/Chap3.lean          |  9 ------
 GroundZero/HITs/Graph.lean               | 37 +++++++++++++++++-------
 GroundZero/Meta/Notation.lean            |  4 +--
 GroundZero/Types/Equiv.lean              |  9 ++++++
 5 files changed, 41 insertions(+), 26 deletions(-)

diff --git a/GroundZero/Algebra/EilenbergMacLane.lean b/GroundZero/Algebra/EilenbergMacLane.lean
index 3d80bf9..ffb5588 100644
--- a/GroundZero/Algebra/EilenbergMacLane.lean
+++ b/GroundZero/Algebra/EilenbergMacLane.lean
@@ -12,7 +12,7 @@ open GroundZero
 namespace GroundZero.Algebra
 universe u v
 
-hott axiom K1 (G : Group) : Type := Opaque 𝟏
+hott axiom K1 (G : Group.{u}) : Type u := Opaque 𝟏
 
 namespace K1
   variable {G : Group}
@@ -173,13 +173,13 @@ namespace K1
   end
 end K1
 
-hott def ItS (A : Type) : ℕ → Type
+hott definition ItS (A : Type u) : ℕ → Type u
 |      0     => A
 | Nat.succ n => ∑ (ItS A n)
 
 open GroundZero.HITs (Trunc)
 
-hott def K (G : Group) (n : ℕ) :=
-Trunc (hlevel.ofNat (n + 1)) (ItS (K1 G) n)
+hott definition K (G : Group) (n : ℕ) :=
+∥ItS (K1 G) n∥ₙ₊₁
 
 end GroundZero.Algebra
diff --git a/GroundZero/Exercises/Chap3.lean b/GroundZero/Exercises/Chap3.lean
index 457bd12..81b05bb 100644
--- a/GroundZero/Exercises/Chap3.lean
+++ b/GroundZero/Exercises/Chap3.lean
@@ -137,15 +137,6 @@ end «3.9»
 namespace «3.10»
   open «3.9»
 
-  inductive Resize (A : Type u) : Type (max u v)
-  | intro : A → Resize A
-
-  hott def Resize.elim {A : Type u} : Resize A → A
-  | intro w => w
-
-  hott theorem Resize.equiv (A : Type u) : A ≃ Resize.{u, v} A :=
-  ⟨Resize.intro, Qinv.toBiinv _ ⟨Resize.elim, (λ (Resize.intro _), idp _, idp)⟩⟩
-
   hott lemma Resize.prop {A : Type u} (H : prop A) : prop (Resize.{u, v} A) :=
   Structures.propRespectsEquiv.{u, max u v} (Resize.equiv A) H
 
diff --git a/GroundZero/HITs/Graph.lean b/GroundZero/HITs/Graph.lean
index 0615584..b5f4a06 100644
--- a/GroundZero/HITs/Graph.lean
+++ b/GroundZero/HITs/Graph.lean
@@ -10,36 +10,51 @@ universe u v w
 inductive Graph.rel {A : Type u} (R : A → A → Type v) : A → A → Prop
 | line {n m : A} : R n m → rel R n m
 
--- TODO: fix universe level
-hott axiom Graph {A : Type u} (R : A → A → Type v) : Type u := Quot (Graph.rel R)
+hott axiom Graph {A : Type u} (R : A → A → Type v) : Type (max u v) :=
+Resize.{u, v} (Quot (Graph.rel R))
 
 namespace Graph
   hott axiom elem {A : Type u} {R : A → A → Type w} : A → Graph R :=
-  Quot.mk (rel R)
+  Resize.intro ∘ Quot.mk (rel R)
 
   hott opaque line {A : Type u} {R : A → A → Type w} {x y : A}
-    (h : R x y) : @elem A R x = @elem A R y :=
-  trustHigherCtor (Quot.sound (rel.line h))
+    (H : R x y) : @elem A R x = @elem A R y :=
+  trustHigherCtor (congrArg Resize.intro (Quot.sound (rel.line H)))
 
   hott axiom rec {A : Type u} {B : Type v} {R : A → A → Type w}
     (f : A → B) (H : Π x y, R x y → f x = f y) : Graph R → B :=
-  λ x, Quot.withUseOf H (Quot.lift f (λ a b, λ (Graph.rel.line ε), elimEq (H a b ε)) x) x
+  λ x, Quot.withUseOf H (Quot.lift f (λ a b, λ (Graph.rel.line ε), elimEq (H a b ε)) x.elim) x.elim
 
   @[eliminator] hott axiom ind {A : Type u} {R : A → A → Type v} {B : Graph R → Type w}
     (f : Π x, B (elem x)) (ε : Π x y H, f x =[line H] f y) : Π x, B x :=
-  λ x, Quot.withUseOf ε (Quot.hrecOn x f (λ a b, λ (Graph.rel.line H), HEq.fromPathover (line H) (ε a b H))) x
+  λ x, Quot.withUseOf ε (@Quot.hrecOn A (Graph.rel R) (B ∘ Resize.intro) x.elim f
+    (λ a b, λ (Graph.rel.line H), HEq.fromPathover (line H) (ε a b H))) x.elim
 
   hott opaque recβrule {A : Type u} {B : Type v} {R : A → A → Type w}
-    (f : A → B) (h : Π x y, R x y → f x = f y) {x y : A}
-    (g : R x y) : ap (rec f h) (line g) = h x y g :=
+    (f : A → B) (ε : Π x y, R x y → f x = f y) {x y : A}
+    (g : R x y) : ap (rec f ε) (line g) = ε x y g :=
   trustCoherence
 
   hott opaque indβrule {A : Type u} {R : A → A → Type v} {B : Graph R → Type w}
-    (f : Π x, B (elem x)) (h : Π x y (H : R x y), f x =[line H] f y)
-    {x y : A} (g : R x y) : apd (ind f h) (line g) = h x y g :=
+    (f : Π x, B (elem x)) (ε : Π x y H, f x =[line H] f y)
+    {x y : A} (g : R x y) : apd (ind f ε) (line g) = ε x y g :=
   trustCoherence
 
   attribute [irreducible] Graph
+
+  section
+    variable {A : Type u} {R : A → A → Type v} {B : Graph R → Type w}
+             (f : Π x, B (elem x)) (ε₁ ε₂ : Π x y H, f x =[line H] f y)
+
+    #failure ind f ε₁ ≡ ind f ε₂
+  end
+
+  section
+    variable {A : Type u} {R : A → A → Type v} {B : Type w}
+             (f : A → B) (ε₁ ε₂ : Π x y, R x y → f x = f y)
+
+    #failure rec f ε₁ ≡ rec f ε₂
+  end
 end Graph
 
 end GroundZero.HITs
diff --git a/GroundZero/Meta/Notation.lean b/GroundZero/Meta/Notation.lean
index 34ebc73..c34486e 100644
--- a/GroundZero/Meta/Notation.lean
+++ b/GroundZero/Meta/Notation.lean
@@ -330,7 +330,7 @@ namespace Defeq
     let τ₁ ← Elab.Term.levelMVarToParam (← instantiateMVars τ₁);
     let τ₂ ← Elab.Term.levelMVarToParam (← instantiateMVars τ₂);
 
-    unless (← Meta.isDefEq τ₁ τ₂) do throwErrorAt tag s!"{← Meta.ppExpr τ₁} ≠ {← Meta.ppExpr τ₂}"
+    unless (← Meta.isDefEqGuarded τ₁ τ₂) do throwErrorAt tag s!"{← Meta.ppExpr τ₁} ≠ {← Meta.ppExpr τ₂}"
   }
 
   elab "#failure " σ₁:term tag:" ≡ " σ₂:term τ:(typeSpec)? : command =>
@@ -343,7 +343,7 @@ namespace Defeq
     let τ₁ ← Elab.Term.levelMVarToParam (← instantiateMVars τ₁);
     let τ₂ ← Elab.Term.levelMVarToParam (← instantiateMVars τ₂);
 
-    if (← Meta.isDefEq τ₁ τ₂) then throwErrorAt tag s!"{← Meta.ppExpr τ₁} ≡ {← Meta.ppExpr τ₂}"
+    if (← Meta.isDefEqGuarded τ₁ τ₂) then throwErrorAt tag s!"{← Meta.ppExpr τ₁} ≡ {← Meta.ppExpr τ₂}"
   }
 end Defeq
 
diff --git a/GroundZero/Types/Equiv.lean b/GroundZero/Types/Equiv.lean
index 12a3c2e..8680ae8 100644
--- a/GroundZero/Types/Equiv.lean
+++ b/GroundZero/Types/Equiv.lean
@@ -986,4 +986,13 @@ namespace Equiv
   | Nat.succ n, α, β => @bimapCharacterizationΩ₂ (a = a) (b = b) (f a b = f a b) (bimap f) (idp a) (idp b) n α β
 end Equiv
 
+inductive Resize (A : Type u) : Type (max u v)
+| intro : A → Resize A
+
+hott definition Resize.elim {A : Type u} : Resize A → A
+| intro w => w
+
+hott theorem Resize.equiv (A : Type u) : A ≃ Resize.{u, v} A :=
+Equiv.intro Resize.intro Resize.elim idp idp
+
 end GroundZero.Types