From c46908b52ca88554237a33de5c03fea208d124c5 Mon Sep 17 00:00:00 2001 From: Siegmentation Fault Date: Fri, 22 Dec 2023 16:53:15 +0700 Subject: [PATCH] lemmas & clean up --- GroundZero/Structures.lean | 32 ++++++- GroundZero/Theorems/Nat.lean | 160 +++++++++++++++++------------------ GroundZero/Types/Nat.lean | 11 +-- 3 files changed, 109 insertions(+), 94 deletions(-) diff --git a/GroundZero/Structures.lean b/GroundZero/Structures.lean index a23c904..62e9f5a 100644 --- a/GroundZero/Structures.lean +++ b/GroundZero/Structures.lean @@ -97,6 +97,36 @@ namespace hlevel | n, −1 => pred n | n, succ (succ m) => addNat n (succSucc m) + hott lemma predPredSuccSucc : Π n, predPred (succSucc n) = n + | −2 => idp −2 + | succ n => ap succ (predPredSuccSucc n) + + hott lemma succSuccPredPred : Π k, succSucc (predPred k) = k + | Nat.zero => idp 0 + | Nat.succ k => ap Nat.succ (succSuccPredPred k) + + hott lemma addNatMinusTwo : Π n, addNat −2 n = predPred n + | Nat.zero => idp −2 + | Nat.succ n => ap succ (addNatMinusTwo n) + + hott lemma addNatMinusOne : Π n, addNat −1 n = succ (predPred n) + | Nat.zero => idp −1 + | Nat.succ n => ap succ (addNatMinusOne n) + + hott corollary minusTwoAdd : Π n, add −2 n = pred (pred n) + | −2 => idp −2 + | −1 => idp −2 + | succ (succ n) => addNatMinusTwo (succSucc n) ⬝ predPredSuccSucc n + + hott corollary minusOneAdd : Π n, add −1 n = pred n + | −2 => idp −2 + | −1 => idp −2 + | succ (succ n) => addNatMinusOne (succSucc n) ⬝ ap succ (predPredSuccSucc n) + + hott lemma addNatToAdd : Π n m, addNat n (succSucc m) = predPred (succSucc n + succSucc m) + | n, −2 => (predPredSuccSucc n)⁻¹ + | n, succ m => ap succ (addNatToAdd n m) + instance : HAdd ℕ₋₂ ℕ₋₂ ℕ₋₂ := ⟨add⟩ hott definition ofNat (n : ℕ) : ℕ₋₂ := @@ -119,7 +149,7 @@ notation n "-Type" => nType n macro n:term "-Type" l:level : term => `(nType.{$l} $n) hott lemma hlevel.cumulative {A : Type u} : Π (n : hlevel), is-n-type A → is-(hlevel.succ n)-type A -| −2, H => λ x y, ⟨(H.2 x)⁻¹ ⬝ H.2 y, λ p, begin induction p; apply Types.Id.invComp end⟩ +| −2, H => λ x y, ⟨(H.2 x)⁻¹ ⬝ H.2 y, λ p, begin induction p; apply Id.invComp end⟩ | hlevel.succ n, H => λ x y, cumulative n (H x y) noncomputable hott corollary hlevel.strongCumulative (n m : hlevel) (ρ : n ≤ m) : diff --git a/GroundZero/Theorems/Nat.lean b/GroundZero/Theorems/Nat.lean index 7e921d6..0b40531 100644 --- a/GroundZero/Theorems/Nat.lean +++ b/GroundZero/Theorems/Nat.lean @@ -22,10 +22,10 @@ namespace Nat hott theorem natIsSet' : hset ℕ := λ n m, propRespectsEquiv (Nat.recognize n m).symm (codeIsProp n m) - def succInj {n m : ℕ} : Nat.succ n = Nat.succ m → n = m := + hott corollary succInj {n m : ℕ} : Nat.succ n = Nat.succ m → n = m := Nat.decode ∘ Nat.encode - hott def natDecEq : Π (m n : ℕ), dec (m = n) + hott definition natDecEq : Π (m n : ℕ), dec (m = n) | Nat.zero, Nat.zero => Sum.inl (idp 0) | Nat.succ m, Nat.zero => Sum.inr succNeqZero | Nat.zero, Nat.succ n => Sum.inr (succNeqZero ∘ Id.inv) @@ -34,137 +34,131 @@ namespace Nat | Sum.inl p => Sum.inl (ap Nat.succ p) | Sum.inr φ => Sum.inr (φ ∘ succInj) - hott def natIsSet : hset ℕ := Hedberg natDecEq + hott theorem natIsSet : hset ℕ := Hedberg natDecEq - hott def zeroPlus : Π (i : ℕ), 0 + i = i + hott theorem zeroPlus : Π (i : ℕ), 0 + i = i | Nat.zero => idp 0 | Nat.succ i => ap Nat.succ (zeroPlus i) - hott def succPlus (i : ℕ) : Π j, Nat.succ i + j = Nat.succ (i + j) + hott lemma succPlus (i : ℕ) : Π j, Nat.succ i + j = Nat.succ (i + j) | Nat.zero => idp _ | Nat.succ j => ap Nat.succ (succPlus i j) - hott def comm : Π (i j : ℕ), i + j = j + i + hott theorem comm : Π (i j : ℕ), i + j = j + i | Nat.zero, j => zeroPlus j | Nat.succ i, j => succPlus i j ⬝ ap Nat.succ (comm i j) - hott def assoc (i j : ℕ) : Π k, (i + j) + k = i + (j + k) + hott theorem assoc (i j : ℕ) : Π k, (i + j) + k = i + (j + k) | Nat.zero => idp (i + j) | Nat.succ k => ap Nat.succ (assoc i j k) - hott def zeroMul : Π (i : ℕ), 0 * i = 0 + hott theorem zeroMul : Π (i : ℕ), 0 * i = 0 | Nat.zero => idp 0 | Nat.succ i => zeroMul i - hott def oneMul : Π (i : ℕ), 1 * i = i + hott theorem oneMul : Π (i : ℕ), 1 * i = i | Nat.zero => idp 0 | Nat.succ i => ap Nat.succ (oneMul i) - hott def mulOne (i : ℕ) : i * 1 = i := zeroPlus i + hott corollary mulOne (i : ℕ) : i * 1 = i := zeroPlus i - hott def distribLeft (i : ℕ) : Π (j n : ℕ), n * (i + j) = n * i + n * j + hott theorem distribLeft (i : ℕ) : Π (j n : ℕ), n * (i + j) = n * i + n * j | Nat.zero, n => idp _ | Nat.succ j, n => ap (λ m, m + n) (distribLeft i j n) ⬝ assoc _ _ _ - hott def mulSucc (i : ℕ) : Π j, Nat.succ i * j = i * j + j + hott lemma mulSucc (i : ℕ) : Π j, Nat.succ i * j = i * j + j | Nat.zero => idp _ | Nat.succ j => ap Nat.succ (ap (λ k, k + i) (mulSucc i j) ⬝ assoc _ _ _ ⬝ (assoc _ _ _ ⬝ ap _ (comm _ _))⁻¹) - hott def mulComm (i : ℕ) : Π j, i * j = j * i + hott theorem mulComm (i : ℕ) : Π j, i * j = j * i | Nat.zero => (zeroMul _)⁻¹ | Nat.succ j => distribLeft j 1 i ⬝ (mulSucc j i ⬝ bimap Nat.add (mulComm i j)⁻¹ (mulOne i)⁻¹)⁻¹ - hott def succMul (i j : ℕ) : i * Nat.succ j = i * j + i := + hott lemma succMul (i j : ℕ) : i * Nat.succ j = i * j + i := mulComm _ _ ⬝ mulSucc _ _ ⬝ Id.ap (Nat.add · _) (mulComm _ _) - hott def distribRight (i j n : ℕ) : (i + j) * n = i * n + j * n := + hott corollary distribRight (i j n : ℕ) : (i + j) * n = i * n + j * n := mulComm (i + j) n ⬝ distribLeft _ _ _ ⬝ bimap Nat.add (mulComm _ _) (mulComm _ _) - hott def oneNeqNPlusTwo (n : ℕ) : ¬(1 = n + 2) := + hott proposition oneNeqNPlusTwo (n : ℕ) : ¬(1 = n + 2) := λ p, succNeqZero (ap Nat.pred p)⁻¹ - def isEven (n : ℕ) := Σ m, n = m * 2 - def isOdd (n : ℕ) := Σ m, n = m * 2 + 1 + hott definition isEven (n : ℕ) := Σ m, n = m * 2 + hott definition isOdd (n : ℕ) := Σ m, n = m * 2 + 1 - hott def plusOnePlus {i j : ℕ} : i + 1 + j = (i + j) + 1 := calc + hott lemma plusOnePlus {i j : ℕ} : i + 1 + j = (i + j) + 1 := calc i + 1 + j = i + (1 + j) : assoc _ _ _ ... = i + (j + 1) : ap (Nat.add i) (comm 1 j) ... = (i + j) + 1 : idp _ - hott def assocTetra {i j k l : ℕ} : i + (j + k) + l = (i + j) + (k + l) := calc + hott lemma assocTetra {i j k l : ℕ} : i + (j + k) + l = (i + j) + (k + l) := calc (i + (j + k)) + l = i + ((j + k) + l) : assoc _ _ _ ... = i + (j + (k + l)) : ap _ (assoc _ _ _) ... = (i + j) + (k + l) : (assoc _ _ _)⁻¹ - hott def plusDiag (n : ℕ) : n * 2 = n + n := + hott lemma plusDiag (n : ℕ) : n * 2 = n + n := ap (λ m, m + n) (zeroPlus _) - hott def apart : ℕ → ℕ → Type - | Nat.zero, Nat.zero => 𝟎 - | Nat.succ m, Nat.zero => 𝟏 - | Nat.zero, Nat.succ n => 𝟏 - | Nat.succ m, Nat.succ n => apart m n - - hott def max : ℕ → ℕ → ℕ + hott definition max : ℕ → ℕ → ℕ | Nat.zero, Nat.zero => 0 | Nat.succ m, Nat.zero => m + 1 | Nat.zero, Nat.succ n => n + 1 | Nat.succ m, Nat.succ n => max m n + 1 - hott def max.comm : Π (m n : ℕ), max m n = max n m + hott lemma max.comm : Π (m n : ℕ), max m n = max n m | Nat.zero, Nat.zero => idp _ | Nat.succ m, Nat.zero => idp _ | Nat.zero, Nat.succ n => idp _ | Nat.succ m, Nat.succ n => ap Nat.succ (comm _ _) - hott def min : ℕ → ℕ → ℕ + hott definition min : ℕ → ℕ → ℕ | Nat.zero, Nat.zero => 0 | Nat.succ m, Nat.zero => 0 | Nat.zero, Nat.succ n => 0 | Nat.succ m, Nat.succ n => min m n + 1 - hott def min.comm : Π (m n : ℕ), min m n = min n m + hott lemma min.comm : Π (m n : ℕ), min m n = min n m | Nat.zero, Nat.zero => idp _ | Nat.succ m, Nat.zero => idp _ | Nat.zero, Nat.succ n => idp _ | Nat.succ m, Nat.succ n => ap Nat.succ (comm _ _) - hott def max.refl : Π n, max n n = n + hott lemma max.refl : Π n, max n n = n | Nat.zero => idp 0 | Nat.succ n => ap Nat.succ (refl n) - hott def min.refl : Π n, min n n = n + hott lemma min.refl : Π n, min n n = n | Nat.zero => idp 0 | Nat.succ n => ap Nat.succ (refl n) - def le (n m : ℕ) := max n m = m + hott definition le (n m : ℕ) := max n m = m infix:55 (priority := high) " ≤ " => le - def ge (n m : ℕ) := m ≤ n + hott definition ge (n m : ℕ) := m ≤ n infix:55 (priority := high) " ≥ " => ge - hott def max.zeroLeft (n : ℕ) : max 0 n = n := + hott lemma max.zeroLeft (n : ℕ) : max 0 n = n := begin induction n using Nat.casesOn <;> reflexivity end - hott def max.zeroRight (n : ℕ) : max n 0 = n := + hott lemma max.zeroRight (n : ℕ) : max n 0 = n := begin induction n using Nat.casesOn <;> reflexivity end - hott def min.zeroLeft (n : ℕ) : min 0 n = 0 := + hott lemma min.zeroLeft (n : ℕ) : min 0 n = 0 := begin induction n using Nat.casesOn <;> reflexivity end - hott def min.zeroRight (n : ℕ) : min n 0 = 0 := + hott lemma min.zeroRight (n : ℕ) : min n 0 = 0 := begin induction n using Nat.casesOn <;> reflexivity end - hott def max.neZero {n : ℕ} : ¬(max (n + 1) 0 = 0) := succNeqZero + hott lemma max.neZero {n : ℕ} : ¬(max (n + 1) 0 = 0) := succNeqZero - hott def max.zero : Π n, max n 0 = 0 → n = 0 + hott lemma max.zero : Π n, max n 0 = 0 → n = 0 | Nat.zero, _ => idp _ | Nat.succ n, p => Proto.Empty.elim (max.neZero p) - hott def le.prop (n m : ℕ) : prop (n ≤ m) := natIsSet _ _ + hott corollary le.prop (n m : ℕ) : prop (n ≤ m) := natIsSet _ _ - hott def max.assoc : Π n m k, max n (max m k) = max (max n m) k + hott lemma max.assoc : Π n m k, max n (max m k) = max (max n m) k | Nat.zero, Nat.zero, Nat.zero => idp _ | Nat.zero, Nat.zero, Nat.succ k => idp _ | Nat.zero, Nat.succ m, Nat.zero => idp _ @@ -174,7 +168,7 @@ namespace Nat | Nat.succ n, Nat.succ m, Nat.zero => idp _ | Nat.succ n, Nat.succ m, Nat.succ k => ap Nat.succ (assoc _ _ _) - hott def min.assoc : Π n m k, min n (min m k) = min (min n m) k + hott lemma min.assoc : Π n m k, min n (min m k) = min (min n m) k | Nat.zero, Nat.zero, Nat.zero => idp _ | Nat.zero, Nat.zero, Nat.succ k => idp _ | Nat.zero, Nat.succ m, Nat.zero => idp _ @@ -184,7 +178,7 @@ namespace Nat | Nat.succ n, Nat.succ m, Nat.zero => idp _ | Nat.succ n, Nat.succ m, Nat.succ k => ap Nat.succ (assoc _ _ _) - hott def le.trans {n m k : ℕ} : n ≤ m → m ≤ k → n ≤ k := + hott theorem le.trans {n m k : ℕ} : n ≤ m → m ≤ k → n ≤ k := begin intros p q; change _ = _; transitivity; apply ap; exact q⁻¹; transitivity; apply max.assoc; @@ -193,74 +187,74 @@ namespace Nat instance : Transitive le := ⟨@le.trans⟩ - hott def le.inj (n m : ℕ) : n + 1 ≤ m + 1 → n ≤ m := ap Nat.pred - hott def le.map (n m : ℕ) : n ≤ m → n + 1 ≤ m + 1 := ap Nat.succ + hott corollary le.inj (n m : ℕ) : n + 1 ≤ m + 1 → n ≤ m := ap Nat.pred + hott corollary le.map (n m : ℕ) : n ≤ m → n + 1 ≤ m + 1 := ap Nat.succ - hott def le.addr (n m : ℕ) : Π k, n ≤ m → n + k ≤ m + k + hott theorem le.addr (n m : ℕ) : Π k, n ≤ m → n + k ≤ m + k | Nat.zero, h => h | Nat.succ k, h => le.map (n + k) (m + k) (le.addr n m k h) - hott def le.addl (n m k : ℕ) (h : n ≤ m) : k + n ≤ k + m := + hott theorem le.addl (n m k : ℕ) (h : n ≤ m) : k + n ≤ k + m := transport (_ ≤ ·) (Nat.comm m k) (transport (· ≤ _) (Nat.comm n k) (le.addr n m k h)) - hott def le.succ : Π (n : ℕ), n ≤ n + 1 + hott lemma le.succ : Π (n : ℕ), n ≤ n + 1 | Nat.zero => idp _ | Nat.succ n => ap Nat.succ (succ n) - hott def le.step : Π (n m : ℕ), n ≤ m → n ≤ m + 1 + hott definition le.step : Π (n m : ℕ), n ≤ m → n ≤ m + 1 | Nat.zero, m, _ => idp _ | Nat.succ n, m, p => le.trans p (le.succ _) - hott def minMax : Π (m n : ℕ), max m n = n → min m n = m + hott lemma minMax : Π (m n : ℕ), max m n = n → min m n = m | Nat.zero, Nat.zero, p => idp _ | Nat.succ m, Nat.zero, p => Proto.Empty.elim (max.neZero p) | Nat.zero, Nat.succ n, p => idp _ | Nat.succ m, Nat.succ n, p => ap Nat.succ (minMax m n (ap Nat.pred p)) - hott def le.max (n m : ℕ) : n ≤ max n m := + hott corollary le.max (n m : ℕ) : n ≤ max n m := begin change _ = _; transitivity; apply max.assoc; apply ap (Nat.max · m); apply max.refl end - hott def le.maxRev (n m : ℕ) : n ≤ Nat.max m n := + hott corollary le.maxRev (n m : ℕ) : n ≤ Nat.max m n := transport (le n) (max.comm n m) (le.max n m) - hott def le.min : Π (n m : ℕ), le (min n m) m + hott lemma le.min : Π (n m : ℕ), le (min n m) m | Nat.zero, Nat.zero => idp _ | Nat.succ n, Nat.zero => idp _ | Nat.zero, Nat.succ m => idp _ | Nat.succ n, Nat.succ m => ap Nat.succ (min n m) - hott def le.minRev (n m : ℕ) : Nat.min m n ≤ m := + hott lemma le.minRev (n m : ℕ) : Nat.min m n ≤ m := @transport ℕ (· ≤ m) (Nat.min n m) (Nat.min m n) (min.comm n m) (le.min n m) - hott def le.asymm {n m : ℕ} (p : n ≤ m) (q : m ≤ n) : n = m := + hott theorem le.asymm {n m : ℕ} (p : n ≤ m) (q : m ≤ n) : n = m := q⁻¹ ⬝ max.comm _ _ ⬝ p - hott def le.dec : Π (m n : ℕ), (m ≤ n) + (n + 1 ≤ m) + hott lemma le.dec : Π (m n : ℕ), (m ≤ n) + (n + 1 ≤ m) | Nat.zero, Nat.zero => Sum.inl (idp _) | Nat.succ m, Nat.zero => Sum.inr (ap Nat.succ (max.zeroLeft m)) | Nat.zero, Nat.succ n => Sum.inl (idp _) | Nat.succ m, Nat.succ n => Coproduct.elim (Sum.inl ∘ ap Nat.succ) (Sum.inr ∘ ap Nat.succ) (dec m n) - hott def le.neSucc : Π (n : ℕ), ¬(n + 1 ≤ n) + hott lemma le.neSucc : Π (n : ℕ), ¬(n + 1 ≤ n) | Nat.zero => max.neZero | Nat.succ n => λ p, neSucc n (le.inj _ _ p) - hott def le.empty (m n : ℕ) : m ≤ n → ¬(n + 1 ≤ m) := + hott lemma le.empty (m n : ℕ) : m ≤ n → ¬(n + 1 ≤ m) := begin intros p q; apply le.neSucc n; transitivity; exact q; exact p end - hott def le.neqSucc {n m : ℕ} (p : n ≠ m + 1) (q : n ≤ m + 1) : n ≤ m := + hott lemma le.neqSucc {n m : ℕ} (p : n ≠ m + 1) (q : n ≤ m + 1) : n ≤ m := match le.dec n m with | Sum.inl r₁ => r₁ | Sum.inr r₂ => Proto.Empty.elim (p (le.asymm q r₂)) - hott def le.leSucc : Π (n : ℕ), n ≤ n + 1 + hott lemma le.leSucc : Π (n : ℕ), n ≤ n + 1 | Nat.zero => idp _ | Nat.succ n => ap Nat.succ (leSucc n) - hott def le.elim (ρ : ℕ → ℕ → Type u) (τ : Π n m k, ρ n m → ρ m k → ρ n k) + hott definition le.elim (ρ : ℕ → ℕ → Type u) (τ : Π n m k, ρ n m → ρ m k → ρ n k) (reflρ : Π n, ρ n n) (succρ : Π n, ρ n (n + 1)) {n : ℕ} : Π {m : ℕ}, n ≤ m → ρ n m | Nat.zero, p => transport (ρ · 0) (max.zero _ p)⁻¹ (reflρ _) | Nat.succ m, p => @@ -268,41 +262,41 @@ namespace Nat | Sum.inl q₁ => transport (ρ n) q₁ (reflρ _) | Sum.inr q₂ => τ n m _ (@elim ρ τ reflρ succρ n m (le.neqSucc q₂ p)) (succρ _) - def dist : ℕ → ℕ → ℕ + hott definition dist : ℕ → ℕ → ℕ | Nat.zero, Nat.zero => 0 | Nat.succ m, Nat.zero => Nat.succ m | Nat.zero, Nat.succ n => Nat.succ n | Nat.succ m, Nat.succ n => dist m n - hott def dist.refl : Π (n : ℕ), dist n n = 0 + hott lemma dist.refl : Π (n : ℕ), dist n n = 0 | Nat.zero => idp 0 | Nat.succ n => refl n - hott def dist.identity : Π (n m : ℕ) (p : dist n m = 0), n = m + hott lemma dist.identity : Π (n m : ℕ) (p : dist n m = 0), n = m | Nat.zero, Nat.zero, _ => idp 0 | Nat.succ m, Nat.zero, p => p | Nat.zero, Nat.succ n, p => p⁻¹ | Nat.succ m, Nat.succ n, p => ap Nat.succ (identity m n p) - hott def dist.symm : Π (n m : ℕ), dist n m = dist m n + hott lemma dist.symm : Π (n m : ℕ), dist n m = dist m n | Nat.zero, Nat.zero => idp _ | Nat.succ m, Nat.zero => idp _ | Nat.zero, Nat.succ n => idp _ | Nat.succ m, Nat.succ n => symm m n - hott def dist.zeroLeft (n : ℕ) : dist n 0 = n := + hott lemma dist.zeroLeft (n : ℕ) : dist n 0 = n := begin induction n using Nat.casesOn <;> reflexivity end - hott def dist.zeroRight (n : ℕ) : dist 0 n = n := + hott lemma dist.zeroRight (n : ℕ) : dist 0 n = n := begin induction n using Nat.casesOn <;> reflexivity end - hott def dist.succLeft : Π (n m : ℕ), dist (n + 1) m ≤ dist n m + 1 + hott lemma dist.succLeft : Π (n m : ℕ), dist (n + 1) m ≤ dist n m + 1 | Nat.zero, Nat.zero => idp _ | Nat.succ n, Nat.zero => max.refl _ | Nat.zero, Nat.succ m => transport (· ≤ m + 2) (dist.zeroRight m)⁻¹ (le.trans (le.leSucc _) (le.leSucc _)) | Nat.succ n, Nat.succ m => succLeft n m - hott def max.leAdd : Π (n m : ℕ), le (max n m) (n + m) + hott lemma max.leAdd : Π (n m : ℕ), le (max n m) (n + m) | Nat.zero, Nat.zero => idp _ | Nat.succ n, Nat.zero => max.refl _ | Nat.zero, Nat.succ m => transport (m + 1 ≤ ·) (zeroPlus _)⁻¹ (max.refl _) @@ -315,16 +309,16 @@ namespace Nat end) -- ℕ-specific property - hott def dist.max : Π (n m : ℕ), dist n m ≤ max n m + hott theorem dist.max : Π (n m : ℕ), dist n m ≤ max n m | Nat.zero, Nat.zero => idp 0 | Nat.succ n, Nat.zero => max.refl _ | Nat.zero, Nat.succ m => max.refl _ | Nat.succ n, Nat.succ m => le.trans (max n m) (le.leSucc _) - hott def dist.le (n m : ℕ) : le (dist n m) (n + m) := + hott corollary dist.le (n m : ℕ) : le (dist n m) (n + m) := le.trans (dist.max n m) (max.leAdd n m) - hott def dist.translation (n m : ℕ) : Π k, dist n m = dist (n + k) (m + k) + hott lemma dist.translation (n m : ℕ) : Π k, dist n m = dist (n + k) (m + k) | Nat.zero => idp _ | Nat.succ k => translation n m k end Nat @@ -332,33 +326,33 @@ end Nat namespace UnitList universe u - def zero' : List 𝟏 := [] - def succ' : List 𝟏 → List 𝟏 := List.cons ★ + hott definition zero' : List 𝟏 := [] + hott definition succ' : List 𝟏 → List 𝟏 := List.cons ★ - def ind' {E : List 𝟏 → Type u} (e₀ : E zero') (eₛ : Π (n : List 𝟏), E n → E (succ' n)) : Π n, E n + hott definition ind' {E : List 𝟏 → Type u} (e₀ : E zero') (eₛ : Π (n : List 𝟏), E n → E (succ' n)) : Π n, E n | [] => e₀ | ★ :: xs => eₛ xs (ind' e₀ eₛ xs) - def encode : ℕ → List 𝟏 + hott definition encode : ℕ → List 𝟏 | Nat.zero => zero' | Nat.succ n => succ' (encode n) - def decode : List 𝟏 → ℕ + hott definition decode : List 𝟏 → ℕ | [] => Nat.zero | _ :: xs => Nat.succ (decode xs) - def decodeEncode : Π n, decode (encode n) = n + hott lemma decodeEncode : Π n, decode (encode n) = n | Nat.zero => idp _ | Nat.succ n => ap Nat.succ (decodeEncode n) - def encodeDecode : Π xs, encode (decode xs) = xs + hott lemma encodeDecode : Π xs, encode (decode xs) = xs | [] => idp _ | ★ :: xs => ap succ' (encodeDecode xs) - hott def iso : ℕ ≃ List 𝟏 := + hott theorem iso : ℕ ≃ List 𝟏 := ⟨encode, (⟨decode, decodeEncode⟩, ⟨decode, encodeDecode⟩)⟩ - noncomputable hott def equality : ℕ = List 𝟏 := ua iso + noncomputable hott corollary equality : ℕ = List 𝟏 := ua iso end UnitList end Theorems diff --git a/GroundZero/Types/Nat.lean b/GroundZero/Types/Nat.lean index df411ed..93d120b 100644 --- a/GroundZero/Types/Nat.lean +++ b/GroundZero/Types/Nat.lean @@ -1,9 +1,7 @@ -import GroundZero.HITs.Colimit import GroundZero.Structures open GroundZero.Types.Equiv (transport) open GroundZero.Types.Id (ap) -open GroundZero.Structures open GroundZero.Types open GroundZero @@ -39,7 +37,7 @@ begin | Coproduct.inl b => Coproduct.inl (e.left b) | Coproduct.inr c => Coproduct.inr c; - existsi f; apply Prod.mk <;> existsi g; + fapply Equiv.intro; exact f; exact g; { intro x; induction x using Sum.casesOn; apply ap Sum.inl; apply e.leftForward; reflexivity }; { intro x; induction x using Sum.casesOn; @@ -60,13 +58,6 @@ hott definition liftToTop (x : 𝟏) : Π n, pt 𝟏 n | Nat.zero => x | Nat.succ n => Coproduct.inl (liftToTop x n) -hott definition Iterated := -HITs.Colimit (pt 𝟏) liftUnit - -hott definition Iterated.encode : ℕ → Iterated -| Nat.zero => HITs.Colimit.inclusion 0 ★ -| Nat.succ n => HITs.Colimit.inclusion (n + 1) (Coproduct.inr ★) - hott definition code : ℕ → ℕ → Type | Nat.zero, Nat.zero => 𝟏 | Nat.succ m, Nat.zero => 𝟎