From 2bdc27a6eb3e2fca5ddb0a5c0840eb5684f1b53c Mon Sep 17 00:00:00 2001 From: Siegmentation Fault Date: Sat, 23 Dec 2023 15:27:24 +0700 Subject: [PATCH] update dependency map & simple lemmas --- GroundZero/Structures.lean | 9 + GroundZero/Theorems/Nat.lean | 14 + pictures/dependency-map.svg | 1248 +++++++++++++++++----------------- 3 files changed, 644 insertions(+), 627 deletions(-) diff --git a/GroundZero/Structures.lean b/GroundZero/Structures.lean index 62e9f5a..338af43 100644 --- 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 index 0b40531..d93e3fb 100644 --- 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 diff --git a/pictures/dependency-map.svg b/pictures/dependency-map.svg index 61bd890..34b578e 100644 --- a/pictures/dependency-map.svg +++ b/pictures/dependency-map.svg @@ -4,1450 +4,1444 @@ - + dependencyMap - + Algebra/Basic - -Algebra/Basic + +Algebra/Basic Algebra/Category - -Algebra/Category + +Algebra/Category Algebra/Basic->Algebra/Category - - + + Algebra/Geometry - -Algebra/Geometry + +Algebra/Geometry Algebra/Basic->Algebra/Geometry - - + + Algebra/Group/Basic - -Algebra/Group/Basic + +Algebra/Group/Basic Algebra/Basic->Algebra/Group/Basic - - + + Algebra/Monoid - -Algebra/Monoid + +Algebra/Monoid Algebra/Basic->Algebra/Monoid - - + + Algebra/Group/Automorphism - -Algebra/Group/Automorphism + +Algebra/Group/Automorphism Algebra/Group/Basic->Algebra/Group/Automorphism - - + + Algebra/EilenbergMacLane - -Algebra/EilenbergMacLane + +Algebra/EilenbergMacLane Algebra/Group/Basic->Algebra/EilenbergMacLane - - + + Algebra/Group/Absolutizer - -Algebra/Group/Absolutizer + +Algebra/Group/Absolutizer Algebra/Group/Basic->Algebra/Group/Absolutizer - - + + Algebra/Group/Finite - -Algebra/Group/Finite + +Algebra/Group/Finite Algebra/Group/Basic->Algebra/Group/Finite - - + + Algebra/Group/Free - -Algebra/Group/Free + +Algebra/Group/Free Algebra/Group/Basic->Algebra/Group/Free - - + + Algebra/Group/Periodic - -Algebra/Group/Periodic + +Algebra/Group/Periodic Algebra/Group/Basic->Algebra/Group/Periodic - - + + Algebra/Group/Product - -Algebra/Group/Product + +Algebra/Group/Product Algebra/Group/Basic->Algebra/Group/Product - - + + Algebra/Group/Subgroup - -Algebra/Group/Subgroup + +Algebra/Group/Subgroup Algebra/Group/Basic->Algebra/Group/Subgroup - - + + Algebra/Group/Action - -Algebra/Group/Action + +Algebra/Group/Action Algebra/Transformational - -Algebra/Transformational + +Algebra/Transformational Algebra/Group/Action->Algebra/Transformational - - + + Algebra/Group/Semidirect - -Algebra/Group/Semidirect + +Algebra/Group/Semidirect Algebra/Group/Automorphism->Algebra/Group/Semidirect - - + + Algebra/Group/Presentation - -Algebra/Group/Presentation + +Algebra/Group/Presentation Algebra/Group/Free->Algebra/Group/Presentation - - + + Algebra/Group/Product->Algebra/Transformational - - + + Algebra/Group/Factor - -Algebra/Group/Factor + +Algebra/Group/Factor Algebra/Group/Subgroup->Algebra/Group/Factor - - + + Algebra/Group/Differential - -Algebra/Group/Differential + +Algebra/Group/Differential Algebra/Group/Subgroup->Algebra/Group/Differential - - + + Algebra/Group/Lemmas - -Algebra/Group/Lemmas + +Algebra/Group/Lemmas Algebra/Group/Subgroup->Algebra/Group/Lemmas - - + + Algebra/Group/Symmetric - -Algebra/Group/Symmetric + +Algebra/Group/Symmetric Algebra/Group/Subgroup->Algebra/Group/Symmetric - - + + Algebra/Group/Alternating - -Algebra/Group/Alternating + +Algebra/Group/Alternating Algebra/Group/Factor->Algebra/Group/Alternating - - + + Algebra/Group/Isomorphism - -Algebra/Group/Isomorphism + +Algebra/Group/Isomorphism Algebra/Group/Factor->Algebra/Group/Isomorphism - - + + Algebra/Ring - -Algebra/Ring + +Algebra/Ring Algebra/Group/Factor->Algebra/Ring - - + + Algebra/Group/Isomorphism->Algebra/Group/Presentation - - + + Algebra/Orgraph - -Algebra/Orgraph + +Algebra/Orgraph Algebra/Ring->Algebra/Orgraph - - + + Algebra/Boolean - -Algebra/Boolean + +Algebra/Boolean Algebra/Ring->Algebra/Boolean - - + + Algebra/Group/Symmetric->Algebra/Group/Action - - + + Algebra/Group/Symmetric->Algebra/Group/Isomorphism - - + + Algebra/Group/Limited - -Algebra/Group/Limited + +Algebra/Group/Limited Algebra/Group/Symmetric->Algebra/Group/Limited - - + + Algebra/Group/Z - -Algebra/Group/Z + +Algebra/Group/Z Algebra/Group/Symmetric->Algebra/Group/Z - - + + Algebra/Reals - -Algebra/Reals + +Algebra/Reals Algebra/Orgraph->Algebra/Reals - - + + Algebra/Reals->Algebra/Group/Limited - - + + HITs/Topologization - -HITs/Topologization + +HITs/Topologization Algebra/Reals->HITs/Topologization - - + + Cubical/Path - -Cubical/Path + +Cubical/Path Cubical/Connection - -Cubical/Connection + +Cubical/Connection Cubical/Path->Cubical/Connection - - + + Cubical/V - -Cubical/V + +Cubical/V Cubical/Path->Cubical/V - - + + Cubical/Example - -Cubical/Example + +Cubical/Example Cubical/V->Cubical/Example - - + + Exercises/Chap1 - -Exercises/Chap1 + +Exercises/Chap1 Exercises/Chap3 - -Exercises/Chap3 + +Exercises/Chap3 Exercises/Chap1->Exercises/Chap3 - - + + Exercises/Chap2 - -Exercises/Chap2 + +Exercises/Chap2 Exercises/Chap4 - -Exercises/Chap4 + +Exercises/Chap4 Exercises/Chap2->Exercises/Chap4 - - + + Exercises/Chap5 - -Exercises/Chap5 + +Exercises/Chap5 Exercises/Chap4->Exercises/Chap5 - - + + HITs/Circle - -HITs/Circle + +HITs/Circle HITs/Circle->Algebra/Group/Z - - + + HITs/Circle->Exercises/Chap4 - - + + HITs/Moebius - -HITs/Moebius + +HITs/Moebius HITs/Circle->HITs/Moebius - - + + HITs/Reals - -HITs/Reals + +HITs/Reals HITs/Circle->HITs/Reals - - + + HITs/Sphere - -HITs/Sphere + +HITs/Sphere HITs/Circle->HITs/Sphere - - + + Theorems/Hopf - -Theorems/Hopf + +Theorems/Hopf HITs/Circle->Theorems/Hopf - - + + - + Types/CellComplex - -Types/CellComplex + +Types/CellComplex - + HITs/Sphere->Types/CellComplex - - + + HITs/Coequalizer - -HITs/Coequalizer + +HITs/Coequalizer HITs/Flattening - -HITs/Flattening + +HITs/Flattening HITs/Coequalizer->HITs/Flattening - - + + HITs/Colimit - -HITs/Colimit + +HITs/Colimit HITs/Merely - -HITs/Merely + +HITs/Merely HITs/Colimit->HITs/Merely - - - - - -Types/Nat - -Types/Nat - - - -HITs/Colimit->Types/Nat - - + + - + Theorems/Equiv - -Theorems/Equiv + +Theorems/Equiv - + HITs/Merely->Theorems/Equiv - - + + - + HITs/Simplicial - -HITs/Simplicial + +HITs/Simplicial - + HITs/Merely->HITs/Simplicial - - + + - + HITs/Trunc - -HITs/Trunc + +HITs/Trunc - + HITs/Merely->HITs/Trunc - - + + - + Theorems/Functions - -Theorems/Functions + +Theorems/Functions - + HITs/Merely->Theorems/Functions - - - - - -Theorems/Nat - -Theorems/Nat - - - -Types/Nat->Theorems/Nat - - + + - + HITs/Generalized - -HITs/Generalized + +HITs/Generalized - + HITs/Generalized->HITs/Merely - - + + - + HITs/Interval - -HITs/Interval + +HITs/Interval - + HITs/Interval->Cubical/Path - - + + - + Cubical/Cubes - -Cubical/Cubes + +Cubical/Cubes - + HITs/Interval->Cubical/Cubes - - + + - + HITs/Interval->Theorems/Equiv - - + + - + Theorems/Fibration - -Theorems/Fibration + +Theorems/Fibration - + HITs/Interval->Theorems/Fibration - - + + - + Theorems/Equiv->Exercises/Chap3 - - + + - + Theorems/Equiv->Exercises/Chap4 - - + + Theorems/Pullback - -Theorems/Pullback + +Theorems/Pullback - + Theorems/Equiv->Theorems/Pullback - - + + Theorems/Univalence - -Theorems/Univalence + +Theorems/Univalence - + Theorems/Equiv->Theorems/Univalence - - + + Types/Precategory - -Types/Precategory + +Types/Precategory - + Theorems/Equiv->Types/Precategory - - + + - + Theorems/Fibration->Theorems/Hopf - - + + - + HITs/Trunc->Algebra/Monoid - - + + - + HITs/Trunc->Algebra/EilenbergMacLane - - + + - + HITs/Trunc->HITs/Sphere - - + + - + HITs/Setquot - -HITs/Setquot + +HITs/Setquot - + HITs/Trunc->HITs/Setquot - - + + - + Theorems/Connectedness - -Theorems/Connectedness + +Theorems/Connectedness - + HITs/Trunc->Theorems/Connectedness - - + + - + Theorems/Functions->Exercises/Chap4 - - + + - + Modal/Etale - -Modal/Etale + +Modal/Etale - + Theorems/Functions->Modal/Etale - - + + - + Theorems/Functions->Theorems/Univalence - - + + - + Theorems/Functions->Types/Precategory - - + + - + HITs/Pushout - -HITs/Pushout + +HITs/Pushout - + HITs/Suspension - -HITs/Suspension + +HITs/Suspension - + HITs/Pushout->HITs/Suspension - - + + - + HITs/Wedge - -HITs/Wedge + +HITs/Wedge - + HITs/Pushout->HITs/Wedge - - + + - + HITs/Suspension->Algebra/EilenbergMacLane - - + + - + HITs/Suspension->HITs/Circle - - + + - + HITs/Join - -HITs/Join + +HITs/Join - + HITs/Suspension->HITs/Join - - + + - + HITs/Quotient - -HITs/Quotient + +HITs/Quotient - + HITs/Quotient->HITs/Coequalizer - - + + - + HITs/Quotient->HITs/Colimit - - + + - + HITs/Quotient->HITs/Generalized - - + + - + HITs/Quotient->HITs/Pushout - - + + - + HITs/Setquot->Algebra/Group/Action - - + + - + HITs/Setquot->Algebra/Group/Absolutizer - - + + - + HITs/Setquot->Algebra/Group/Factor - - + + - + Meta/Basic - -Meta/Basic + +Meta/Basic - + Proto - -Proto + +Proto - + Meta/Basic->Proto - - + + - + Theorems/Ontological - -Theorems/Ontological + +Theorems/Ontological - + Proto->Theorems/Ontological - - + + - + Types/Id - -Types/Id + +Types/Id - + Proto->Types/Id - - + + - + Meta/HottTheory - -Meta/HottTheory + +Meta/HottTheory - + Meta/HottTheory->Meta/Basic - - + + - + Meta/Notation - -Meta/Notation + +Meta/Notation - + Meta/Notation->Meta/Basic - - + + - + Meta/Tactic - -Meta/Tactic + +Meta/Tactic - + Meta/Tactic->Meta/Basic - - + + - + Meta/Trust - -Meta/Trust + +Meta/Trust - + Types/Equiv - -Types/Equiv + +Types/Equiv - + Meta/Trust->Types/Equiv - - + + - + Modal/Infinitesimal - -Modal/Infinitesimal + +Modal/Infinitesimal - + Types/Equiv->Modal/Infinitesimal - - + + Types/Coproduct - -Types/Coproduct + +Types/Coproduct - + Types/Equiv->Types/Coproduct - - + + Types/HEq - -Types/HEq + +Types/HEq - + Types/Equiv->Types/HEq - - + + Types/Lost - -Types/Lost + +Types/Lost - + Types/Equiv->Types/Lost - - + + Types/Sigma - -Types/Sigma + +Types/Sigma - + Types/Equiv->Types/Sigma - - + + Types/Unit - -Types/Unit + +Types/Unit - + Types/Equiv->Types/Unit - - + + - + Modal/Disc - -Modal/Disc + +Modal/Disc - + Modal/Disc->Modal/Etale - - + + - + Modal/Infinitesimal->Modal/Disc - - + + - + Types/Id->Meta/Trust - - + + - + Structures - -Structures + +Structures - + Structures->HITs/Merely - - - - - -Structures->Types/Nat - - + + - + Structures->HITs/Interval - - + + - + Structures->Modal/Disc - - + + - + Theorems/Weak - -Theorems/Weak + +Theorems/Weak - + Structures->Theorems/Weak - - + + + + + +Types/Nat + +Types/Nat + + + +Structures->Types/Nat + + + + + +Theorems/Nat + +Theorems/Nat + + + +Types/Nat->Theorems/Nat + + Theorems/Classical - -Theorems/Classical + +Theorems/Classical - + Theorems/Classical->Algebra/Category - - + + - + Theorems/Classical->Algebra/Orgraph - - + + - + Theorems/Pullback->Exercises/Chap2 - - + + - + Theorems/Univalence->Cubical/V - - + + - + Theorems/Univalence->Exercises/Chap2 - - + + - + Theorems/Univalence->HITs/Circle - - + + - + Theorems/Univalence->HITs/Flattening - - + + - + Theorems/Univalence->Theorems/Connectedness - - + + - + Theorems/Univalence->Theorems/Classical - - + + - + Theorems/Univalence->Theorems/Nat - - + + Types/Ens - -Types/Ens + +Types/Ens - + Theorems/Univalence->Types/Ens - - + + Types/Category - -Types/Category + +Types/Category - + Types/Precategory->Types/Category - - + + Theorems/Funext - -Theorems/Funext + +Theorems/Funext Types/Product - -Types/Product + +Types/Product - + Theorems/Funext->Types/Product - - + + - + Types/Product->Exercises/Chap1 - - + + - + Types/Product->Exercises/Chap4 - - + + - + Types/Product->Structures - - + + - + Theorems/Nat->Algebra/Group/Finite - - + + - + Theorems/Nat->Algebra/Group/Lemmas - - + + - + Theorems/Nat->Algebra/Reals - - + + - + Theorems/Nat->Exercises/Chap1 - - + + - + Theorems/Nat->Exercises/Chap4 - - + + HITs/Int - -HITs/Int + +HITs/Int - + Theorems/Nat->HITs/Int - - + + Types/Integer - -Types/Integer + +Types/Integer - + Theorems/Nat->Types/Integer - - + + - + Types/Integer->HITs/Circle - - + + - + Types/Ens->Algebra/Basic - - + + Types/Setquot - -Types/Setquot + +Types/Setquot - + Types/Ens->Types/Setquot - - + + - + Types/Coproduct->Structures - - + + - + Types/HEq->HITs/Quotient - - + + - + Types/HEq->Theorems/Funext - - + + - + Types/Lost->Exercises/Chap3 - - + + - + Types/Lost->Exercises/Chap5 - - + + - + Types/Sigma->Exercises/Chap1 - - + + - + Types/Sigma->Exercises/Chap4 - - + + - + Types/Sigma->Structures - - + + - + Types/Unit->HITs/Suspension - - + + - + Types/Unit->HITs/Wedge - - + + - + Types/Unit->Structures - - + +