From 198bef591685fe1af7ee7f3ad147ea0d300db47c Mon Sep 17 00:00:00 2001
From: Siegmentation Fault <siegmentationfault@yandex.ru>
Date: Fri, 29 Dec 2023 14:04:18 +0700
Subject: [PATCH] formatting

---
 GroundZero/Exercises/Chap1.lean | 113 ++++++++++++++++----------------
 GroundZero/Exercises/Chap2.lean |  58 ++++++++--------
 GroundZero/Exercises/Chap3.lean |  57 ++++++++--------
 GroundZero/Exercises/Chap4.lean |  22 +++----
 4 files changed, 125 insertions(+), 125 deletions(-)

diff --git a/GroundZero/Exercises/Chap1.lean b/GroundZero/Exercises/Chap1.lean
index f341f70..fab38d0 100644
--- a/GroundZero/Exercises/Chap1.lean
+++ b/GroundZero/Exercises/Chap1.lean
@@ -13,13 +13,13 @@ universe u v w k
 
 -- exercise 1.1
 
-hott def compAssoc {A : Type u} {B : Type v} {C : Type w} {D : Type k}
+hott exercise compAssoc {A : Type u} {B : Type v} {C : Type w} {D : Type k}
   (f : A → B) (g : B → C) (h : C → D) : h ∘ (g ∘ f) = (h ∘ g) ∘ f :=
 by reflexivity
 
 -- exercise 1.2
 
-hott def Product.rec' {A : Type u} {B : Type v} {C : Type w}
+hott definition Product.rec' {A : Type u} {B : Type v} {C : Type w}
   (φ : A → B → C) : A × B → C :=
 λ u, φ u.1 u.2
 
@@ -27,7 +27,7 @@ hott example {A : Type u} {B : Type v} {C : Type w}
   (φ : A → B → C) (a : A) (b : B) : Product.rec' φ (a, b) = φ a b :=
 by reflexivity
 
-hott def Sigma.rec' {A : Type u} {B : A → Type v} {C : Type w}
+hott definition Sigma.rec' {A : Type u} {B : A → Type v} {C : Type w}
   (φ : Π x, B x → C) : (Σ x, B x) → C :=
 λ u, φ u.1 u.2
 
@@ -37,7 +37,7 @@ by reflexivity
 
 -- exercise 1.3
 
-hott def Product.ind' {A : Type u} {B : Type v} {C : A × B → Type w}
+hott definition Product.ind' {A : Type u} {B : Type v} {C : A × B → Type w}
   (φ : Π a b, C (a, b)) : Π x, C x :=
 λ u, transport C (Product.uniq u) (φ u.1 u.2)
 
@@ -45,7 +45,7 @@ hott example {A : Type u} {B : Type v} {C : A × B → Type w}
   (φ : Π a b, C (a, b)) (a : A) (b : B) : Product.ind' φ (a, b) = φ a b :=
 by reflexivity
 
-hott def Sigma.ind' {A : Type u} {B : A → Type v} {C : (Σ x, B x) → Type w}
+hott definition Sigma.ind' {A : Type u} {B : A → Type v} {C : (Σ x, B x) → Type w}
   (φ : Π a b, C ⟨a, b⟩) : Π x, C x :=
 λ u, transport C (Sigma.uniq u) (φ u.1 u.2)
 
@@ -55,76 +55,75 @@ by reflexivity
 
 -- exercise 1.4
 
-hott def Nat.iter {C : Type u} (c₀ : C) (cₛ : C → C) : ℕ → C
+hott definition Nat.iter {C : Type u} (c₀ : C) (cₛ : C → C) : ℕ → C
 | Nat.zero   => c₀
 | Nat.succ n => cₛ (iter c₀ cₛ n)
 
-hott def grec {C : Type u} (c₀ : C) (cₛ : ℕ → C → C) : ℕ → ℕ × C :=
+hott definition grec {C : Type u} (c₀ : C) (cₛ : ℕ → C → C) : ℕ → ℕ × C :=
 @Nat.iter (ℕ × C) (0, c₀) (λ u, (u.1 + 1, cₛ u.1 u.2))
 
-hott def grec.stable {C : Type u} (c₀ : C) (cₛ : ℕ → C → C) :
-  Π n, (grec c₀ cₛ n).1 = n
+hott definition grec.stable {C : Type u} (c₀ : C) (cₛ : ℕ → C → C) : Π n, (grec c₀ cₛ n).1 = n
 | Nat.zero   => idp 0
 | Nat.succ n => ap Nat.succ (stable c₀ cₛ n)
 
 section
   variable {C : Type u} (c₀ : C) (cₛ : ℕ → C → C)
 
-  hott def Nat.rec' : ℕ → C := Prod.pr₂ ∘ grec c₀ cₛ
+  hott definition Nat.rec' : ℕ → C := Prod.pr₂ ∘ grec c₀ cₛ
 
-  hott def Nat.iterB₁ : Nat.rec' c₀ cₛ 0 = c₀ :=
+  hott definition Nat.iterβ₁ : Nat.rec' c₀ cₛ 0 = c₀ :=
   by reflexivity
 
-  hott def Nat.iterB₂ (n : ℕ) : Nat.rec' c₀ cₛ (n + 1) = cₛ n (Nat.rec' c₀ cₛ n) :=
+  hott definition Nat.iterβ₂ (n : ℕ) : Nat.rec' c₀ cₛ (n + 1) = cₛ n (Nat.rec' c₀ cₛ n) :=
   ap (λ m, cₛ m (Nat.rec' c₀ cₛ n)) (grec.stable c₀ cₛ n)
 end
 
 -- exercise 1.5
 
-hott def Coproduct' (A B : Type u) :=
+hott definition Coproduct' (A B : Type u) :=
 Σ (x : 𝟐), Bool.elim A B x
 
 namespace Coproduct'
   variable {A B : Type u}
 
-  def inl {A B : Type u} (a : A) : Coproduct' A B := ⟨false, a⟩
-  def inr {A B : Type u} (b : B) : Coproduct' A B := ⟨true,  b⟩
+  hott definition inl {A B : Type u} (a : A) : Coproduct' A B := ⟨false, a⟩
+  hott definition inr {A B : Type u} (b : B) : Coproduct' A B := ⟨true,  b⟩
 
   variable (C : Coproduct' A B → Type v) (u : Π a, C (inl a)) (v : Π b, C (inr b))
 
-  hott def ind : Π x, C x
+  hott definition ind : Π x, C x
   | ⟨false, a⟩ => u a | ⟨true, b⟩ => v b
 
-  hott def indβ₁ (a : A) : ind C u v (inl a) = u a :=
+  hott definition indβ₁ (a : A) : ind C u v (inl a) = u a :=
   by reflexivity
 
-  hott def indβ₂ (b : B) : ind C u v (inr b) = v b :=
+  hott definition indβ₂ (b : B) : ind C u v (inr b) = v b :=
   by reflexivity
 end Coproduct'
 
 -- exercise 1.6
 
-hott def Product' (A B : Type u) :=
+hott definition Product' (A B : Type u) :=
 Π (x : 𝟐), Bool.elim A B x
 
 namespace Product'
   variable {A B : Type u}
 
-  def mk (a : A) (b : B) : Product' A B :=
+  hott definition mk (a : A) (b : B) : Product' A B :=
   (@Bool.casesOn (Bool.elim A B) · a b)
 
-  def pr₁ : Product' A B → A := λ u, u false
-  def pr₂ : Product' A B → B := λ u, u true
+  hott definition pr₁ : Product' A B → A := λ u, u false
+  hott definition pr₂ : Product' A B → B := λ u, u true
 
-  def η (x : Product' A B) : mk (pr₁ x) (pr₂ x) = x :=
+  hott definition η (x : Product' A B) : mk (pr₁ x) (pr₂ x) = x :=
   begin apply Theorems.funext; intro b; induction b using Bool.casesOn <;> reflexivity end
 
   variable (π : Product' A B → Type v) (φ : Π a b, π (mk a b))
 
-  hott def ind : Π x, π x :=
+  hott definition ind : Π x, π x :=
   λ x, transport π (η x) (φ (pr₁ x) (pr₂ x))
 
-  hott def indβ (a : A) (b : B) : ind π φ (mk a b) = φ a b :=
+  hott definition indβ (a : A) (b : B) : ind π φ (mk a b) = φ a b :=
   begin
     transitivity; apply ap (transport π · (φ a b));
     transitivity; apply ap Theorems.funext; change _ = (λ x, idp (mk a b x));
@@ -135,11 +134,11 @@ end Product'
 
 -- exercise 1.7
 
-hott def Ind :=
+hott definition Ind :=
 Π (A : Type u) (C : Π x y, x = y → Type v),
   (Π x, C x x (idp x)) → Π (x y : A) (p : x = y), C x y p
 
-hott def Ind' :=
+hott definition Ind' :=
 Π (A : Type u) (a : A) (C : Π x, a = x → Type v),
   C a (idp a) → Π (x : A) (p : a = x), C x p
 
@@ -149,61 +148,61 @@ hott example (φ : Ind.{u, max u (v + 1)}) : Ind'.{u, v} :=
   (λ x C d, d) a x p C c
 
 -- lemma 2.3.1
-hott def Transport :=
+hott definition Transport :=
 Π (A : Type u) (P : A → Type v) (a b : A) (p : a = b), P a → P b
 
 -- lemma 3.11.8
-hott def SinglContr :=
+hott definition SinglContr :=
 Π (A : Type u) (a b : A) (p : a = b), @Id (singl a) ⟨a, idp a⟩ ⟨b, p⟩
 
-hott def Ind.transport (φ : Ind.{u, v}) : Transport.{u, v} :=
+hott definition Ind.transport (φ : Ind.{u, v}) : Transport.{u, v} :=
 λ A P, φ A (λ x y p, P x → P y) (λ x d, d)
 
-hott def Ind.singlContr (φ : Ind.{u, u}) : SinglContr.{u} :=
+hott definition Ind.singlContr (φ : Ind.{u, u}) : SinglContr.{u} :=
 λ A a b p, φ A (λ x y p, @Id (singl x) ⟨x, idp x⟩ ⟨y, p⟩) (λ _, idp _) a b p
 
-hott def Ind.based (φ : Ind.{u, u}) : Ind'.{u, u} :=
+hott definition Ind.based (φ : Ind.{u, u}) : Ind'.{u, u} :=
 λ A a C c x p, Ind.transport φ (singl a) (λ d, C d.1 d.2)
   ⟨a, idp a⟩ ⟨x, p⟩ (Ind.singlContr φ A a x p) c
 
 -- exercise 1.8
 
 namespace Nat'
-  def ind (C : ℕ → Type u) (c₀ : C 0) (cₛ : Π n, C n → C (n + 1)) : Π n, C n
+  hott definition ind (C : ℕ → Type u) (c₀ : C 0) (cₛ : Π n, C n → C (n + 1)) : Π n, C n
   | Nat.zero   => c₀
   | Nat.succ n => cₛ n (ind C c₀ cₛ n)
 
-  def rec {C : Type u} (c₀ : C) (cₛ : ℕ → C → C) : ℕ → C :=
+  hott definition rec {C : Type u} (c₀ : C) (cₛ : ℕ → C → C) : ℕ → C :=
   ind (λ _, C) c₀ cₛ
 
-  def add : ℕ → ℕ → ℕ :=
+  hott definition add : ℕ → ℕ → ℕ :=
   λ n, rec n (λ _, Nat.succ)
 
-  def mult : ℕ → ℕ → ℕ :=
+  hott definition mult : ℕ → ℕ → ℕ :=
   λ n, rec 0 (λ _, add n)
 
-  def exp : ℕ → ℕ → ℕ :=
+  hott definition exp : ℕ → ℕ → ℕ :=
   λ n, rec 1 (λ _, mult n)
 
-  hott def addZero : Π n, add n 0 = n := idp
+  hott definition addZero : Π n, add n 0 = n := idp
 
-  hott def zeroAdd : Π n, add 0 n = n :=
+  hott definition zeroAdd : Π n, add 0 n = n :=
   ind (λ n, add 0 n = n) (idp 0) (λ n p, ap Nat.succ p)
 
-  hott def succAdd : Π n m, add (n + 1) m = add n m + 1 :=
+  hott definition succAdd : Π n m, add (n + 1) m = add n m + 1 :=
   λ n, ind (λ m, add (n + 1) m = add n m + 1) (idp (n + 1)) (λ m p, ap Nat.succ p)
 
-  hott def addComm : Π n m, add n m = add m n :=
+  hott definition addComm : Π n m, add n m = add m n :=
   λ n, ind (λ m, add n m = add m n) (zeroAdd n)⁻¹
     (λ m p, (ap Nat.succ p) ⬝ (succAdd m n)⁻¹)
 
-  hott def addAssoc : Π n m k, add n (add m k) = add (add n m) k :=
+  hott definition addAssoc : Π n m k, add n (add m k) = add (add n m) k :=
   λ n m, ind (λ k, add n (add m k) = add (add n m) k) (idp (add n m)) (λ k p, ap Nat.succ p)
 
-  hott def oneMul : Π n, mult 1 n = n :=
+  hott definition oneMul : Π n, mult 1 n = n :=
   ind (λ n, mult 1 n = n) (idp 0) (λ n p, (addComm 1 (mult 1 n)) ⬝ ap Nat.succ p)
 
-  hott def succMul : Π n m, mult (n + 1) m = add m (mult n m) :=
+  hott definition succMul : Π n m, mult (n + 1) m = add m (mult n m) :=
   λ n, ind (λ m, mult (n + 1) m = add m (mult n m)) (idp 0) (λ m p, calc
     mult (n + 1) (m + 1) = add n (mult (n + 1) m) + 1   : succAdd n (mult (n + 1) m)
                      ... = add n (add m (mult n m)) + 1 : ap (λ k, add n k + 1) p
@@ -212,32 +211,32 @@ namespace Nat'
                      ... = add m (add n (mult n m)) + 1 : ap Nat.succ (addAssoc m n (mult n m))⁻¹
                      ... = add (m + 1) (mult n (m + 1)) : (succAdd m (mult n (m + 1)))⁻¹)
 
-  hott def mulOne : Π n, mult n 1 = n :=
+  hott definition mulOne : Π n, mult n 1 = n :=
   ind (λ n, mult n 1 = n) (idp 0) (λ n p,
     (succMul n 1) ⬝ (addComm 1 (mult n 1)) ⬝ ap Nat.succ p)
 
-  hott def mulZero : Π n, mult n 0 = 0 := λ _, idp 0
+  hott definition mulZero : Π n, mult n 0 = 0 := λ _, idp 0
 
-  hott def zeroMul : Π n, mult 0 n = 0 :=
+  hott definition zeroMul : Π n, mult 0 n = 0 :=
   ind (λ n, mult 0 n = 0) (idp 0) (λ n p, zeroAdd (mult 0 n) ⬝ p)
 
-  hott def mulComm : Π n m, mult n m = mult m n :=
+  hott definition mulComm : Π n m, mult n m = mult m n :=
   λ n, ind (λ m, mult n m = mult m n) (zeroMul n)⁻¹
     (λ m p, ap (add n) p ⬝ (succMul m n)⁻¹)
 
-  hott def mulDistrLeft : Π n m k, mult n (add m k) = add (mult n m) (mult n k) :=
+  hott definition mulDistrLeft : Π n m k, mult n (add m k) = add (mult n m) (mult n k) :=
   λ n m, ind (λ k, mult n (add m k) = add (mult n m) (mult n k)) (idp (mult n m)) (λ k p, calc
       mult n (add m (k + 1)) = add n (add (mult n m) (mult n k)) : ap (add n) p
                          ... = add (add (mult n m) (mult n k)) n : addComm _ _
                          ... = add (mult n m) (add (mult n k) n) : (addAssoc _ _ _)⁻¹
                          ... = add (mult n m) (mult n (k + 1))   : ap (add (mult n m)) (addComm _ _))
 
-  hott def mulDistrRight : Π n m k, mult (add n m) k = add (mult n k) (mult m k) :=
+  hott definition mulDistrRight : Π n m k, mult (add n m) k = add (mult n k) (mult m k) :=
   λ n m k, calc mult (add n m) k = mult k (add n m)          : mulComm _ _
                              ... = add (mult k n) (mult k m) : mulDistrLeft _ _ _
                              ... = add (mult n k) (mult m k) : bimap add (mulComm _ _) (mulComm _ _)
 
-  hott def mulAssoc : Π n m k, mult n (mult m k) = mult (mult n m) k :=
+  hott definition mulAssoc : Π n m k, mult n (mult m k) = mult (mult n m) k :=
   λ n m, ind (λ k, mult n (mult m k) = mult (mult n m) k) (idp 0) (λ k p, calc
     mult n (mult m (k + 1)) = add (mult n m) (mult n (mult m k)) : mulDistrLeft _ _ _
                         ... = add (mult n m) (mult (mult n m) k) : ap (add (mult n m)) p
@@ -246,18 +245,18 @@ end Nat'
 
 -- exercise 1.9
 
-def fin (n : ℕ) : Type := Σ m, m + 1 ≤ n
+hott definition fin (n : ℕ) : Type := Σ m, m + 1 ≤ n
 
-hott def fin.fmax (n : ℕ) : fin (n + 1) :=
+hott definition fin.fmax (n : ℕ) : fin (n + 1) :=
 ⟨n, Theorems.Nat.max.refl (n + 1)⟩
 
 -- exercise 1.10
 
 namespace Nat'
-  hott def iterate {A : Type u} (f : A → A) : ℕ → (A → A) :=
+  hott definition iterate {A : Type u} (f : A → A) : ℕ → (A → A) :=
   @rec (A → A) idfun (λ _ g, f ∘ g)
 
-  hott def ack : ℕ → ℕ → ℕ :=
+  hott definition ack : ℕ → ℕ → ℕ :=
   rec Nat.succ (λ m φ n, iterate φ (n + 1) 1)
 
   hott example (n : ℕ) : ack 0 n = n + 1 :=
@@ -294,13 +293,13 @@ hott example (A : Type u) : ¬¬(A + ¬A) :=
 -- exercise 1.14
 
 /-
-def f {A : Type u} (x : A) (p : x = x) : p = idp x :=
+hott definition f {A : Type u} (x : A) (p : x = x) : p = idp x :=
 @Id.casesOn A x (λ y p, ???) x p (idp (idp x))
 -/
 
 -- exercise 1.15
 
-hott def «Indiscernibility of Identicals» {A : Type u} (C : A → Type v)
+hott definition «Indiscernibility of Identicals» {A : Type u} (C : A → Type v)
   {a b : A} (p : a = b) : C a → C b :=
 @Id.casesOn A a (λ x p, C a → C x) b p idfun
 
diff --git a/GroundZero/Exercises/Chap2.lean b/GroundZero/Exercises/Chap2.lean
index e966815..4b30a62 100644
--- a/GroundZero/Exercises/Chap2.lean
+++ b/GroundZero/Exercises/Chap2.lean
@@ -15,28 +15,28 @@ universe u v u' v' w w' k k'
 section
   variable {A : Type u} {a b c : A}
 
-  hott def trans₁ (p : a = b) (q : b = c) : a = c :=
-  @Id.casesOn A a (λ x _, x = c → a = c) b p (@Id.casesOn A a (λ x _, a = x) c · (idp a)) q
+  hott definition trans₁ (p : a = b) (q : b = c) : a = c :=
+  @J₁ A a (λ x _, x = c → a = c) (@J₁ A a (λ x _, a = x) (idp a) c) b p q
 
   infixl:99 " ⬝₁ " => trans₁
 
-  hott def trans₂ (p : a = b) (q : b = c) : a = c :=
-  @Id.casesOn A a (λ x _, x = c → a = c) b p idfun q
+  hott definition trans₂ (p : a = b) (q : b = c) : a = c :=
+  @J₁ A a (λ x _, x = c → a = c) idfun b p q
 
   infixl:99 " ⬝₂ " => trans₂
 
-  hott def trans₃ (p : a = b) (q : b = c) : a = c :=
-  @Id.casesOn A b (λ x _, a = b → a = x) c q idfun p
+  hott definition trans₃ (p : a = b) (q : b = c) : a = c :=
+  @J₁ A b (λ x _, a = b → a = x) idfun c q p
 
   infixl:99 " ⬝₃ " => trans₃
 
-  hott def eq₁₂ (p : a = b) (q : b = c) : p ⬝₁ q = p ⬝₂ q :=
+  hott remark eq₁₂ (p : a = b) (q : b = c) : p ⬝₁ q = p ⬝₂ q :=
   begin induction p; induction q; reflexivity end
 
-  hott def eq₂₃ (p : a = b) (q : b = c) : p ⬝₂ q = p ⬝₃ q :=
+  hott remark eq₂₃ (p : a = b) (q : b = c) : p ⬝₂ q = p ⬝₃ q :=
   begin induction p; induction q; reflexivity end
 
-  hott def eq₁₃ (p : a = b) (q : b = c) : p ⬝₁ q = p ⬝₃ q :=
+  hott remark eq₁₃ (p : a = b) (q : b = c) : p ⬝₁ q = p ⬝₃ q :=
   begin induction p; induction q; reflexivity end
 end
 
@@ -54,8 +54,8 @@ end
 section
   variable {A : Type u} {a b c : A}
 
-  hott def trans₄ (p : a = b) (q : b = c) : a = c :=
-  @Id.casesOn A b (λ x _, a = b → a = x) c q (@Id.casesOn A a (λ x _, a = x) b · (idp a)) p
+  hott definition trans₄ (p : a = b) (q : b = c) : a = c :=
+  @J₁ A b (λ x _, a = b → a = x) (@J₁ A a (λ x _, a = x) (idp a) b) c q p
 
   infixl:99 " ⬝₄ " => trans₄
 
@@ -71,11 +71,11 @@ end
 
 -- exercise 2.4
 
-hott def nPath (A : Type u) : ℕ → Type u
+hott definition nPath (A : Type u) : ℕ → Type u
 | Nat.zero   => A
 | Nat.succ n => Σ (a b : nPath A n), a = b
 
-hott def boundary {A : Type u} {n : ℕ} :
+hott definition boundary {A : Type u} {n : ℕ} :
   nPath A (n + 1) → (nPath A n) × (nPath A n) :=
 λ ⟨a, b, _⟩, (a, b)
 
@@ -84,13 +84,13 @@ hott def boundary {A : Type u} {n : ℕ} :
 namespace «2.5»
   variable {A : Type u} {B : Type v} {x y : A} (p : x = y)
 
-  hott def transconst (b : B) : transport (λ _, B) p b = b :=
+  hott definition transconst (b : B) : transport (λ _, B) p b = b :=
   begin induction p; reflexivity end
 
-  hott def f (φ : A → B) : φ x = φ y → transport (λ _, B) p (φ x) = φ y :=
+  hott definition f (φ : A → B) : φ x = φ y → transport (λ _, B) p (φ x) = φ y :=
   λ q, transconst p (φ x) ⬝ q
 
-  hott def g (φ : A → B) : transport (λ _, B) p (φ x) = φ y → φ x = φ y :=
+  hott definition g (φ : A → B) : transport (λ _, B) p (φ x) = φ y → φ x = φ y :=
   λ q, (transconst p (φ x))⁻¹ ⬝ q
 
   hott example (φ : A → B) : f p φ ∘ g p φ ~ id :=
@@ -111,9 +111,9 @@ namespace «2.7»
   variable {A : Type u} {A' : Type u'} {B : A → Type v} {B' : A' → Type v'}
            (g : A → A') (h : Π a, B a → B' (g a))
 
-  def φ (x : Σ a, B a) : Σ a', B' a' := ⟨g x.1, h x.1 x.2⟩
+  hott definition φ (x : Σ a, B a) : Σ a', B' a' := ⟨g x.1, h x.1 x.2⟩
 
-  hott def prodMap : Π (x y : Σ a, B a) (p : x.1 = y.1) (q : x.2 =[p] y.2),
+  hott definition prodMap : Π (x y : Σ a, B a) (p : x.1 = y.1) (q : x.2 =[p] y.2),
       ap (φ g h) (Sigma.prod p q)
     = @Sigma.prod A' B' (φ g h x) (φ g h y)
         (@ap A A' x.1 y.1 g p) (depPathMap' g h q) :=
@@ -128,16 +128,16 @@ end «2.7»
 namespace «2.8»
   variable {A A' B B' : Type u} (g : A → A') (h : B → B')
 
-  def φ : A + B → A' + B' :=
+  hott definition φ : A + B → A' + B' :=
   Coproduct.elim (Coproduct.inl ∘ g) (Coproduct.inr ∘ h)
 
-  hott def ρ : Π {x y : A + B}, Coproduct.code x y → Coproduct.code (φ g h x) (φ g h y)
+  hott definition ρ : Π {x y : A + B}, Coproduct.code x y → Coproduct.code (φ g h x) (φ g h y)
   | Sum.inl _, Sum.inl _, p => ap _ p
   | Sum.inr _, Sum.inl _, p => Empty.elim p
   | Sum.inl _, Sum.inr _, p => Empty.elim p
   | Sum.inr _, Sum.inr _, p => ap _ p
 
-  hott def mapPathSum (x y : A + B) : Π p,
+  hott definition mapPathSum (x y : A + B) : Π p,
       ap (φ g h) (Coproduct.pathSum x y p)
     = Coproduct.pathSum (φ g h x) (φ g h y) (ρ g h p) :=
   begin
@@ -156,7 +156,7 @@ end «2.8»
 
 -- exercise 2.9
 
-hott def Coproduct.depUnivProperty (A : Type u) (B : Type v) (X : A + B → Type w) :
+hott definition Coproduct.depUnivProperty (A : Type u) (B : Type v) (X : A + B → Type w) :
   (Π x, X x) ≃ (Π a, X (Coproduct.inl a)) × (Π b, X (Coproduct.inr b)) :=
 begin
   fapply Sigma.mk; { intro φ; exact (λ a, φ (Coproduct.inl a), λ b, φ (Coproduct.inr b)) };
@@ -166,7 +166,7 @@ begin
   { intro f; apply Theorems.funext; intro z; induction z using Sum.casesOn <;> reflexivity }
 end
 
-hott def Coproduct.univProperty (A : Type u) (B : Type v) (X : Type w) :
+hott definition Coproduct.univProperty (A : Type u) (B : Type v) (X : Type w) :
   (A + B → X) ≃ (A → X) × (B → X) :=
 Coproduct.depUnivProperty A B (λ _, X)
 
@@ -194,14 +194,14 @@ namespace «2.12»
            {k : E → F} {h : B → D} {s : D → F}
            (α : j ∘ f = h ∘ i) (β : k ∘ g = s ∘ j)
 
-  def left  : hcommSquare A C B D := ⟨j, h, f, i, α⟩
-  def right : hcommSquare C E D F := ⟨k, s, g, j, β⟩
+  hott definition left  : hcommSquare A C B D := ⟨j, h, f, i, α⟩
+  hott definition right : hcommSquare C E D F := ⟨k, s, g, j, β⟩
 
-  def outer : hcommSquare A E B F :=
+  hott definition outer : hcommSquare A E B F :=
   ⟨k, s ∘ h, g ∘ f, i, @ap (C → F) (A → F) _ _ (· ∘ f) β
                      ⬝ @ap _ (A → F) _ _ (s ∘ ·) α⟩
 
-  hott def pullbackLemma (H : (right β).isPullback) :
+  hott theorem pullbackLemma (H : (right β).isPullback) :
     (left α).isPullback ↔ (outer α β).isPullback :=
   sorry
 end «2.12»
@@ -219,12 +219,12 @@ hott example : (𝟐 ≃ 𝟐) ≃ 𝟐 := Theorems.Equiv.boolEquivEqvBool
 
 -- exercise 2.15
 
-hott def transportMap {A : Type u} {B : A → Type v} {x y : A} (p : x = y) :
+hott definition transportMap {A : Type u} {B : A → Type v} {x y : A} (p : x = y) :
   transport B p = idtoeqv (ap B p) :=
 begin induction p; reflexivity end
 
 -- exercise 2.18
 
-hott def transportSquare {A : Type u} {B : A → Type v} {f g : Π x, B x} (H : f ~ g) {x y : A} (p : x = y) :
+hott definition transportSquare {A : Type u} {B : A → Type v} {f g : Π x, B x} (H : f ~ g) {x y : A} (p : x = y) :
   ap (transport B p) (H x) ⬝ apd g p = apd f p ⬝ H y :=
 begin induction p; transitivity; apply Id.rid; apply Equiv.idmap end
diff --git a/GroundZero/Exercises/Chap3.lean b/GroundZero/Exercises/Chap3.lean
index 81b05bb..7135dff 100644
--- a/GroundZero/Exercises/Chap3.lean
+++ b/GroundZero/Exercises/Chap3.lean
@@ -73,13 +73,13 @@ namespace «3.8»
            (ii  : Π (f : A → B), isequiv f → qinv f)
            (iii : Π (f : A → B), prop (isequiv f))
 
-  hott def i₂ (f : A → B) : qinv f → ∥qinv f∥ :=
+  hott definition i₂ (f : A → B) : qinv f → ∥qinv f∥ :=
   Merely.elem
 
-  hott def ii₂ (f : A → B) : ∥qinv f∥ → qinv f :=
+  hott definition ii₂ (f : A → B) : ∥qinv f∥ → qinv f :=
   ii f ∘ Merely.rec (iii f) idfun ∘ Merely.lift (i f)
 
-  hott def iii₂ (f : A → B) : prop ∥qinv f∥ :=
+  hott definition iii₂ (f : A → B) : prop ∥qinv f∥ :=
   Merely.uniq
 
   hott theorem isequivEqvMerelyQinv (f : A → B) : isequiv f ≃ ∥qinv f∥ :=
@@ -93,21 +93,21 @@ namespace «3.9»
   section
     variable {A : Type u} {H : prop A} {lem : LEM₋₁}
 
-    hott def lemTrue (x : A) : lem A H = Sum.inl x :=
+    hott definition lemTrue (x : A) : lem A H = Sum.inl x :=
     match lem A H with
     | Sum.inl y => ap Sum.inl (H y x)
     | Sum.inr φ => Empty.elim (φ x)
 
-    hott def lemFalse (φ : ¬A) : lem A H = Sum.inr φ :=
+    hott definition lemFalse (φ : ¬A) : lem A H = Sum.inr φ :=
     match lem A H with
     | Sum.inl x => Empty.elim (φ x)
     | Sum.inr ψ => ap Sum.inr (Structures.notIsProp ψ φ)
   end
 
-  hott def Ωelim (lem : LEM₋₁ u) : Prop u → 𝟐 :=
+  hott definition Ωelim (lem : LEM₋₁ u) : Prop u → 𝟐 :=
   λ w, Coproduct.elim (λ _, true) (λ _, false) (lem w.1 w.2)
 
-  hott def Ωintro : 𝟐 → Prop :=
+  hott definition Ωintro : 𝟐 → Prop :=
   Bool.elim ⟨𝟎, Structures.emptyIsProp⟩ ⟨𝟏, Structures.unitIsProp⟩
 
   hott lemma propsetInhIsProp (A : Prop) : prop A.1 := A.2
@@ -140,7 +140,7 @@ namespace «3.10»
   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
 
-  hott def ResizeΩ : Prop u → Prop (max u v) :=
+  hott definition ResizeΩ : Prop u → Prop (max u v) :=
   λ w, ⟨Resize.{u, v} w.1, Resize.prop w.2⟩
 
   hott lemma lemCumulativity (lem : LEM₋₁ (max u v)) : LEM₋₁ u :=
@@ -261,20 +261,20 @@ namespace «3.14»
   open «3.11»
   open «3.9»
 
-  hott def dn.intro {A : Type u} : A → ¬¬A :=
+  hott definition dn.intro {A : Type u} : A → ¬¬A :=
   λ x φ, φ x
 
-  hott def dn.rec (lem : LEM₋₁ v) {A : Type u} {B : Type v} : prop B → (A → B) → (¬¬A → B) :=
+  hott definition dn.rec (lem : LEM₋₁ v) {A : Type u} {B : Type v} : prop B → (A → B) → (¬¬A → B) :=
   λ H f, Coproduct.elim (λ b _, b) (λ φ g, Empty.elim (g (φ ∘ f))) (lem B H)
 
-  hott def dn.recβrule (lem : LEM₋₁ v) {A : Type u} {B : Type v} {H : prop B}
+  hott definition dn.recβrule (lem : LEM₋₁ v) {A : Type u} {B : Type v} {H : prop B}
     {f : A → B} (x : A) : dn.rec lem H f (dn.intro x) = f x :=
   H _ _
 
-  hott def dnImplMerely (lem : LEM₋₁ u) {A : Type u} : ¬¬A → ∥A∥ :=
+  hott definition dnImplMerely (lem : LEM₋₁ u) {A : Type u} : ¬¬A → ∥A∥ :=
   dn.rec lem HITs.Merely.uniq HITs.Merely.elem
 
-  hott def lemMerelyEqvDef (lem : LEM₋₁ u) {A : Type u} : ¬¬A ≃ ∥A∥ :=
+  hott definition lemMerelyEqvDef (lem : LEM₋₁ u) {A : Type u} : ¬¬A ≃ ∥A∥ :=
   Structures.propEquivLemma Structures.notIsProp HITs.Merely.uniq (dnImplMerely lem) merelyImplDn
 end «3.14»
 
@@ -286,14 +286,15 @@ namespace «3.15»
 
   variable (RES : qinv ResizeΩ.{0, v})
 
-  hott def Merely (A : Type u) := Π (P : Prop 0), (A → P.1) → P.1
+  hott definition Merely (A : Type u) :=
+  Π (P : Prop 0), (A → P.1) → P.1
 
-  hott def Merely.elem {A : Type u} : A → Merely A :=
+  hott definition Merely.elem {A : Type u} : A → Merely A :=
   λ x P f, f x
 
   -- judgmental computation rule??
   -- https://github.com/HoTT/Coq-HoTT/pull/1678#issuecomment-1334818499
-  hott def Merely.rec {A : Type u} {B : Type v} (H : prop B) (f : A → B) (φ : Merely A) : B :=
+  hott definition Merely.rec {A : Type u} {B : Type v} (H : prop B) (f : A → B) (φ : Merely A) : B :=
   transport Sigma.fst (RES.2.1 ⟨B, H⟩)
     (Resize.intro.{0, v} (φ (RES.1 ⟨B, H⟩) (λ x, Resize.elim.{0, v}
       (transport Sigma.fst (RES.2.1 ⟨B, H⟩)⁻¹ (f x)))))
@@ -372,7 +373,7 @@ namespace «3.17»
            (uniq   : Π A, prop (Merely A))
            (mrec   : Π A B, prop B → (A → B) → (Merely A → B))
 
-  def mind {A : Type u} (B : Merely A → Type v) (H : Π x, prop (B x)) (f : Π x, B (elem A x)) : Π x, B x :=
+  hott definition mind {A : Type u} (B : Merely A → Type v) (H : Π x, prop (B x)) (f : Π x, B (elem A x)) : Π x, B x :=
   λ x, mrec A (B x) (H x) (λ y, transport B (uniq A (elem A y) x) (f y)) x
 end «3.17»
 
@@ -407,11 +408,11 @@ namespace «3.19»
   variable {P : ℕ → Type u} (H : Π n, prop (P n)) (G : Π n, dec (P n))
   open GroundZero.HITs
 
-  hott def BSA (n : ℕ) : ℕ → ℕ
+  hott definition BSA (n : ℕ) : ℕ → ℕ
   | Nat.zero   => n
   | Nat.succ m => Coproduct.elim (λ _, n) (λ _, BSA (Nat.succ n) m) (G n)
 
-  hott def BS := BSA G Nat.zero
+  hott definition BS := BSA G Nat.zero
 
   hott lemma BSP (n m : ℕ) : P (n + m) → P (BSA G n m) :=
   begin
@@ -490,7 +491,7 @@ namespace «3.22»
   open GroundZero.Theorems.Nat
   open GroundZero.HITs
 
-  hott def fin.fsuc {n : ℕ} (m : fin n) : fin (n + 1) :=
+  hott definition fin.fsuc {n : ℕ} (m : fin n) : fin (n + 1) :=
   ⟨m.1, le.step (m.1 + 1) n m.2⟩
 
   hott lemma step (n : ℕ) (Y : fin (n + 1) → Type u)
@@ -511,20 +512,20 @@ namespace «3.23»
   open GroundZero.Structures
   open GroundZero.HITs
 
-  hott def choice {A : Type u} (G : dec A) : A → Type u :=
+  hott definition choice {A : Type u} (G : dec A) : A → Type u :=
   λ x, Coproduct.elim (x = ·) (λ φ, Empty.elim (φ x)) G
 
-  hott def decMerely {A : Type u} (G : dec A) : Type u :=
+  hott definition decMerely {A : Type u} (G : dec A) : Type u :=
   Σ x, choice G x
 
-  hott def decMerely.elem {A : Type u} (G : dec A) : A → decMerely G :=
+  hott definition decMerely.elem {A : Type u} (G : dec A) : A → decMerely G :=
   begin
     intro x; induction G using Sum.casesOn;
     case inl y => { existsi y; apply idp };
     case inr φ => { apply Empty.elim (φ x) }
   end
 
-  hott def decMerely.uniq {A : Type u} (G : dec A) : prop (decMerely G) :=
+  hott definition decMerely.uniq {A : Type u} (G : dec A) : prop (decMerely G) :=
   begin
     induction G using Sum.casesOn;
     case inl _ => { intro w₁ w₂; fapply Sigma.prod;
@@ -535,7 +536,7 @@ namespace «3.23»
     case inr φ => { intro w₁ w₂; apply Empty.elim (φ w₁.1) }
   end
 
-  hott def decMerely.dec {A : Type u} (G : dec A) : dec (@decMerely A G) :=
+  hott definition decMerely.dec {A : Type u} (G : dec A) : dec (@decMerely A G) :=
   begin
     induction G using Sum.casesOn;
     case inl x => { left; existsi x; apply idp };
@@ -576,9 +577,9 @@ namespace «3.24»
   | Nat.zero,   Nat.succ m => emptyIsProp
   | Nat.succ n, Nat.succ m => codeProp n m
 
-  hott def encodeDecode {m n : ℕ} (p : Nat.code m n) : Nat.encode (Nat.decode p) = p :=
+  hott definition encodeDecode {m n : ℕ} (p : Nat.code m n) : Nat.encode (Nat.decode p) = p :=
   codeProp _ _ _ _
 
-  hott def recognize (m n : ℕ) : m = n ≃ Nat.code m n :=
-  ⟨Nat.encode, (⟨Nat.decode, Nat.decodeEncode⟩, ⟨Nat.decode, encodeDecode⟩)⟩
+  hott theorem recognize (m n : ℕ) : m = n ≃ Nat.code m n :=
+  Equiv.intro Nat.encode Nat.decode Nat.decodeEncode Nat.encodeDecode
 end «3.24»
diff --git a/GroundZero/Exercises/Chap4.lean b/GroundZero/Exercises/Chap4.lean
index 3b78b1b..8718466 100644
--- a/GroundZero/Exercises/Chap4.lean
+++ b/GroundZero/Exercises/Chap4.lean
@@ -20,7 +20,7 @@ namespace «4.1»
   open GroundZero.Structures (prop)
   open GroundZero.Types.Id (ap)
 
-  def Adjoint {A : Type u} {B : Type v} (f : A → B) :=
+  hott definition Adjoint {A : Type u} {B : Type v} (f : A → B) :=
   Σ (g : B → A) (η : g ∘ f ~ idfun) (ε : f ∘ g ~ idfun), (Π x, ap f (η x) = ε (f x)) × (Π y, ap g (ε y) = η (g y))
 
   hott lemma adjointIdfun (A : Type u) : Adjoint (@idfun A) ≃ (Π (x : A), idp x = idp x) :=
@@ -66,7 +66,7 @@ namespace «4.2»
   noncomputable hott example : Corr A B ≃ (A ≃ B) :=
   Theorems.Equiv.biinvEquivCorr
 
-  hott def isequiv (f : A → B) := Σ (ρ : Corr A B), Π x, ρ.1 x (f x)
+  hott definition isequiv (f : A → B) := Σ (ρ : Corr A B), Π x, ρ.1 x (f x)
 
   hott theorem «4.2.i» (f : A → B) : qinv f → isequiv f :=
   begin
@@ -80,13 +80,13 @@ namespace «4.2»
     apply Theorems.funext; intro x; exact ap Sigma.fst ((w.1.2.1 x).2 ⟨f x, w.2 x⟩);
   end
 
-  hott def corrPath {f : A → B} (e : isequiv f) {a : A} {b : B} :=
+  hott definition corrPath {f : A → B} (e : isequiv f) {a : A} {b : B} :=
   λ r, contrImplProp (e.1.2.1 a) ⟨f a, e.2 a⟩ ⟨b, r⟩
 
-  hott def F {f : A → B} (e : isequiv f) {a : A} {b : B} : e.1.1 a b → f a = b :=
+  hott definition F {f : A → B} (e : isequiv f) {a : A} {b : B} : e.1.1 a b → f a = b :=
   λ r, ap Sigma.fst (corrPath e r)
 
-  hott def G {f : A → B} (e : isequiv f) {a : A} {b : B} : f a = b → e.1.1 a b :=
+  hott definition G {f : A → B} (e : isequiv f) {a : A} {b : B} : f a = b → e.1.1 a b :=
   λ p, transport (e.1.1 a) p (e.2 a)
 
   hott lemma isequivRel {f : A → B} (e : isequiv f) {a : A} {b : B} : (e.1.1 a b) ≃ (f a = b) :=
@@ -182,7 +182,7 @@ namespace «4.4»
   hott lemma bisigmaComm (A : Type u) (B : Type v) (C : A → B → Type w) : (Σ x y, C x y) ≃ (Σ y x, C x y) :=
   ⟨λ w, ⟨w.2.1, w.1, w.2.2⟩, Qinv.toBiinv _ ⟨λ w, ⟨w.2.1, w.1, w.2.2⟩, (idp, idp)⟩⟩
 
-  hott def mapProd {A : Type u} {A' : Type u'} {B : A → Type v} {B' : A' → Type v'}
+  hott definition mapProd {A : Type u} {A' : Type u'} {B : A → Type v} {B' : A' → Type v'}
     (f : A → A') (g : Π x, B x → B' (f x)) : (Σ x, B x) → (Σ y, B' y) :=
   λ w, ⟨f w.1, g w.1 w.2⟩
 
@@ -213,7 +213,7 @@ namespace «4.4»
 
   variable {A : Type u} {B : Type v} {C : Type w} (f : A → B) (g : B → C) (b : B)
 
-  hott def naturalMap : fib (g ∘ f) (g b) → fib g (g b) :=
+  hott definition naturalMap : fib (g ∘ f) (g b) → fib g (g b) :=
   λ w, ⟨f w.1, w.2⟩
 
   hott theorem «4.4.i» : fib (naturalMap f g b) ⟨b, idp (g b)⟩ ≃ fib f b :=
@@ -309,7 +309,7 @@ namespace «4.6»
   open GroundZero.Structures
   open GroundZero.HITs
 
-  hott def idtoqinv {A B : Type u} : A = B → Σ (f : A → B), qinv f :=
+  hott definition idtoqinv {A B : Type u} : A = B → Σ (f : A → B), qinv f :=
   λ p, transport (λ X, Σ (f : A → X), qinv f) p ⟨idfun, ⟨idfun, (idp, idp)⟩⟩
 
   -- 4.6.i
@@ -332,10 +332,10 @@ namespace «4.6»
     variable (uaq : Π (A B : Type), qinv (@idtoqinv A B))
     open Circle (base loop rot)
 
-    hott def negBoolQinv : qinv not :=
+    hott definition negBoolQinv : qinv not :=
     ⟨not, (negNeg, negNeg)⟩
 
-    hott def universeNotASet : ¬(hset Type) :=
+    hott definition universeNotASet : ¬(hset Type) :=
     let φ : Σ (f : 𝟐 → 𝟐), qinv f := ⟨not, negBoolQinv⟩;
     let ψ : Σ (f : 𝟐 → 𝟐), qinv f := ⟨idfun, Qinv.ideqv⟩;
 
@@ -344,7 +344,7 @@ namespace «4.6»
     let g : idtoqinv p = ψ := ap idtoqinv (ε _ _ p (idp 𝟐));
     ffNeqTt (Interval.happly (ap Sigma.fst (f⁻¹ ⬝ g)) true)
 
-    noncomputable hott def loopNeqRefl : loop ≠ idp base :=
+    noncomputable hott definition loopNeqRefl : loop ≠ idp base :=
     begin
       intro H; apply universeNotASet uaq;
       intros A B p q; apply (KIffSet Type).left;