update dependency map & simple lemmas

forked-from-1kasper · Dec 23, 2023 · 2bdc27a · 2bdc27a
1 parent c46908b
commit 2bdc27a
Show file tree

Hide file tree

Showing 3 changed files with 644 additions and 627 deletions.
diff --git a/GroundZero/Structures.lean b/GroundZero/Structures.lean
@@ -127,6 +127,15 @@ namespace hlevel
   | n, −2     => (predPredSuccSucc n)⁻¹
   | n, succ m => ap succ (addNatToAdd n m)
 
+  hott lemma addNatSuccSucc : Π n m, addNat (succ (succ n)) m = succ (succ (addNat n m))
+  | n, Nat.zero   => idp (succ (succ n))
+  | n, Nat.succ m => ap succ (addNatSuccSucc n m)
+
+  hott lemma addSuccSucc : Π n m, add (succ (succ n)) m = addNat n (succSucc m)
+  | n, −2            => idp n
+  | n, −1            => idp (succ n)
+  | n, succ (succ m) => addNatSuccSucc n (succSucc m)
+
   instance : HAdd ℕ₋₂ ℕ₋₂ ℕ₋₂ := ⟨add⟩
 
   hott definition ofNat (n : ℕ) : ℕ₋₂ :=

diff --git a/GroundZero/Theorems/Nat.lean b/GroundZero/Theorems/Nat.lean
@@ -356,4 +356,18 @@ namespace UnitList
 end UnitList
 
 end Theorems
+
+namespace Structures
+open GroundZero.Theorems
+
+namespace hlevel
+  hott corollary comm : Π n m, add n m = add m n
+  | n, −2            => (minusTwoAdd n)⁻¹
+  | n, −1            => (minusOneAdd n)⁻¹
+  | n, succ (succ m) => addNatToAdd _ _ ⬝ ap predPred (Nat.comm _ _) ⬝
+                        (addNatToAdd _ _)⁻¹ ⬝ (addSuccSucc m n)⁻¹
+end hlevel
+
+end Structures
+
 end GroundZero