From 53a6f43631bbe67d3e81e1fd8152b4b0daeecd16 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Tue, 11 Feb 2025 14:19:20 +0100
Subject: [PATCH 01/17] Initial commit

---
 Mathlib.lean                                  |   1 +
 .../GeneratorsRelations/Basic.lean            | 306 ++++++++++++++++++
 2 files changed, 307 insertions(+)
 create mode 100644 Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 02ebd19c19587..44b2e55f1706f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1128,6 +1128,7 @@ import Mathlib.AlgebraicTopology.Quasicategory.Basic
 import Mathlib.AlgebraicTopology.Quasicategory.Nerve
 import Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
 import Mathlib.AlgebraicTopology.SimplexCategory
+import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
 import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
 import Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
 import Mathlib.AlgebraicTopology.SimplicialNerve
diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
new file mode 100644
index 0000000000000..0ba40245a0ebd
--- /dev/null
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
@@ -0,0 +1,306 @@
+/-
+Copyright (c) 2025 Robin Carlier. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Carlier
+-/
+import Mathlib.CategoryTheory.PathCategory.MorphismProperty
+import Mathlib.AlgebraicTopology.SimplexCategory
+/-! # Presentation of the simplex category by generator and relations.
+
+We introduce `SimplexCategoryGenRel` as a the category presented by generating
+morphisms `δ i : [n] ⟶ [n + 1]` and `σ i : [n + 1] ⟶ [n]` and subject to the
+simplicial identities, and we provide induction principles for reasoning about
+objects and morphisms in this category.
+
+This category admits a canonical functor `toSimplexCategory` to the usual simplex category.
+The fact that this functor is an equivalence will be recorded in a separate file.
+-/
+namespace AlgebraicTopology.SimplexCategory
+
+open CategoryTheory
+
+/-- The objects of the free simplex quiver are the natural numbers. -/
+def FreeSimplexQuiver := ℕ
+
+/-- Making an object of `FreeSimplexQuiver` out of a natural number. -/
+def FreeSimplexQuiver.mk (n : ℕ) : FreeSimplexQuiver := n
+
+/-- Getting back the natural number from the objects. -/
+def FreeSimplexQuiver.len (x : FreeSimplexQuiver) : ℕ := x
+
+namespace FreeSimplexQuiver
+
+/-- A morphisms in `FreeSimplexQuiver` is either a face map (`δ`) or a degeneracy map (`σ`). -/
+inductive Hom : FreeSimplexQuiver → FreeSimplexQuiver → Type
+  | δ {n : ℕ} (i : Fin (n + 2)) : Hom (.mk n) (.mk (n + 1))
+  | σ {n : ℕ} (i : Fin (n + 1)) : Hom (.mk (n + 1)) (.mk n)
+
+instance Quiv : Quiver FreeSimplexQuiver where
+  Hom := FreeSimplexQuiver.Hom
+
+/-- `FreeSimplexQuiver.δ i` represents the `i`-th face map `.mk n ⟶ .mk (n + 1)`. -/
+abbrev δ {n : ℕ} (i : Fin (n + 2)) : FreeSimplexQuiver.mk n ⟶ .mk (n + 1) :=
+  FreeSimplexQuiver.Hom.δ i
+
+/-- `FreeSimplexQuiver.σ i` represents `i`-th degeneracy map `.mk (n + 1) ⟶ .mk n`. -/
+abbrev σ {n : ℕ} (i : Fin (n + 1)) : FreeSimplexQuiver.mk (n + 1) ⟶ .mk n :=
+  FreeSimplexQuiver.Hom.σ i
+
+/-- `FreeSimplexQuiver.homRel` is the relation on morphisms freely generated on the
+five simplicial identities. -/
+inductive homRel : HomRel (Paths FreeSimplexQuiver)
+  | simplicial1 {n : ℕ} {i j : Fin (n + 2)} (H : i ≤ j) : homRel
+    (Paths.of.map (δ i) ≫ Paths.of.map (δ j.succ))
+    (Paths.of.map (δ j) ≫ Paths.of.map (δ i.castSucc))
+  | simplicial2 {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc) : homRel
+    (Paths.of.map (δ i.castSucc) ≫ Paths.of.map (σ j.succ))
+    (Paths.of.map (σ j) ≫ Paths.of.map (δ i))
+  | simplicial3₁ {n : ℕ} {i : Fin (n + 1)} : homRel
+    (Paths.of.map (δ i.castSucc) ≫ Paths.of.map (σ i)) (𝟙 _)
+  | simplicial3₂ {n : ℕ} {i : Fin (n + 1)} : homRel
+    (Paths.of.map (δ i.succ) ≫ Paths.of.map (σ i)) (𝟙 _)
+  | simplicial4 {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) : homRel
+    (Paths.of.map (δ i.succ) ≫ Paths.of.map (σ j.castSucc))
+    (Paths.of.map (σ j) ≫ Paths.of.map (δ i))
+  | simplicial5 {n : ℕ} {i j : Fin (n + 1)} (H : i ≤ j) : homRel
+    (Paths.of.map (σ i.castSucc) ≫ Paths.of.map (σ j))
+    (Paths.of.map (σ j.succ) ≫ Paths.of.map (σ i))
+
+end FreeSimplexQuiver
+
+/-- SimplexCategory is the category presented by generators and relation by the simplicial
+identities.-/
+def SimplexCategoryGenRel := Quotient FreeSimplexQuiver.homRel
+  deriving Category
+
+/-- `SimplexCategoryGenRel.mk` is the main constructor for objects of `SimplexCategoryGenRel`. -/
+def SimplexCategoryGenRel.mk (n : ℕ) : SimplexCategoryGenRel where
+  as := Paths.of.obj n
+
+namespace SimplexCategoryGenRel
+
+/-- `SimplexCategoryGenRel.δ i` is the `i`-th face map `.mk n ⟶ .mk (n + 1)`. -/
+abbrev δ {n : ℕ} (i : Fin (n + 2)) : (SimplexCategoryGenRel.mk n) ⟶ .mk (n + 1) :=
+  (Quotient.functor FreeSimplexQuiver.homRel).map <| Paths.of.map (.δ i)
+
+/-- `SimplexCategoryGenRel.σ i` is the `i`-th degeneracy map `.mk (n + 1) ⟶ .mk n`. -/
+abbrev σ {n : ℕ} (i : Fin (n + 1)) :
+    (SimplexCategoryGenRel.mk (n + 1)) ⟶ (SimplexCategoryGenRel.mk n) :=
+  (Quotient.functor FreeSimplexQuiver.homRel).map <| Paths.of.map (.σ i)
+
+/-- The length of an object of `SimplexCategoryGenRel`. -/
+def len (x : SimplexCategoryGenRel) : ℕ := by rcases x with ⟨n⟩; exact n
+
+@[simp]
+lemma mk_len (n : ℕ) : (len (mk n)) = n := rfl
+
+section InductionPrinciples
+
+/-- An induction principle for reasonning about morphisms properties in SimplexCategoryGenRel. -/
+lemma hom_induction (P : MorphismProperty SimplexCategoryGenRel)
+    (hi : ∀ {n : ℕ}, P (𝟙 (.mk n)))
+    (hc₁ : ∀ {n m : ℕ} (u : .mk n ⟶ .mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i))
+    (hc₂ : ∀ {n m : ℕ} (u : .mk n ⟶ .mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i))
+    {a b : SimplexCategoryGenRel} (f : a ⟶ b) :
+    P f := by
+  apply CategoryTheory.Quotient.induction (P := (fun f ↦ P f))
+  apply Paths.induction
+  · exact hi
+  · rintro _ _ _ _ ⟨⟩
+    · exact hc₁ _ _
+    · exact hc₂ _ _
+
+/-- An induction principle for reasonning about morphisms in SimplexCategoryGenRel, where we compose
+with generators on the right. -/
+lemma hom_induction' (P : MorphismProperty SimplexCategoryGenRel)
+    (hi : ∀ {n : ℕ}, P (𝟙 (SimplexCategoryGenRel.mk n)))
+    (hc₁ : ∀ {n m : ℕ} (u : SimplexCategoryGenRel.mk (m + 1) ⟶ SimplexCategoryGenRel.mk n)
+      (i : Fin (m + 2)), P u → P (δ i ≫ u))
+    (hc₂ : ∀ {n m : ℕ} (u : SimplexCategoryGenRel.mk m ⟶ SimplexCategoryGenRel.mk n)
+      (i : Fin (m + 1)), P u → P (σ i ≫ u )) {a b : SimplexCategoryGenRel} (f : a ⟶ b) :
+    P f := by
+  apply CategoryTheory.Quotient.induction (P := (fun f ↦ P f))
+  apply Paths.induction'
+  · exact hi
+  · rintro _ _ _ ⟨⟩ _
+    · exact hc₁ _ _
+    · exact hc₂ _ _
+
+/-- An induction principle for reasonning about morphisms properties in SimplexCategoryGenRel. -/
+lemma hom_induction_eq_top (P : MorphismProperty SimplexCategoryGenRel)
+    (hi : ∀ {n : ℕ}, P (𝟙 (.mk n)))
+    (hc₁ : ∀ {n m : ℕ} (u : .mk n ⟶ .mk m) (i : Fin (m + 2)),
+      P u → P (u ≫ δ i))
+    (hc₂ : ∀ {n m : ℕ} (u : .mk n ⟶ .mk (m + 1))
+      (i : Fin (m + 1)), P u → P (u ≫ σ i)) :
+    P = ⊤ := by
+  ext; constructor
+  · simp
+  · intro _
+    apply hom_induction <;> assumption
+
+/-- An induction principle for reasonning about morphisms properties in SimplexCategoryGenRel,
+where we compose with generators on the right. -/
+lemma hom_induction_eq_top' (P : MorphismProperty SimplexCategoryGenRel)
+    (hi : ∀ {n : ℕ}, P (𝟙 (.mk n)))
+    (hc₁ : ∀ {n m : ℕ} (u : .mk (m + 1) ⟶ .mk n) (i : Fin (m + 2)), P u → (P (δ i ≫ u)))
+    (hc₂ : ∀ {n m : ℕ} (u : .mk m ⟶ .mk n) (i : Fin (m + 1)), P u → (P (σ i ≫ u ))) :
+    P = ⊤ := by
+  ext; constructor
+  · simp
+  · intro _
+    apply hom_induction' <;> assumption
+
+/-- An induction principle for reasonning about objects in SimplexCategoryGenRel. This should be
+used instead of identifying an object with `mk` of its len.-/
+@[elab_as_elim]
+def obj_induction {P : SimplexCategoryGenRel → Sort*}
+    (H : ∀ n : ℕ, P (.mk n)) :
+    ∀ x : SimplexCategoryGenRel, P x := by
+  intro x
+  exact H x.len
+
+/-- A basic ext lemma for objects of SimplexCategoryGenRel --/
+@[ext]
+lemma obj_ext {x y : SimplexCategoryGenRel} (h : x.len = y.len) : x = y := by
+  cases x using obj_induction
+  cases y using obj_induction
+  simp only [mk_len] at h
+  congr
+
+end InductionPrinciples
+
+section SimplicialIdentities
+
+@[reassoc]
+theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) :
+    δ i ≫ δ j.succ = δ j ≫ δ i.castSucc := by
+  apply CategoryTheory.Quotient.sound
+  exact FreeSimplexQuiver.homRel.simplicial1 H
+
+@[reassoc]
+theorem δ_comp_σ_of_le {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc) :
+    δ i.castSucc ≫ σ j.succ = σ j ≫ δ i := by
+  apply CategoryTheory.Quotient.sound
+  exact FreeSimplexQuiver.homRel.simplicial2 H
+
+@[reassoc]
+theorem δ_comp_σ_self {n} {i : Fin (n + 1)} :
+    δ i.castSucc ≫ σ i = 𝟙 (mk n) := by
+  apply CategoryTheory.Quotient.sound
+  exact FreeSimplexQuiver.homRel.simplicial3₁
+
+@[reassoc]
+theorem δ_comp_σ_succ {n} {i : Fin (n + 1)} : δ i.succ ≫ σ i = 𝟙 (mk n) := by
+  apply CategoryTheory.Quotient.sound
+  exact FreeSimplexQuiver.homRel.simplicial3₂
+
+@[reassoc]
+theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) :
+    δ i.succ ≫ σ j.castSucc = σ j ≫ δ i := by
+  apply CategoryTheory.Quotient.sound
+  exact FreeSimplexQuiver.homRel.simplicial4 H
+
+@[reassoc]
+theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) :
+    σ i.castSucc ≫ σ j = σ j.succ ≫ σ i := by
+  apply CategoryTheory.Quotient.sound
+  exact FreeSimplexQuiver.homRel.simplicial5 H
+
+/-- A version of δ_comp_δ with indices in ℕ satisfying relevant inequalities. -/
+lemma δ_comp_δ_nat {n} (i j : ℕ) (hi : i < n + 2) (hj : j < n + 2) (H : i ≤ j) :
+    δ (i : Fin (n + 2)) ≫ δ ↑(j + 1) = δ ↑j ≫ δ ↑i := by
+  let i₁ : Fin (n + 2) := ⟨i, hi⟩
+  let j₁ : Fin (n + 2) := ⟨j, hj⟩
+  conv_lhs =>
+    congr
+    · right
+      equals i₁ =>
+        congr
+        ext
+        simp only [Fin.val_natCast, Nat.mod_eq_of_lt hi]
+        rfl
+    · right
+      equals j₁.succ =>
+        congr
+        ext
+        simp only [Fin.val_natCast]
+        rw [Nat.mod_eq_of_lt]
+        · rfl
+        · omega
+  rw [δ_comp_δ (by simpa)]
+  congr
+  · ext
+    simp only [Fin.val_succ, Fin.val_natCast, Nat.mod_eq_of_lt hj,
+      Nat.mod_eq_of_lt (Nat.succ_lt_succ hi), Nat.succ_eq_add_one, add_left_inj ]
+    rfl
+  · ext
+    simp only [Fin.val_succ, Fin.val_natCast, Nat.succ_eq_add_one, add_left_inj ]
+    rw [Nat.mod_eq_of_lt]
+    · rfl
+    · omega
+
+/-- A version of σ_comp_σ with indices in ℕ satisfying relevant inequalities. -/
+lemma σ_comp_σ_nat {n} (i j : ℕ) (hi : i < n + 1) (hj : j < n + 1) (H : i ≤ j) :
+    σ (i : Fin (n + 1 + 1)) ≫ σ (j : Fin (n + 1)) = σ ↑(j + 1) ≫ σ ↑i := by
+  let i₁ : Fin (n + 1) := ⟨i, hi⟩
+  let j₁ : Fin (n + 1) := ⟨j, hj⟩
+  conv_lhs =>
+    congr
+    · right
+      equals i₁.castSucc =>
+        congr
+        ext
+        simp only [Fin.val_natCast, Nat.mod_eq_of_lt (Nat.lt_succ_of_lt hi), Fin.coe_castSucc]
+        rfl
+    · right
+      equals j₁ =>
+        congr
+        ext
+        simp only [Fin.val_natCast, Nat.mod_eq_of_lt hj]
+        rfl
+  rw [σ_comp_σ (by simpa)]
+  congr <;> {
+    ext
+    simp only [Fin.val_succ, Fin.val_natCast, Nat.mod_eq_of_lt hi,
+      Nat.mod_eq_of_lt (Nat.succ_lt_succ hj), Nat.succ_eq_add_one, add_left_inj ]
+    rfl }
+
+end SimplicialIdentities
+
+/-- The canonical functor from `SimplexCategoryGenRel` to SimplexCategory, which exists as the
+simplicial identities hold in `SimplexCategory`. -/
+def toSimplexCategory : SimplexCategoryGenRel ⥤ SimplexCategory := by
+  fapply CategoryTheory.Quotient.lift
+  · fapply Paths.lift
+    exact { obj i := .mk i,
+            map f := match f with
+              | FreeSimplexQuiver.Hom.δ i => SimplexCategory.δ i
+              | FreeSimplexQuiver.Hom.σ i => SimplexCategory.σ i }
+  · intro x y f₁ f₂ h
+    cases h with
+    | simplicial1 H => exact SimplexCategory.δ_comp_δ H
+    | simplicial2 H => exact SimplexCategory.δ_comp_σ_of_le H
+    | simplicial3₁ => exact SimplexCategory.δ_comp_σ_self
+    | simplicial3₂ => exact SimplexCategory.δ_comp_σ_succ
+    | simplicial4 H => exact SimplexCategory.δ_comp_σ_of_gt H
+    | simplicial5 H => exact SimplexCategory.σ_comp_σ H
+
+@[simp]
+lemma toSimplexCategory_obj_mk (n : ℕ) : toSimplexCategory.obj (mk n) = .mk n := rfl
+
+@[simp]
+lemma toSimplexCategory_map_δ {n : ℕ} (i : Fin (n + 2)) : toSimplexCategory.map (δ i) =
+    SimplexCategory.δ i := rfl
+
+@[simp]
+lemma toSimplexCategory_map_σ {n : ℕ} (i : Fin (n + 1)) : toSimplexCategory.map (σ i) =
+    SimplexCategory.σ i := rfl
+
+@[simp]
+lemma toSimplexCategory_len {x : SimplexCategoryGenRel} : (toSimplexCategory.obj x).len = x.len :=
+  rfl
+
+end SimplexCategoryGenRel
+
+end AlgebraicTopology.SimplexCategory

From b5404f9b523a08cf0557a7c9ab21eada551ecbd5 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Tue, 11 Feb 2025 22:35:22 +0100
Subject: [PATCH 02/17] lake shake

---
 .../SimplexCategory/GeneratorsRelations/Basic.lean              | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
index 0ba40245a0ebd..2e00a97e354db 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
@@ -3,8 +3,8 @@ Copyright (c) 2025 Robin Carlier. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robin Carlier
 -/
-import Mathlib.CategoryTheory.PathCategory.MorphismProperty
 import Mathlib.AlgebraicTopology.SimplexCategory
+import Mathlib.CategoryTheory.PathCategory.Basic
 /-! # Presentation of the simplex category by generator and relations.
 
 We introduce `SimplexCategoryGenRel` as a the category presented by generating

From de993467685abbac416239cc558520011a4caed6 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Wed, 12 Feb 2025 11:58:25 +0100
Subject: [PATCH 03/17] Apply suggestions from code review
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
---
 .../GeneratorsRelations/Basic.lean            | 40 +++++++++----------
 1 file changed, 20 insertions(+), 20 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
index 2e00a97e354db..381f83087af2e 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
@@ -7,7 +7,7 @@ import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.CategoryTheory.PathCategory.Basic
 /-! # Presentation of the simplex category by generator and relations.
 
-We introduce `SimplexCategoryGenRel` as a the category presented by generating
+We introduce `SimplexCategoryGenRel` as the category presented by generating
 morphisms `δ i : [n] ⟶ [n + 1]` and `σ i : [n + 1] ⟶ [n]` and subject to the
 simplicial identities, and we provide induction principles for reasoning about
 objects and morphisms in this category.
@@ -30,7 +30,7 @@ def FreeSimplexQuiver.len (x : FreeSimplexQuiver) : ℕ := x
 
 namespace FreeSimplexQuiver
 
-/-- A morphisms in `FreeSimplexQuiver` is either a face map (`δ`) or a degeneracy map (`σ`). -/
+/-- A morphism in `FreeSimplexQuiver` is either a face map (`δ`) or a degeneracy map (`σ`). -/
 inductive Hom : FreeSimplexQuiver → FreeSimplexQuiver → Type
   | δ {n : ℕ} (i : Fin (n + 2)) : Hom (.mk n) (.mk (n + 1))
   | σ {n : ℕ} (i : Fin (n + 1)) : Hom (.mk (n + 1)) (.mk n)
@@ -127,7 +127,7 @@ lemma hom_induction' (P : MorphismProperty SimplexCategoryGenRel)
     · exact hc₂ _ _
 
 /-- An induction principle for reasonning about morphisms properties in SimplexCategoryGenRel. -/
-lemma hom_induction_eq_top (P : MorphismProperty SimplexCategoryGenRel)
+lemma morphismProperty_eq_top (P : MorphismProperty SimplexCategoryGenRel)
     (hi : ∀ {n : ℕ}, P (𝟙 (.mk n)))
     (hc₁ : ∀ {n m : ℕ} (u : .mk n ⟶ .mk m) (i : Fin (m + 2)),
       P u → P (u ≫ δ i))
@@ -154,7 +154,7 @@ lemma hom_induction_eq_top' (P : MorphismProperty SimplexCategoryGenRel)
 /-- An induction principle for reasonning about objects in SimplexCategoryGenRel. This should be
 used instead of identifying an object with `mk` of its len.-/
 @[elab_as_elim]
-def obj_induction {P : SimplexCategoryGenRel → Sort*}
+protected def rec {P : SimplexCategoryGenRel → Sort*}
     (H : ∀ n : ℕ, P (.mk n)) :
     ∀ x : SimplexCategoryGenRel, P x := by
   intro x
@@ -162,7 +162,7 @@ def obj_induction {P : SimplexCategoryGenRel → Sort*}
 
 /-- A basic ext lemma for objects of SimplexCategoryGenRel --/
 @[ext]
-lemma obj_ext {x y : SimplexCategoryGenRel} (h : x.len = y.len) : x = y := by
+lemma ext {x y : SimplexCategoryGenRel} (h : x.len = y.len) : x = y := by
   cases x using obj_induction
   cases y using obj_induction
   simp only [mk_len] at h
@@ -270,21 +270,21 @@ end SimplicialIdentities
 
 /-- The canonical functor from `SimplexCategoryGenRel` to SimplexCategory, which exists as the
 simplicial identities hold in `SimplexCategory`. -/
-def toSimplexCategory : SimplexCategoryGenRel ⥤ SimplexCategory := by
-  fapply CategoryTheory.Quotient.lift
-  · fapply Paths.lift
-    exact { obj i := .mk i,
-            map f := match f with
-              | FreeSimplexQuiver.Hom.δ i => SimplexCategory.δ i
-              | FreeSimplexQuiver.Hom.σ i => SimplexCategory.σ i }
-  · intro x y f₁ f₂ h
-    cases h with
-    | simplicial1 H => exact SimplexCategory.δ_comp_δ H
-    | simplicial2 H => exact SimplexCategory.δ_comp_σ_of_le H
-    | simplicial3₁ => exact SimplexCategory.δ_comp_σ_self
-    | simplicial3₂ => exact SimplexCategory.δ_comp_σ_succ
-    | simplicial4 H => exact SimplexCategory.δ_comp_σ_of_gt H
-    | simplicial5 H => exact SimplexCategory.σ_comp_σ H
+def toSimplexCategory : SimplexCategoryGenRel ⥤ SimplexCategory :=
+  CategoryTheory.Quotient.lift _
+    (Paths.lift
+      { obj := .mk
+        map f := match f with
+          | FreeSimplexQuiver.Hom.δ i => SimplexCategory.δ i
+          | FreeSimplexQuiver.Hom.σ i => SimplexCategory.σ i })
+    (fun _ _ _ _ h ↦ by
+      cases h with
+      | simplicial1 H => exact SimplexCategory.δ_comp_δ H
+      | simplicial2 H => exact SimplexCategory.δ_comp_σ_of_le H
+      | simplicial3₁ => exact SimplexCategory.δ_comp_σ_self
+      | simplicial3₂ => exact SimplexCategory.δ_comp_σ_succ
+      | simplicial4 H => exact SimplexCategory.δ_comp_σ_of_gt H
+      | simplicial5 H => exact SimplexCategory.σ_comp_σ H)
 
 @[simp]
 lemma toSimplexCategory_obj_mk (n : ℕ) : toSimplexCategory.obj (mk n) = .mk n := rfl

From 8307c3ed0d2d20b353a79074d0a8fa6c186743b1 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Wed, 12 Feb 2025 12:04:33 +0100
Subject: [PATCH 04/17] fix build

---
 .../SimplexCategory/GeneratorsRelations/Basic.lean          | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
index 381f83087af2e..8b62cf559cc7f 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
@@ -153,7 +153,7 @@ lemma hom_induction_eq_top' (P : MorphismProperty SimplexCategoryGenRel)
 
 /-- An induction principle for reasonning about objects in SimplexCategoryGenRel. This should be
 used instead of identifying an object with `mk` of its len.-/
-@[elab_as_elim]
+@[elab_as_elim, cases_eliminator]
 protected def rec {P : SimplexCategoryGenRel → Sort*}
     (H : ∀ n : ℕ, P (.mk n)) :
     ∀ x : SimplexCategoryGenRel, P x := by
@@ -163,8 +163,8 @@ protected def rec {P : SimplexCategoryGenRel → Sort*}
 /-- A basic ext lemma for objects of SimplexCategoryGenRel --/
 @[ext]
 lemma ext {x y : SimplexCategoryGenRel} (h : x.len = y.len) : x = y := by
-  cases x using obj_induction
-  cases y using obj_induction
+  cases x
+  cases y
   simp only [mk_len] at h
   congr
 

From f36825f5eff77cace9a9b185c069ab910d08f056 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Wed, 12 Feb 2025 12:04:50 +0100
Subject: [PATCH 05/17] change namespace

---
 .../SimplexCategory/GeneratorsRelations/Basic.lean            | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
index 8b62cf559cc7f..44f006d8a00dd 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
@@ -15,7 +15,7 @@ objects and morphisms in this category.
 This category admits a canonical functor `toSimplexCategory` to the usual simplex category.
 The fact that this functor is an equivalence will be recorded in a separate file.
 -/
-namespace AlgebraicTopology.SimplexCategory
+namespace AlgebraicTopology
 
 open CategoryTheory
 
@@ -303,4 +303,4 @@ lemma toSimplexCategory_len {x : SimplexCategoryGenRel} : (toSimplexCategory.obj
 
 end SimplexCategoryGenRel
 
-end AlgebraicTopology.SimplexCategory
+end AlgebraicTopology

From 89e52642b62b0ec2fd657ab9f8808bbdd2fce69d Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Wed, 12 Feb 2025 12:08:31 +0100
Subject: [PATCH 06/17] mirror names

---
 .../GeneratorsRelations/Basic.lean            | 36 +++++++++----------
 1 file changed, 18 insertions(+), 18 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
index 44f006d8a00dd..e02d4e9f80f0a 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
@@ -49,20 +49,20 @@ abbrev σ {n : ℕ} (i : Fin (n + 1)) : FreeSimplexQuiver.mk (n + 1) ⟶ .mk n :
 /-- `FreeSimplexQuiver.homRel` is the relation on morphisms freely generated on the
 five simplicial identities. -/
 inductive homRel : HomRel (Paths FreeSimplexQuiver)
-  | simplicial1 {n : ℕ} {i j : Fin (n + 2)} (H : i ≤ j) : homRel
+  | δ_comp_δ {n : ℕ} {i j : Fin (n + 2)} (H : i ≤ j) : homRel
     (Paths.of.map (δ i) ≫ Paths.of.map (δ j.succ))
     (Paths.of.map (δ j) ≫ Paths.of.map (δ i.castSucc))
-  | simplicial2 {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc) : homRel
+  | δ_comp_σ_of_le {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc) : homRel
     (Paths.of.map (δ i.castSucc) ≫ Paths.of.map (σ j.succ))
     (Paths.of.map (σ j) ≫ Paths.of.map (δ i))
-  | simplicial3₁ {n : ℕ} {i : Fin (n + 1)} : homRel
+  | δ_comp_σ_self {n : ℕ} {i : Fin (n + 1)} : homRel
     (Paths.of.map (δ i.castSucc) ≫ Paths.of.map (σ i)) (𝟙 _)
-  | simplicial3₂ {n : ℕ} {i : Fin (n + 1)} : homRel
+  | δ_comp_σ_succ {n : ℕ} {i : Fin (n + 1)} : homRel
     (Paths.of.map (δ i.succ) ≫ Paths.of.map (σ i)) (𝟙 _)
-  | simplicial4 {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) : homRel
+  | δ_comp_σ_of_gt {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) : homRel
     (Paths.of.map (δ i.succ) ≫ Paths.of.map (σ j.castSucc))
     (Paths.of.map (σ j) ≫ Paths.of.map (δ i))
-  | simplicial5 {n : ℕ} {i j : Fin (n + 1)} (H : i ≤ j) : homRel
+  | σ_comp_σ {n : ℕ} {i j : Fin (n + 1)} (H : i ≤ j) : homRel
     (Paths.of.map (σ i.castSucc) ≫ Paths.of.map (σ j))
     (Paths.of.map (σ j.succ) ≫ Paths.of.map (σ i))
 
@@ -176,36 +176,36 @@ section SimplicialIdentities
 theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) :
     δ i ≫ δ j.succ = δ j ≫ δ i.castSucc := by
   apply CategoryTheory.Quotient.sound
-  exact FreeSimplexQuiver.homRel.simplicial1 H
+  exact FreeSimplexQuiver.homRel.δ_comp_δ H
 
 @[reassoc]
 theorem δ_comp_σ_of_le {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc) :
     δ i.castSucc ≫ σ j.succ = σ j ≫ δ i := by
   apply CategoryTheory.Quotient.sound
-  exact FreeSimplexQuiver.homRel.simplicial2 H
+  exact FreeSimplexQuiver.homRel.δ_comp_σ_of_le H
 
 @[reassoc]
 theorem δ_comp_σ_self {n} {i : Fin (n + 1)} :
     δ i.castSucc ≫ σ i = 𝟙 (mk n) := by
   apply CategoryTheory.Quotient.sound
-  exact FreeSimplexQuiver.homRel.simplicial3₁
+  exact FreeSimplexQuiver.homRel.δ_comp_σ_self
 
 @[reassoc]
 theorem δ_comp_σ_succ {n} {i : Fin (n + 1)} : δ i.succ ≫ σ i = 𝟙 (mk n) := by
   apply CategoryTheory.Quotient.sound
-  exact FreeSimplexQuiver.homRel.simplicial3₂
+  exact FreeSimplexQuiver.homRel.δ_comp_σ_succ
 
 @[reassoc]
 theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) :
     δ i.succ ≫ σ j.castSucc = σ j ≫ δ i := by
   apply CategoryTheory.Quotient.sound
-  exact FreeSimplexQuiver.homRel.simplicial4 H
+  exact FreeSimplexQuiver.homRel.δ_comp_σ_of_gt H
 
 @[reassoc]
 theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) :
     σ i.castSucc ≫ σ j = σ j.succ ≫ σ i := by
   apply CategoryTheory.Quotient.sound
-  exact FreeSimplexQuiver.homRel.simplicial5 H
+  exact FreeSimplexQuiver.homRel.σ_comp_σ H
 
 /-- A version of δ_comp_δ with indices in ℕ satisfying relevant inequalities. -/
 lemma δ_comp_δ_nat {n} (i j : ℕ) (hi : i < n + 2) (hj : j < n + 2) (H : i ≤ j) :
@@ -279,12 +279,12 @@ def toSimplexCategory : SimplexCategoryGenRel ⥤ SimplexCategory :=
           | FreeSimplexQuiver.Hom.σ i => SimplexCategory.σ i })
     (fun _ _ _ _ h ↦ by
       cases h with
-      | simplicial1 H => exact SimplexCategory.δ_comp_δ H
-      | simplicial2 H => exact SimplexCategory.δ_comp_σ_of_le H
-      | simplicial3₁ => exact SimplexCategory.δ_comp_σ_self
-      | simplicial3₂ => exact SimplexCategory.δ_comp_σ_succ
-      | simplicial4 H => exact SimplexCategory.δ_comp_σ_of_gt H
-      | simplicial5 H => exact SimplexCategory.σ_comp_σ H)
+      | δ_comp_δ H => exact SimplexCategory.δ_comp_δ H
+      | δ_comp_σ_of_le H => exact SimplexCategory.δ_comp_σ_of_le H
+      | δ_comp_σ_self => exact SimplexCategory.δ_comp_σ_self
+      | δ_comp_σ_succ => exact SimplexCategory.δ_comp_σ_succ
+      | δ_comp_σ_of_gt H => exact SimplexCategory.δ_comp_σ_of_gt H
+      | σ_comp_σ H => exact SimplexCategory.σ_comp_σ H)
 
 @[simp]
 lemma toSimplexCategory_obj_mk (n : ℕ) : toSimplexCategory.obj (mk n) = .mk n := rfl

From 0a75491dfcc0ce241df3dc6f0b68ba9edd834fa5 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Wed, 12 Feb 2025 12:12:48 +0100
Subject: [PATCH 07/17] better nat lemmas

---
 .../GeneratorsRelations/Basic.lean            | 57 ++-----------------
 1 file changed, 4 insertions(+), 53 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
index e02d4e9f80f0a..25d09a47a5640 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
@@ -209,62 +209,13 @@ theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) :
 
 /-- A version of δ_comp_δ with indices in ℕ satisfying relevant inequalities. -/
 lemma δ_comp_δ_nat {n} (i j : ℕ) (hi : i < n + 2) (hj : j < n + 2) (H : i ≤ j) :
-    δ (i : Fin (n + 2)) ≫ δ ↑(j + 1) = δ ↑j ≫ δ ↑i := by
-  let i₁ : Fin (n + 2) := ⟨i, hi⟩
-  let j₁ : Fin (n + 2) := ⟨j, hj⟩
-  conv_lhs =>
-    congr
-    · right
-      equals i₁ =>
-        congr
-        ext
-        simp only [Fin.val_natCast, Nat.mod_eq_of_lt hi]
-        rfl
-    · right
-      equals j₁.succ =>
-        congr
-        ext
-        simp only [Fin.val_natCast]
-        rw [Nat.mod_eq_of_lt]
-        · rfl
-        · omega
-  rw [δ_comp_δ (by simpa)]
-  congr
-  · ext
-    simp only [Fin.val_succ, Fin.val_natCast, Nat.mod_eq_of_lt hj,
-      Nat.mod_eq_of_lt (Nat.succ_lt_succ hi), Nat.succ_eq_add_one, add_left_inj ]
-    rfl
-  · ext
-    simp only [Fin.val_succ, Fin.val_natCast, Nat.succ_eq_add_one, add_left_inj ]
-    rw [Nat.mod_eq_of_lt]
-    · rfl
-    · omega
+    δ ⟨i, hi⟩ ≫ δ ⟨j + 1, by omega⟩ = δ ⟨j, hj⟩ ≫ δ ⟨i, by omega⟩ :=
+  δ_comp_δ (n := n) (i := ⟨i, by omega⟩) (j := ⟨j, by omega⟩) (by simpa)
 
 /-- A version of σ_comp_σ with indices in ℕ satisfying relevant inequalities. -/
 lemma σ_comp_σ_nat {n} (i j : ℕ) (hi : i < n + 1) (hj : j < n + 1) (H : i ≤ j) :
-    σ (i : Fin (n + 1 + 1)) ≫ σ (j : Fin (n + 1)) = σ ↑(j + 1) ≫ σ ↑i := by
-  let i₁ : Fin (n + 1) := ⟨i, hi⟩
-  let j₁ : Fin (n + 1) := ⟨j, hj⟩
-  conv_lhs =>
-    congr
-    · right
-      equals i₁.castSucc =>
-        congr
-        ext
-        simp only [Fin.val_natCast, Nat.mod_eq_of_lt (Nat.lt_succ_of_lt hi), Fin.coe_castSucc]
-        rfl
-    · right
-      equals j₁ =>
-        congr
-        ext
-        simp only [Fin.val_natCast, Nat.mod_eq_of_lt hj]
-        rfl
-  rw [σ_comp_σ (by simpa)]
-  congr <;> {
-    ext
-    simp only [Fin.val_succ, Fin.val_natCast, Nat.mod_eq_of_lt hi,
-      Nat.mod_eq_of_lt (Nat.succ_lt_succ hj), Nat.succ_eq_add_one, add_left_inj ]
-    rfl }
+    σ ⟨i, by omega⟩ ≫ σ ⟨j, hj⟩ = σ ⟨j + 1, by omega⟩ ≫ σ ⟨i, hi⟩ :=
+  σ_comp_σ (n := n) (i := ⟨i, by omega⟩) (j := ⟨j, by omega⟩) (by simpa)
 
 end SimplicialIdentities
 

From 99c76f2a5b69f6d800fe4a773699e86606aa8532 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Thu, 13 Feb 2025 11:33:19 +0100
Subject: [PATCH 08/17] change namespace

---
 .../SimplexCategory/GeneratorsRelations/Basic.lean            | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
index 25d09a47a5640..54b9c60a70120 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
@@ -15,8 +15,6 @@ objects and morphisms in this category.
 This category admits a canonical functor `toSimplexCategory` to the usual simplex category.
 The fact that this functor is an equivalence will be recorded in a separate file.
 -/
-namespace AlgebraicTopology
-
 open CategoryTheory
 
 /-- The objects of the free simplex quiver are the natural numbers. -/
@@ -253,5 +251,3 @@ lemma toSimplexCategory_len {x : SimplexCategoryGenRel} : (toSimplexCategory.obj
   rfl
 
 end SimplexCategoryGenRel
-
-end AlgebraicTopology

From 92ac6ea6174bfa83e11f467a10aacf9bc0549d02 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Tue, 11 Feb 2025 15:27:22 +0100
Subject: [PATCH 09/17] Initial

---
 Mathlib.lean                                  |   1 +
 .../GeneratorsRelations/EpiMono.lean          | 186 ++++++++++++++++++
 2 files changed, 187 insertions(+)
 create mode 100644 Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 44b2e55f1706f..22f4fd9f69019 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1129,6 +1129,7 @@ import Mathlib.AlgebraicTopology.Quasicategory.Nerve
 import Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
 import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
+import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
 import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
 import Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
 import Mathlib.AlgebraicTopology.SimplicialNerve
diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
new file mode 100644
index 0000000000000..46672d15754fc
--- /dev/null
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
@@ -0,0 +1,186 @@
+/-
+Copyright (c) 2025 Robin Carlier. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Carlier
+-/
+import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
+/-! # Epi-mono factorisation in the simplex category presented by generators and relations
+
+This file aims to establish that there is a nice epi-mono factorisation in `SimplexCategoryGenRel`.
+More precisely, we introduce two (inductively-defined) morphism property `P_δ` and `P_σ` that
+single out morphisms that are compositions of `δ i` (resp. `σ i`).
+
+We only define these, and prove various lemmas to help reasoning about them.
+
+## TODOs
+ - Prove that every morphism factors as a `P_σ` followed by a `P_δ`.
+
+-/
+
+namespace AlgebraicTopology.SimplexCategory.SimplexCategoryGenRel
+open CategoryTheory
+
+section EpiMono
+
+/-- `δ i` is a split monomorphism thanks to the simplicial identities. -/
+def SplitMonoδ {n : ℕ} {i : Fin (n + 2)} : SplitMono (δ i) where
+  retraction := by
+    induction i using Fin.lastCases with
+    | last => exact σ n
+    | cast i => exact σ i
+  id := by
+    cases i using Fin.lastCases
+    · simp only [Fin.natCast_eq_last, Fin.lastCases_last]
+      exact δ_comp_σ_succ
+    · simp only [Fin.natCast_eq_last, Fin.lastCases_castSucc]
+      exact δ_comp_σ_self
+
+instance {n : ℕ} {i : Fin (n + 2)} : IsSplitMono (δ i) := .mk' SplitMonoδ
+
+/-- `δ i` is a split epimorphism thanks to the simplicial identities. -/
+def SplitEpiσ {n : ℕ} {i : Fin (n + 1)} : SplitEpi (σ i) where
+  section_ := δ i.castSucc
+  id := δ_comp_σ_self
+
+instance {n : ℕ} {i : Fin (n + 1)} : IsSplitEpi (σ i) := .mk' SplitEpiσ
+
+/-- Auxiliary predicate to express that a morphism is purely a composition of `σ i`s. -/
+inductive P_σ : MorphismProperty SimplexCategoryGenRel
+  | σ {n : ℕ} (i : Fin (n + 1)) : P_σ <| σ i
+  | id {n : ℕ} : P_σ <| 𝟙 (.mk n)
+  | comp {n : ℕ} (i : Fin (n + 1)) {a : SimplexCategoryGenRel} (g : a ⟶ .mk (n + 1))
+    (hg: P_σ g) : P_σ <| g ≫ σ i
+
+/-- A version of `P_σ` where composition is taken on the right instead. It is equivalent to `P_σ`
+(see `P_σ_eq_P_σ'`). -/
+inductive P_σ' : MorphismProperty SimplexCategoryGenRel
+  | σ {n : ℕ} (i : Fin (n + 1)) : P_σ' <| σ i
+  | id {n : ℕ} : P_σ' <| 𝟙 (.mk n)
+  | comp {n : ℕ} (i : Fin (n + 1)) {a : SimplexCategoryGenRel} (g :.mk n ⟶ a)
+    (hg: P_σ' g) : P_σ' <| σ i ≫ g
+
+/-- Auxiliary predicate to express that a morphism is purely a composition of `δ i`s. -/
+inductive P_δ : MorphismProperty SimplexCategoryGenRel
+  | δ {n : ℕ} (i : Fin (n + 2)) : P_δ <| δ i
+  | id {n : ℕ} : P_δ <| 𝟙 (.mk n)
+  | comp {n : ℕ} (i : Fin (n + 2)) {a : SimplexCategoryGenRel} (g : a ⟶ .mk n )
+    (hg: P_δ g) : P_δ <| g ≫ δ i
+
+/-- A version of `P_δ` where composition is taken on the right instead. It is equivalent to `P_δ`
+(see `P_σ_eq_P_δ'`). -/
+inductive P_δ' : MorphismProperty SimplexCategoryGenRel
+  | δ {n : ℕ} (i : Fin (n + 2)) : P_δ' <| δ i
+  | id {n : ℕ} : P_δ' <| 𝟙 (.mk n)
+  | comp {a : SimplexCategoryGenRel} {n : ℕ} (i : Fin (n + 2)) (g : .mk (n + 1) ⟶ a)
+    (hg: P_δ' g) : P_δ' <| δ i ≫ g
+
+lemma P_σ_eqToHom {x y : SimplexCategoryGenRel} (h : x = y) : P_σ <| eqToHom h := by
+  subst h
+  rw [eqToHom_refl]
+  exact P_σ.id
+
+lemma P_δ_eqToHom {x y : SimplexCategoryGenRel} (h : x = y) : P_δ <| eqToHom h := by
+  subst h
+  rw [eqToHom_refl]
+  exact P_δ.id
+
+lemma P_δ_comp {x y z : SimplexCategoryGenRel} (f : x ⟶ y) (g : y ⟶ z) :
+    P_δ f → P_δ g → P_δ (f ≫ g) := by
+  intro hf hg
+  induction hg with
+  | δ i => exact P_δ.comp _ f hf
+  | id => rwa [Category.comp_id]
+  | comp i b _ h => specialize h f hf
+                    rw [← Category.assoc]
+                    exact P_δ.comp i (f ≫ b) h
+
+lemma P_σ_comp {x y z : SimplexCategoryGenRel} (f : x ⟶ y) (g : y ⟶ z) :
+    P_σ f → P_σ g → P_σ (f ≫ g) := by
+  intro hf hg
+  induction hg with
+  | σ i => exact P_σ.comp _ f hf
+  | id => rwa [Category.comp_id]
+  | comp i b _ h => specialize h f hf
+                    rw [← Category.assoc]
+                    exact P_σ.comp i (f ≫ b) h
+
+lemma P_σ'_comp {x y z : SimplexCategoryGenRel} (f : x ⟶ y) (g : y ⟶ z) :
+    P_σ' f → P_σ' g → P_σ' (f ≫ g) := by
+  intro hf hg
+  induction hf with
+  | σ i => exact P_σ'.comp _ g hg
+  | id => rwa [Category.id_comp]
+  | comp i b _ h => specialize h g hg
+                    rw [Category.assoc]
+                    exact P_σ'.comp i (b ≫ g) h
+
+lemma P_δ'_comp {x y z : SimplexCategoryGenRel} (f : x ⟶ y) (g : y ⟶ z) :
+    P_δ' f → P_δ' g → P_δ' (f ≫ g) := by
+  intro hf hg
+  induction hf with
+  | δ i => exact P_δ'.comp _ g hg
+  | id => rwa [Category.id_comp]
+  | comp i b _ h => specialize h g hg
+                    rw [Category.assoc]
+                    exact P_δ'.comp i (b ≫ g) h
+
+/-- The property `P_σ` is equivalent to `P_σ'`. -/
+lemma P_σ_eq_P_σ' : P_σ = P_σ' := by
+  apply le_antisymm <;> intro x y f h
+  · induction h with
+    | σ i => exact P_σ'.σ i
+    | id => exact P_σ'.id
+    | comp i f h h' => exact P_σ'_comp _ _ h' (P_σ'.σ _)
+  · induction h with
+    | σ i => exact P_σ.σ i
+    | id => exact P_σ.id
+    | comp i f h h' => exact P_σ_comp _ _ (P_σ.σ _) h'
+
+/-- The property `P_δ` is equivalent to `P_δ'`. -/
+lemma P_δ_eq_P_δ' : P_δ = P_δ' := by
+  apply le_antisymm <;> intro x y f h
+  · induction h with
+    | δ i => exact P_δ'.δ i
+    | id => exact P_δ'.id
+    | comp i f h h' => exact P_δ'_comp _ _ h' (P_δ'.δ _)
+  · induction h with
+    | δ i => exact P_δ.δ i
+    | id => exact P_δ.id
+    | comp i f h h' => exact P_δ_comp _ _ (P_δ.δ _) h'
+
+/-- All `P_σ` are split epis as composition of such. -/
+lemma isSplitEpi_P_σ {x y : SimplexCategoryGenRel} {e : x ⟶ y} (he : P_σ e) : IsSplitEpi e := by
+  induction he <;> infer_instance
+
+/-- All `P_δ` are split monos as composition of such. -/
+lemma isSplitMono_P_δ {x y : SimplexCategoryGenRel} {m : x ⟶ y} (hm : P_δ m) :
+    IsSplitMono m := by
+  induction hm <;> infer_instance
+
+lemma isSplitEpi_P_σ_toSimplexCategory {x y : SimplexCategoryGenRel} {e : x ⟶ y} (he : P_σ e)
+    : IsSplitEpi <| toSimplexCategory.map e := by
+  constructor
+  constructor
+  apply SplitEpi.map
+  exact isSplitEpi_P_σ he |>.exists_splitEpi.some
+
+lemma isSplitMono_P_δ_toSimplexCategory {x y : SimplexCategoryGenRel} {m : x ⟶ y} (hm : P_δ m)
+    : IsSplitMono <| toSimplexCategory.map m := by
+  constructor
+  constructor
+  apply SplitMono.map
+  exact isSplitMono_P_δ hm |>.exists_splitMono.some
+
+lemma eq_or_len_le_of_P_δ {x y : SimplexCategoryGenRel} {f : x ⟶ y} (h_δ : P_δ f) :
+    (∃ h : x = y, f = eqToHom h) ∨ x.len < y.len := by
+  induction h_δ with
+  | δ i => right; simp
+  | id => left; use rfl; simp
+  | comp i u _ h' =>
+    rcases h' with ⟨e, _⟩ | h'
+    · right; rw [e]; exact Nat.lt_add_one _
+    · right; exact Nat.lt_succ_of_lt h'
+
+end EpiMono
+
+end AlgebraicTopology.SimplexCategory.SimplexCategoryGenRel

From 1e84b0083d9a9f79ba4cdf032d1cb1e806710e12 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Wed, 12 Feb 2025 12:15:29 +0100
Subject: [PATCH 10/17] adapt to changes in #21741

---
 .../SimplexCategory/GeneratorsRelations/EpiMono.lean          | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
index 46672d15754fc..f165113ff3182 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
@@ -17,7 +17,7 @@ We only define these, and prove various lemmas to help reasoning about them.
 
 -/
 
-namespace AlgebraicTopology.SimplexCategory.SimplexCategoryGenRel
+namespace AlgebraicTopology.SimplexCategoryGenRel
 open CategoryTheory
 
 section EpiMono
@@ -183,4 +183,4 @@ lemma eq_or_len_le_of_P_δ {x y : SimplexCategoryGenRel} {f : x ⟶ y} (h_δ : P
 
 end EpiMono
 
-end AlgebraicTopology.SimplexCategory.SimplexCategoryGenRel
+end AlgebraicTopology.SimplexCategoryGenRel

From 7679d6063806ea06bc5992e8fa916eb8ba5f10bc Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Thu, 13 Feb 2025 11:35:39 +0100
Subject: [PATCH 11/17] adapt namespace change

---
 .../SimplexCategory/GeneratorsRelations/EpiMono.lean          | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
index f165113ff3182..c7aa110587804 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
@@ -17,7 +17,7 @@ We only define these, and prove various lemmas to help reasoning about them.
 
 -/
 
-namespace AlgebraicTopology.SimplexCategoryGenRel
+namespace SimplexCategoryGenRel
 open CategoryTheory
 
 section EpiMono
@@ -183,4 +183,4 @@ lemma eq_or_len_le_of_P_δ {x y : SimplexCategoryGenRel} {f : x ⟶ y} (h_δ : P
 
 end EpiMono
 
-end AlgebraicTopology.SimplexCategoryGenRel
+end SimplexCategoryGenRel

From ee6df34d4df8bbd8b169e4c6cfaddb75aae9d5b1 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Wed, 12 Feb 2025 12:17:31 +0100
Subject: [PATCH 12/17] rebase on #21742

---
 .../GeneratorsRelations/EpiMono.lean          | 176 +++++++++++++++++-
 1 file changed, 172 insertions(+), 4 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
index c7aa110587804..2b85851b7a4b0 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
@@ -10,10 +10,8 @@ This file aims to establish that there is a nice epi-mono factorisation in `Simp
 More precisely, we introduce two (inductively-defined) morphism property `P_δ` and `P_σ` that
 single out morphisms that are compositions of `δ i` (resp. `σ i`).
 
-We only define these, and prove various lemmas to help reasoning about them.
-
-## TODOs
- - Prove that every morphism factors as a `P_σ` followed by a `P_δ`.
+The main result of this file is `exists_P_σ_P_δ_factorisation`, which asserts that every
+moprhism as a decomposition of a `P_σ` followed by a `P_δ`.
 
 -/
 
@@ -183,4 +181,174 @@ lemma eq_or_len_le_of_P_δ {x y : SimplexCategoryGenRel} {f : x ⟶ y} (h_δ : P
 
 end EpiMono
 
+section ExistenceOfFactorisations
+
+/-- An auxiliary lemma to show that one can always use the simplicial identities to simplify a term
+in the form `δ ≫ σ` into either an identity, or a term of the form `σ ≫ δ`. This is the crucial
+special case to induct on to get an epi-mono factorisation for all morphisms. -/
+private lemma switch_δ_σ {n : ℕ} (i : Fin (n + 1 + 1)) (i' : Fin (n + 1 + 2)) :
+   δ i' ≫ σ i = 𝟙 _ ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j' := by
+  obtain h'' | h'' | h'' : i'= i.castSucc ∨ i' < i.castSucc ∨ i.castSucc < i' := by
+      simp only [lt_or_lt_iff_ne, ne_eq]
+      tauto
+  · subst h''
+    rw [δ_comp_σ_self]
+    simp
+  · obtain ⟨h₁, h₂⟩ : i' ≠ Fin.last _ ∧ i ≠ 0 := by
+      constructor
+      · exact Fin.ne_last_of_lt h''
+      · rw [Fin.lt_def, Fin.coe_castSucc] at h''
+        apply Fin.ne_of_val_ne
+        exact Nat.not_eq_zero_of_lt h''
+    rw [← i'.castSucc_castPred h₁, ← i.succ_pred h₂]
+    have H : i'.castPred h₁ ≤ (i.pred h₂).castSucc := by
+      simp only [Fin.le_def, Fin.coe_castPred, Fin.coe_castSucc, Fin.coe_pred]
+      rw [Fin.lt_def, Nat.lt_iff_add_one_le] at h''
+      exact Nat.le_sub_one_of_lt h''
+    rw [δ_comp_σ_of_le H]
+    right
+    use i.pred h₂, i'.castPred h₁
+  · by_cases h : i.succ = i'
+    · subst h
+      rw [δ_comp_σ_succ]
+      simp
+    · obtain ⟨h₁, h₂⟩ : i ≠ Fin.last _ ∧ i' ≠ 0 := by
+        constructor
+        · by_cases h' : i' = Fin.last _
+          · simp_all
+          · rw [← Fin.val_eq_val] at h' h
+            apply Fin.ne_of_val_ne
+            rw [Fin.lt_def, Fin.coe_castSucc] at h''
+            rcases i with ⟨i, hi⟩; rcases i' with ⟨i', hi'⟩
+            intro hyp; subst hyp
+            rw [Nat.lt_iff_add_one_le] at h'' hi'
+            simp_all only [add_le_add_iff_right, Fin.val_last, Fin.succ_mk]
+            rw [← one_add_one_eq_two] at hi'
+            exact h (Nat.le_antisymm hi' h'').symm
+        · exact Fin.ne_zero_of_lt h''
+      rw [← i'.succ_pred h₂, ← i.castSucc_castPred h₁]
+      have H : (i.castPred h₁).castSucc < i'.pred h₂ := by
+        rcases (Nat.le_iff_lt_or_eq.mp h'') with h' | h'
+        · simp only [Fin.lt_def, Fin.coe_castSucc, Nat.succ_eq_add_one, Fin.castSucc_castPred,
+            Fin.coe_pred] at *
+          exact Nat.lt_sub_of_add_lt h'
+        · exfalso
+          exact Fin.val_ne_of_ne h h'
+      rw [δ_comp_σ_of_gt H]
+      right
+      use i.castPred h₁, i'.pred h₂
+
+/-- A low-dimensional special case of the previous -/
+private lemma switch_δ_σ₀ (i : Fin 1) (i' : Fin 2) :
+    δ i' ≫ σ i = 𝟙 _ := by
+  rcases i with ⟨i, hi⟩
+  rcases i' with ⟨i', hi'⟩
+  simp at hi hi'
+  rw [Nat.lt_iff_le_pred Nat.zero_lt_two] at hi'
+  simp at hi'
+  subst hi
+  obtain h | h := Nat.le_one_iff_eq_zero_or_eq_one.mp hi'
+  · subst h
+    simp only [Fin.zero_eta, Fin.isValue, ← Fin.castSucc_zero, δ_comp_σ_self]
+  · subst h
+    simp only [Fin.mk_one, Fin.isValue, Fin.zero_eta]
+    rw [← Fin.succ_zero_eq_one, δ_comp_σ_succ]
+
+private lemma factor_δ_σ {n : ℕ} (i : Fin (n + 1)) (i' : Fin (n + 2)) :
+    ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n)
+      (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m := by
+  cases n with
+  | zero =>
+    rw [switch_δ_σ₀]
+    use mk 0, 𝟙 _, 𝟙 _, P_σ.id, P_δ.id
+    simp
+  | succ n =>
+    obtain h | ⟨j, j', h⟩ := switch_δ_σ i i' <;> rw [h]
+    · use mk (n + 1), 𝟙 _, 𝟙 _, P_σ.id, P_δ.id
+      simp
+    · use mk n, σ j, δ j', P_σ.σ _, P_δ.δ _
+
+/-- An auxiliary lemma that shows there exists a factorisation as a P_δ followed by a P_σ for
+morphisms of the form `P_δ ≫ σ`. -/
+private lemma factor_P_δ_σ {n : ℕ} (i : Fin (n + 1)) {x : SimplexCategoryGenRel}
+    (f : x ⟶ mk (n + 1)) (hf : P_δ f) : ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n)
+      (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m := by
+  induction n using Nat.case_strong_induction_on generalizing x with
+  | hz => cases hf with
+    | δ i => exact factor_δ_σ _ _
+    | id  =>
+      rw [Category.id_comp]
+      use mk 0, σ i, 𝟙 _, P_σ.σ _, P_δ.id
+      simp
+    | comp j f hf =>
+      obtain ⟨h', hf'⟩ | hf' := eq_or_len_le_of_P_δ hf
+      · subst h'
+        simp only [eqToHom_refl] at hf'
+        subst hf'
+        rw [Category.id_comp]
+        exact factor_δ_σ _ _
+      · simp at hf'
+  | hi n h_rec =>
+    cases hf with
+    | δ i' => exact factor_δ_σ _ _
+    | @id n =>
+      rw [Category.id_comp]
+      use mk (n + 1), σ i, 𝟙 _, P_σ.σ _, P_δ.id
+      simp
+    | @comp m i' _ g hg =>
+      obtain ⟨h', h''⟩ | h := eq_or_len_le_of_P_δ hg
+      · subst h'
+        rw [eqToHom_refl] at h''; subst h''
+        rw [Category.id_comp]
+        exact factor_δ_σ _ _
+      · obtain h' | ⟨j, j', h'⟩ := switch_δ_σ i i' <;> rw [Category.assoc, h']
+        · rw [Category.comp_id]
+          use x, 𝟙 x, g, P_σ.id, hg
+          simp
+        · rw [mk_len, Nat.lt_add_one_iff] at h
+          obtain ⟨z, e, m₁, he, hm₁, h⟩ := h_rec n (Nat.le_refl _) j g hg
+          rw [reassoc_of% h]
+          use z, e, m₁ ≫ δ j', he, P_δ.comp _ m₁ hm₁
+
+/-- Any morphism in `SimplexCategoryGenRel` can be decomposed as a `P_σ` followed by a `P_δ`. -/
+theorem exists_P_σ_P_δ_factorisation {x y : SimplexCategoryGenRel} (f : x ⟶ y) :
+    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ y)
+        (_ : P_σ e) (_ : P_δ m), f = e ≫ m := by
+  induction f using hom_induction with
+  | @hi n => use (mk n), (𝟙 (mk n)), (𝟙 (mk n)), P_σ.id, P_δ.id; simp
+  | @hc₁ n n' f j h =>
+    obtain ⟨z, e, m, ⟨he, hm, h⟩⟩ := h
+    rw [h, Category.assoc]
+    use z, e, m ≫ δ j, he, P_δ.comp _ _ hm
+  | @hc₂ n n' f j h =>
+    obtain ⟨z, e, m, ⟨he, hm, h⟩⟩ := h
+    rw [h]
+    cases hm with
+    | @δ i j' =>
+      rw [Category.assoc]
+      obtain ⟨z₁, e₁, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_δ_σ j j'
+      rw [h₁]
+      use z₁, e ≫ e₁, m₁, P_σ_comp _ _ he he₁, hm₁
+      simp
+    | @id n =>
+      simp only [Category.comp_id]
+      use mk n', e ≫ σ j, 𝟙 _, P_σ.comp _ _ he, P_δ.id
+      simp
+    | @comp n'' i x' g hg =>
+      rw [Category.assoc, Category.assoc]
+      cases n' with
+      | zero =>
+        rw [switch_δ_σ₀, Category.comp_id]
+        use z, e, g, he, hg
+      | succ n =>
+        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i <;> rw [h']
+        · rw [Category.comp_id]
+          use z, e, g, he, hg
+        · obtain ⟨z₁, e₁, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' g hg
+          rw [reassoc_of% h₁]
+          use z₁, e ≫ e₁, m₁ ≫ δ j'', P_σ_comp _ _ he he₁, P_δ.comp _ _ hm₁
+          simp
+
+end ExistenceOfFactorisations
+
 end SimplexCategoryGenRel

From 3b3e30560a7dc3e5ebedee7d24d400e6a75e45c2 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Tue, 11 Feb 2025 16:54:57 +0100
Subject: [PATCH 13/17] Initial

---
 Mathlib.lean                                  |   1 +
 .../GeneratorsRelations/NormalForms.lean      | 225 ++++++++++++++++++
 2 files changed, 226 insertions(+)
 create mode 100644 Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 22f4fd9f69019..51ea5d3592d8b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1130,6 +1130,7 @@ import Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
 import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
 import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
+import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
 import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
 import Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
 import Mathlib.AlgebraicTopology.SimplicialNerve
diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
new file mode 100644
index 0000000000000..7b09a2b3f4485
--- /dev/null
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -0,0 +1,225 @@
+/-
+Copyright (c) 2025 Robin Carlier. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Carlier
+-/
+import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
+/-! # Normal forms for morphisms in `SimplexCategoryGenRel`.
+
+In this file, we establish that `P_δ` and `P_σ` morphisms in `SimplexCategoryGenRel`
+each admits a normal form.
+
+In both cases, the normal forms are encoded as an integer `m`, and a strictly increasing
+lists of integers `[i₀,…,iₙ]` such that `iₖ ≤ m + k` for all `k`. We define a predicate
+`isAdmissible m : List ℕ → Prop` encoding this property. And provide some lemmas to help
+work with such lists.
+
+Normal forms for `P_σ` morphisms are encoded by `m`-admissible lists, in which case the list
+`[i₀,…,iₙ]` represents the morphism `σ iₙ ≫ ⋯ ≫ σ i₀ : .mk (m + n) ⟶ .mk n`.
+
+Normal forms for `P_δ` morphisms are encoded by `(m + 1)`-admissible lists, in which case the list
+`[i₀,…,iₙ]` represents the morphism `δ i₀ ≫ ⋯ ≫ δ iₙ : .mk n ⟶ .mk (m + n)`.
+
+The results in this file are to be treated as implementation-only, and they only serve as stepping
+stones towards proving that the canonical functor
+`toSimplexCategory : SimplexCategoryGenRel ⥤ SimplexCategory` is an equivalence.
+
+## References:
+* [Kerodon Tag 04FQ](https://kerodon.net/tag/04FQ)
+* [Kerodon Tag 04FT](https://kerodon.net/tag/04FT)
+
+## TODOs:
+ - Show that every `P_σ` admits a unique normal form.
+ - Show that every `P_δ` admits a unique normal form.
+-/
+
+namespace AlgebraicTopology.SimplexCategory.SimplexCategoryGenRel
+
+open CategoryTheory
+
+section AdmissibleLists
+-- Impl. note: We are not bundling admissible lists as a subtype of `List ℕ` so that it remains
+-- easier to perform inductive constructions and proofs on such lists, and we instead bundle
+-- propositions asserting that various List constructions produce admissible lists.
+
+variable (m : ℕ)
+/-- A list of natural numbers [i₀, ⋯, iₙ]) is said to be `m`-admissible (for `m : ℕ`) if
+`i₀ < ⋯ < iₙ` and `iₖ ≤ m + k` for all `k`.
+-/
+def isAdmissible (L : List ℕ) : Prop :=
+  List.Sorted (· < ·) L ∧
+  ∀ k: ℕ, (h : k < L.length) → L[k] ≤ m + k
+
+lemma isAdmissible_nil : isAdmissible m [] := by simp [isAdmissible]
+
+variable {m}
+/-- If `(a :: l)` is `m`-admissible then a is less than all elements of `l` -/
+lemma isAdmissible_head_lt (a : ℕ) (L : List ℕ) (hl : isAdmissible m (a :: L)) :
+    ∀ a' ∈ L, a < a' := by
+  obtain ⟨h₁, h₂⟩ := hl
+  intro i hi
+  exact (List.sorted_cons.mp h₁).left i hi
+
+/-- If `L` is (m+1)-admissible index, and `a` is natural number such that a ≤ m and a < L[0], then
+  `a::L` is `m`-admissible -/
+lemma isAdmissible_cons (L : List ℕ) (hL : isAdmissible (m + 1) L) (a : ℕ) (ha : a ≤ m)
+    (ha' : (_ : 0 < L.length) → a < L[0]) : isAdmissible m (a :: L) := by
+  dsimp [isAdmissible] at hL ⊢
+  cases L with
+  | nil => constructor <;> simp [ha]
+  | cons head tail =>
+    simp only [List.length_cons, lt_add_iff_pos_left, add_pos_iff,
+      Nat.lt_one_iff, pos_of_gt, or_true, List.getElem_cons_zero,
+      forall_const] at ha'
+    have ⟨P₁, P₂⟩ := hL
+    simp only [List.sorted_cons, List.mem_cons, forall_eq_or_imp] at P₁ ⊢
+    constructor <;> repeat constructor
+    · exact ha'
+    · have h_tail := P₁.left
+      rw [← List.forall_getElem] at h_tail ⊢
+      intro i hi
+      exact ha'.trans <| h_tail i hi
+    · exact P₁
+    · intro i hi
+      cases i with
+      | zero => simp [ha]
+      | succ i =>
+          simp only [List.getElem_cons_succ]
+          haveI := P₂ i <| Nat.lt_of_succ_lt_succ hi
+          rwa [← add_comm 1, ← add_assoc]
+
+/-- The tail of an `m`-admissible list is (m+1)-admissible. -/
+lemma isAdmissible_tail (a : ℕ) (l : List ℕ) (h : isAdmissible m (a::l)) :
+      isAdmissible (m + 1) l := by
+  obtain ⟨h₁, h₂⟩ := h
+  refine ⟨(List.sorted_cons.mp h₁).right, ?_⟩
+  intro k hk
+  haveI := h₂ (k + 1) (by simpa)
+  simpa [Nat.add_assoc, Nat.add_comm 1] using this
+
+/-- Since they are strictly sorted, two admissible lists with same elements are equal -/
+lemma isAdmissible_ext (L₁ : List ℕ) (L₂ : List ℕ)
+    (hL₁ : isAdmissible m L₁) (hL₂ : isAdmissible m L₂)
+    (h : ∀ x : ℕ, x ∈ L₁ ↔ x ∈ L₂) : L₁ = L₂ := by
+  obtain ⟨hL₁, hL₁₂⟩ := hL₁
+  obtain ⟨hL₂, hL₂₂⟩ := hL₂
+  clear hL₁₂ hL₂₂
+  induction L₁ generalizing L₂ with
+  | nil =>
+    simp only [List.nil_eq, List.eq_nil_iff_forall_not_mem]
+    intro a ha
+    exact List.not_mem_nil _ ((h a).mpr ha)
+  | cons a L₁ h_rec =>
+    cases L₂ with
+    | nil =>
+      simp only [List.nil_eq, List.eq_nil_iff_forall_not_mem]
+      intro a ha
+      exact List.not_mem_nil _ ((h a).mp ha)
+    | cons b L₂ =>
+      rw [List.cons_eq_cons]
+      simp only [List.mem_cons] at h
+      simp only [List.sorted_cons] at hL₁ hL₂
+      obtain ⟨haL₁, hL₁⟩ := hL₁
+      obtain ⟨hbL₂, hL₂⟩ := hL₂
+      have hab : a = b := by
+        haveI := h b
+        simp only [true_or, iff_true] at this
+        obtain hb | bL₁ := this
+        · exact hb.symm
+        · have ha := h a
+          simp only [true_or, true_iff] at ha
+          obtain hab | aL₂ := ha
+          · exact hab
+          · have f₁ := haL₁ _ bL₁
+            have f₂ := hbL₂ _ aL₂
+            linarith
+      refine ⟨hab, ?_⟩
+      apply h_rec L₂ _ hL₁ hL₂
+      intro x
+      subst hab
+      haveI := h x
+      by_cases hax : x = a
+      · subst hax
+        constructor
+        · intro h₁
+          haveI := haL₁ x h₁
+          linarith
+        · intro h₁
+          haveI := hbL₂ x h₁
+          linarith
+      simpa [hax] using this
+
+/-- An element of a `m`-admissible list, as an element of the appropriate `Fin` -/
+@[simps]
+def isAdmissibleGetElemAsFin (L : List ℕ) (hl : isAdmissible m L) (k : ℕ)
+    (hK : k < L.length) : Fin (m + k + 1) :=
+  Fin.mk L[k] <| Nat.le_iff_lt_add_one.mp (by simp [hl.right])
+
+/-- The head of an `m`-admissible list is a special case of this.  -/
+@[simps!]
+def isAdmissibleHead (a : ℕ) (L : List ℕ) (hl : isAdmissible m (a :: L)) : Fin (m + 1) :=
+  isAdmissibleGetElemAsFin (a :: L) hl 0 (by simp)
+
+/-- The construction `simplicialInsert` describes inserting an element in a list of integer and
+moving it to its "right place" according to the simplicial relations. Somewhat miraculously,
+the algorithm is the same for the first or the fifth simplicial relations, making it "valid"
+when we treat the list as a normal form for a morphism satisfying `P_δ`, or for a morphism
+satisfying `P_σ`!
+
+This is similar in nature to `List.orderedInsert`, but note that we increment one of the element
+every time we perform an exchange, making it a different construction. -/
+def simplicialInsert (a : ℕ) : List ℕ → List ℕ
+  | [] => [a]
+  | b :: l => if a < b then a :: b :: l else b :: simplicialInsert (a + 1) l
+
+/-- `simplicialInsert ` just adds one to the length. -/
+lemma simplicialInsert_length (a : ℕ) (L : List ℕ) :
+    (simplicialInsert a L).length = L.length + 1 := by
+  induction L generalizing a with
+  | nil => rfl
+  | cons head tail h_rec =>
+    simp only [simplicialInsert, List.length_cons]
+    split_ifs with h <;> simp only [List.length_cons, add_left_inj]
+    exact h_rec (a + 1)
+
+/-- `simplicialInsert` preserves admissibility -/
+theorem simplicialInsert_isAdmissible (L : List ℕ) (hL : isAdmissible (m + 1) L) (j : ℕ)
+    (hj : j < m + 1) :
+    isAdmissible m (simplicialInsert j L) := by
+  have ⟨h₁, h₂⟩ := hL
+  induction L generalizing j m with
+  | nil =>
+    simp only [simplicialInsert]
+    constructor
+    · simp
+    · simp [j.le_of_lt_add_one hj]
+  | cons a L h_rec =>
+    simp only [simplicialInsert]
+    split_ifs <;> rename_i ha
+    · exact isAdmissible_cons _ hL _ (j.le_of_lt_add_one hj) (fun _ ↦ ha)
+    · apply isAdmissible_cons
+      · apply h_rec
+        · exact isAdmissible_tail a L hL
+        · simp [hj]
+        · exact (List.sorted_cons.mp h₁).right
+        · intro k hk
+          haveI := h₂ (k + 1) (by simpa)
+          conv_rhs at this => rw [k.add_comm 1, ← Nat.add_assoc]
+          exact this
+      · rw [not_lt] at ha
+        apply ha.trans
+        exact j.le_of_lt_add_one hj
+      · rw [not_lt, Nat.le_iff_lt_add_one] at ha
+        intro u
+        cases L with
+        | nil => simp [simplicialInsert, ha]
+        | cons a' l' =>
+          simp only [simplicialInsert]
+          split_ifs <;> rename_i h'
+          · exact ha
+          · simp only [List.sorted_cons, List.mem_cons, forall_eq_or_imp] at h₁
+            simpa using h₁.left.left
+
+end AdmissibleLists
+
+end AlgebraicTopology.SimplexCategory.SimplexCategoryGenRel

From 4721ff80d67510ae34ce57e9dc924556a11f9eed Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Tue, 11 Feb 2025 22:54:28 +0100
Subject: [PATCH 14/17] lake shake fix

---
 .../SimplexCategory/GeneratorsRelations/NormalForms.lean    | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index 7b09a2b3f4485..4034d8b139910 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Robin Carlier. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robin Carlier
 -/
-import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
+import Mathlib.Tactic.Zify
+import Mathlib.Data.List.Sort
+import Mathlib.Tactic.Linarith.Lemmas
+import Mathlib.Tactic.NormNum.Ineq
+import Mathlib.Tactic.Ring.Basic
 /-! # Normal forms for morphisms in `SimplexCategoryGenRel`.
 
 In this file, we establish that `P_δ` and `P_σ` morphisms in `SimplexCategoryGenRel`

From 89d037bd84dc88c90bdf0ad62f00b10063a4d8a9 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Wed, 12 Feb 2025 12:24:17 +0100
Subject: [PATCH 15/17] fix build

---
 .../SimplexCategory/GeneratorsRelations/NormalForms.lean  | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index 4034d8b139910..5cdd84062696b 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -5,7 +5,7 @@ Authors: Robin Carlier
 -/
 import Mathlib.Tactic.Zify
 import Mathlib.Data.List.Sort
-import Mathlib.Tactic.Linarith.Lemmas
+import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.NormNum.Ineq
 import Mathlib.Tactic.Ring.Basic
 /-! # Normal forms for morphisms in `SimplexCategoryGenRel`.
@@ -37,9 +37,7 @@ stones towards proving that the canonical functor
  - Show that every `P_δ` admits a unique normal form.
 -/
 
-namespace AlgebraicTopology.SimplexCategory.SimplexCategoryGenRel
-
-open CategoryTheory
+namespace AlgebraicTopology.SimplexCategoryGenRel
 
 section AdmissibleLists
 -- Impl. note: We are not bundling admissible lists as a subtype of `List ℕ` so that it remains
@@ -226,4 +224,4 @@ theorem simplicialInsert_isAdmissible (L : List ℕ) (hL : isAdmissible (m + 1)
 
 end AdmissibleLists
 
-end AlgebraicTopology.SimplexCategory.SimplexCategoryGenRel
+end AlgebraicTopology.SimplexCategoryGenRel

From 12bbc184facfa2dcd55443b330115218da20d576 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Thu, 13 Feb 2025 11:39:06 +0100
Subject: [PATCH 16/17] adapt namespace

---
 .../SimplexCategory/GeneratorsRelations/NormalForms.lean      | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index 5cdd84062696b..f1bde41291a0d 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -37,7 +37,7 @@ stones towards proving that the canonical functor
  - Show that every `P_δ` admits a unique normal form.
 -/
 
-namespace AlgebraicTopology.SimplexCategoryGenRel
+namespace SimplexCategoryGenRel
 
 section AdmissibleLists
 -- Impl. note: We are not bundling admissible lists as a subtype of `List ℕ` so that it remains
@@ -224,4 +224,4 @@ theorem simplicialInsert_isAdmissible (L : List ℕ) (hL : isAdmissible (m + 1)
 
 end AdmissibleLists
 
-end AlgebraicTopology.SimplexCategoryGenRel
+end SimplexCategoryGenRel

From 0e442a8564d424094a3d10d7a32e5bf42a3e9b73 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Tue, 11 Feb 2025 17:39:58 +0100
Subject: [PATCH 17/17] Normal forms for compositions of degeneracies

---
 .../GeneratorsRelations/NormalForms.lean      | 320 +++++++++++++++++-
 1 file changed, 314 insertions(+), 6 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index f1bde41291a0d..502754464c391 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -3,11 +3,7 @@ Copyright (c) 2025 Robin Carlier. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robin Carlier
 -/
-import Mathlib.Tactic.Zify
-import Mathlib.Data.List.Sort
-import Mathlib.Tactic.Linarith
-import Mathlib.Tactic.NormNum.Ineq
-import Mathlib.Tactic.Ring.Basic
+import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
 /-! # Normal forms for morphisms in `SimplexCategoryGenRel`.
 
 In this file, we establish that `P_δ` and `P_σ` morphisms in `SimplexCategoryGenRel`
@@ -33,12 +29,13 @@ stones towards proving that the canonical functor
 * [Kerodon Tag 04FT](https://kerodon.net/tag/04FT)
 
 ## TODOs:
- - Show that every `P_σ` admits a unique normal form.
  - Show that every `P_δ` admits a unique normal form.
 -/
 
 namespace SimplexCategoryGenRel
 
+open CategoryTheory
+
 section AdmissibleLists
 -- Impl. note: We are not bundling admissible lists as a subtype of `List ℕ` so that it remains
 -- easier to perform inductive constructions and proofs on such lists, and we instead bundle
@@ -224,4 +221,315 @@ theorem simplicialInsert_isAdmissible (L : List ℕ) (hL : isAdmissible (m + 1)
 
 end AdmissibleLists
 
+section NormalFormsP_σ
+
+-- Impl note.: The definition is a bit akward with the extra parameter `k`, but this
+-- is necessary in order to avoid some type theory hell when proving that `orderedInsert`
+-- behaves as expected...
+
+/-- Given a sequence `L = [ i 0, ..., i b ]`, `standardσ m L` i is the morphism
+`σ (i b) ≫ … ≫ σ (i 0)`. The construction is provided for any list of natural numbers,
+but it is intended to behave well only when the list is admissible. -/
+def standardσ (m : ℕ) (L : List ℕ) (k : ℕ) (hK : L.length = k): mk (m + k) ⟶ mk m :=
+  match L with
+  | .nil => eqToHom (by rw [← hK]; rfl)
+  | .cons a t => eqToHom
+    (by rw [← hK, List.length_cons, Nat.add_comm t.length 1, Nat.add_assoc]) ≫
+      standardσ (m + 1) t t.length rfl ≫ σ a
+
+variable (m : ℕ) (L : List ℕ)
+-- Because we gave a degree of liberty with the parameter `k`, we need this kind of lemma to ease
+-- working with different `k`s
+lemma standardσ_heq (k₁ : ℕ) (hk₁ : L.length = k₁) (k₂ : ℕ) (hk₂ : L.length = k₂) :
+    HEq (standardσ m L k₁ hk₁) (standardσ m L k₂ hk₂) := by
+  subst hk₁
+  subst hk₂
+  simp
+
+/-- `simplicialEvalσ` is a lift to ℕ of `toSimplexCategory.map (standardσ m L _ _)).toOrderHom`,
+but we define it this way to enable for less painful inductive reasoning,
+and we keep the eqToHom shenanigans in the proof that it is indeed such a lift
+(see `simplicialEvalσ_of_isAdmissible`). It is expected to produce the "correct result" only if
+`L` is admissible, but as usual, it is more convenient to have it defined for any list. -/
+def simplicialEvalσ (L : List ℕ) : ℕ → ℕ :=
+  fun j ↦ match L with
+  | [] => j
+  | a :: L => if a < simplicialEvalσ L j then simplicialEvalσ L j - 1 else simplicialEvalσ L j
+
+@[simp]
+private lemma eqToHom_toOrderHom_eq_cast {m n : ℕ}
+    (h : SimplexCategory.mk m = SimplexCategory.mk n) :
+    (eqToHom h).toOrderHom =
+      (Fin.castOrderIso (congrArg (fun x ↦ x.len + 1) h)).toOrderEmbedding.toOrderHom := by
+  ext
+  haveI := congrArg (fun x ↦ x.len + 1) h
+  simp only [SimplexCategory.len_mk, add_left_inj] at this
+  subst this
+  simp
+
+variable {m}
+-- most of the proof is about fighting with `eqToHom`s...
+/- We prove that simplicialEvalσ is indeed the lift we claimed when the list is admissible. -/
+lemma simplicialEvalσ_of_isAdmissible (hL : isAdmissible m L)
+    (k : ℕ) (hk : L.length = k)
+    (j : ℕ) (hj : j < m + k + 1) :
+    ((toSimplexCategory.map (standardσ m L k hk)).toOrderHom ⟨j, hj⟩ : ℕ)
+      = simplicialEvalσ L j := by
+  induction L generalizing m k with
+  | nil =>
+    simp [simplicialEvalσ, standardσ, eqToHom_map]
+  | cons a L h_rec =>
+    subst hk
+    haveI := h_rec (isAdmissible_tail a L hL) L.length rfl <|
+      by simpa [← Nat.add_comm 1 L.length, ← Nat.add_assoc] using hj
+    simp only [toSimplexCategory_obj_mk, SimplexCategory.len_mk, List.length_cons, standardσ,
+      Functor.map_comp, eqToHom_map, toSimplexCategory_map_σ, SimplexCategory.σ,
+      SimplexCategory.mkHom, SimplexCategory.comp_toOrderHom, SimplexCategory.Hom.toOrderHom_mk,
+      eqToHom_toOrderHom_eq_cast, Nat.add_eq, Nat.succ_eq_add_one, OrderHom.comp_coe,
+      OrderHom.coe_mk, OrderEmbedding.toOrderHom_coe, OrderIso.coe_toOrderEmbedding,
+      Function.comp_apply, Fin.predAbove, simplicialEvalσ, ← this]
+    split_ifs with h₁ h₂ h₂
+    · generalize_proofs _ pf
+      rw [Fin.castOrderIso_apply pf ⟨j, hj⟩] at h₁
+      simp only [Fin.cast_mk, Fin.coe_pred] at h₁ ⊢
+      congr
+    · exfalso
+      rw [Fin.lt_def] at h₁
+      simp only [Fin.coe_castSucc, Fin.val_natCast, not_lt] at h₁ h₂
+      haveI := Nat.mod_eq_of_lt (isAdmissibleHead a L hL).prop
+      dsimp [isAdmissibleHead] at this
+      rw [this] at h₁
+      haveI := h₂.trans_lt h₁
+      simp only [Fin.val_fin_lt] at this
+      generalize_proofs _ pf at this
+      conv_rhs at this =>
+        arg 2
+        equals ⟨j, pf⟩ => ext; rfl
+      exact (lt_self_iff_false _).mp this
+    · exfalso
+      rw [Fin.lt_def] at h₁
+      simp only [Fin.coe_castSucc, Fin.val_natCast, not_lt] at h₁ h₂
+      haveI := Nat.mod_eq_of_lt (isAdmissibleHead a L hL).prop
+      dsimp [isAdmissibleHead] at this
+      rw [this] at h₁
+      haveI := h₁.trans_lt h₂
+      simp only [Fin.val_fin_lt] at this
+      generalize_proofs pf1 pf2 pf3 at this
+      conv_rhs at this =>
+        arg 2
+        equals ⟨j, pf3⟩ => ext; rfl
+      exact (lt_self_iff_false _).mp this
+    · generalize_proofs _ pf
+      rw [Fin.castOrderIso_apply pf ⟨j, hj⟩] at h₁
+      simp only [Fin.cast_mk, not_lt, Fin.coe_castPred] at h₁ ⊢
+      congr
+
+lemma simplicialEvalσ_of_lt_mem (j : ℕ) (hj : ∀ k ∈ L, j ≤ k) :
+    simplicialEvalσ L j = j := by
+  induction L with
+  | nil => simp [simplicialEvalσ]
+  | cons a h h_rec =>
+    dsimp only [simplicialEvalσ]
+    split_ifs with h1 <;> {
+      simp only [List.mem_cons, forall_eq_or_imp] at hj
+      obtain ⟨hj₁, hj₂⟩ := hj
+      haveI := h_rec hj₂
+      linarith }
+
+lemma simplicialEvalσ_monotone (L : List ℕ) : Monotone (simplicialEvalσ L) := by
+  intro a b hab
+  induction L generalizing a b with
+  | nil => exact hab
+  | cons head tail h_rec =>
+    dsimp only [simplicialEvalσ]
+    haveI := h_rec hab
+    split_ifs with h h' h' <;> omega
+
+/-- Performing a simplicial insert in a list is (up to some unfortunate `eqToHom`) the same
+as composition on the right by the corresponding degeneracy operator. -/
+lemma standardσ_simplicialInsert (hL : isAdmissible (m + 1) L) (j : ℕ)
+    (hj : j < m + 1) :
+      standardσ m (simplicialInsert j L) (L.length + 1) (simplicialInsert_length _ _) =
+        eqToHom (by rw [Nat.add_assoc, Nat.add_comm 1]) ≫
+          standardσ (m + 1) L L.length rfl ≫
+            σ j := by
+  induction L generalizing m j with
+  | nil => simp [standardσ, simplicialInsert]
+  | cons a L h_rec =>
+    simp only [List.length_cons, eqToHom_refl, simplicialInsert, Category.id_comp]
+    split_ifs <;> rename_i h <;> simp only [standardσ]
+    simp only [eqToHom_trans_assoc, Category.assoc]
+    haveI := h_rec
+      (isAdmissible_tail a L hL)
+      (j + 1)
+      (by simpa)
+    simp only [eqToHom_refl, Category.id_comp] at this
+    slice_rhs 3 5 => equals σ (↑(j + 1)) ≫ σ a =>
+      have ha : a < m + 1 := Nat.lt_of_le_of_lt (not_lt.mp h) hj
+      haveI := σ_comp_σ_nat a j ha hj (not_lt.mp h)
+      generalize_proofs p p' at this
+      -- We have to get rid of the natCasts...
+      have ha₁ : (⟨a, p⟩ : Fin (m + 1 + 1)) = ↑a := by
+        ext
+        simp [Nat.mod_eq_of_lt p]
+      have ha₂ : (⟨a, ha⟩ : Fin (m + 1)) = ↑a := by
+        ext
+        simp [Nat.mod_eq_of_lt ha]
+      have hj₁ : (⟨j + 1, p'⟩ : Fin (m + 1 + 1)) = ↑(j + 1) := by
+        ext
+        simp [Nat.mod_eq_of_lt p']
+      have hj₂ : (⟨j, hj⟩ : Fin (m + 1)) = ↑j := by
+        ext
+        simp [Nat.mod_eq_of_lt hj]
+      rwa [← ha₁, ← ha₂, ← hj₁, ← hj₂]
+    rw [← eqToHom_comp_iff] at this
+    rotate_left
+    · ext; simp [Nat.add_assoc, Nat.add_comm 1, Nat.add_comm 2]
+    · rw [← reassoc_of%this]
+      simp only [eqToHom_trans_assoc]
+      rw [← heq_iff_eq, eqToHom_comp_heq_iff, HEq.comm, eqToHom_comp_heq_iff]
+      apply heq_comp <;> try simp [simplicialInsert_length, heq_iff_eq]
+      apply standardσ_heq
+
+/-- Using the above property, we can prove that every morphism satisfying `P_σ` is equal to some
+`standardσ` for some admissible list of indices. Because morphisms of the form `standardσ` have a
+rather  constrained sources and targets, we have again to splice in some `eqToHom`'s to make
+everything work. -/
+theorem exists_normal_form_P_σ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hf : P_σ f) :
+    ∃ L : List ℕ,
+    ∃ m : ℕ,
+    ∃ b : ℕ,
+    ∃ h₁ : mk m = y,
+    ∃ h₂ : x = mk (m + b),
+    ∃ h: (L.length = b),
+    isAdmissible m L ∧ f = eqToHom h₂ ≫ standardσ m L b h ≫ eqToHom h₁ := by
+  induction hf with
+  | @id n =>
+    use [], n, 0, rfl, rfl, rfl, isAdmissible_nil _
+    simp [standardσ]
+  | @σ m j =>
+    use [j.val], m, 1 , rfl, rfl, rfl
+    constructor <;> simp [isAdmissible, Nat.le_of_lt_add_one j.prop, standardσ]
+  | @comp m j x' g hg h_rec =>
+    obtain ⟨L₁, m₁, b₁, h₁', h₂', h', hL₁, e₁⟩ := h_rec
+    have hm₁ : m₁ = m + 1 := by haveI := h₁'; apply_fun (fun x ↦ x.len) at this; exact this
+    use simplicialInsert j.val L₁, m, b₁ + 1, rfl, ?_, ?_, ?_
+    rotate_right 3
+    · rwa [← Nat.add_comm 1, ← Nat.add_assoc, ← hm₁]
+    · rw [simplicialInsert_length, h']
+    · exact simplicialInsert_isAdmissible _ (by rwa [← hm₁]) _ (j.prop)
+    · subst e₁
+      subst h'
+      rw [standardσ_simplicialInsert]
+      · simp only [Category.assoc, Fin.cast_val_eq_self, eqToHom_refl, Category.comp_id,
+        eqToHom_trans_assoc]
+        subst m₁
+        simp
+      · subst m₁
+        exact hL₁
+      · exact j.prop
+
+section MemIsAdmissible
+
+lemma mem_isAdmissible_of_lt_and_eval_eq_eval_succ (hL : isAdmissible m L)
+    (j : ℕ) (hj₁ : j < m + L.length) (hj₂ : simplicialEvalσ L j = simplicialEvalσ L j.succ) :
+    j ∈ L := by
+  induction L generalizing m with
+  | nil => simp [simplicialEvalσ] at hj₂
+  | cons a L h_rec =>
+    simp only [List.mem_cons]
+    by_cases hja : j = a
+    · left; exact hja
+    · right
+      haveI := (h_rec (isAdmissible_tail a L hL))
+      apply this
+      · simpa [← Nat.add_comm 1 L.length, ← Nat.add_assoc] using hj₁
+      · simp only [simplicialEvalσ, Nat.succ_eq_add_one] at hj₂
+        split_ifs at hj₂ with h₁ h₂ h₂
+        · simp only [Nat.succ_eq_add_one]
+          omega
+        · rw [← hj₂, Nat.eq_self_sub_one]
+          rw [not_lt] at h₂
+          haveI : simplicialEvalσ L j ≤ simplicialEvalσ L (j + 1) :=
+            simplicialEvalσ_monotone L (by simp)
+          linarith
+        · rw [hj₂, Nat.succ_eq_add_one, Eq.comm, Nat.eq_self_sub_one]
+          rw [not_lt] at h₁
+          simp only [isAdmissible, List.sorted_cons, List.length_cons] at hL
+          obtain ⟨⟨hL₁, hL₂⟩, hL₃⟩ := hL
+          obtain h | h | h := Nat.lt_trichotomy j a
+          · haveI : simplicialEvalσ L j ≤ simplicialEvalσ L (j + 1) :=
+              simplicialEvalσ_monotone L (by simp)
+            have ha := simplicialEvalσ_of_lt_mem L a (fun x h ↦ (le_of_lt (hL₁ x h)))
+            have hj₁ := (simplicialEvalσ_monotone L h)
+            linarith
+          · exfalso; exact hja h
+          · haveI := simplicialEvalσ_of_lt_mem L a (fun x h ↦ (le_of_lt (hL₁ x h)))
+            rw [← this] at h₁ h₂
+            have ha₁ := le_antisymm (simplicialEvalσ_monotone L (le_of_lt h)) h₁
+            have ha₂ := simplicialEvalσ_of_lt_mem L (a + 1) (fun x h ↦ (hL₁ x h))
+            rw (occs := .pos [2]) [← this] at ha₂
+            rw [ha₁, hj₂] at ha₂
+            by_cases h': simplicialEvalσ L (j + 1) = 0
+            · exact h'
+            · rw [Nat.sub_one_add_one h'] at ha₂
+              have ha₃ := simplicialEvalσ_monotone L h
+              rw [Nat.succ_eq_add_one] at ha₃
+              linarith
+        · exact hj₂
+
+lemma lt_and_eval_eq_eval_succ_of_mem_isAdmissible (hL : isAdmissible m L) (j : ℕ) (hj : j ∈ L) :
+    j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L j.succ := by
+  induction L generalizing m with
+  | nil => simp [simplicialEvalσ] at hj
+  | cons a L h_rec =>
+    constructor
+    · simp only [isAdmissible, List.sorted_cons] at hL
+      obtain ⟨⟨hL₁, hL₂⟩, hL₃⟩ := hL
+      haveI : ∀ (k : ℕ), (_ : k < (a::L).length) → (a::L)[k] < m + (a::L).length := by
+        intro k hk
+        apply (hL₃ k hk).trans_lt
+        simpa using hk
+      obtain ⟨k, hk, hk'⟩ := List.mem_iff_getElem.mp hj
+      subst hk'
+      exact this k hk
+    · simp only [List.mem_cons] at hj
+      obtain h | h := hj
+      · subst h
+        simp only [simplicialEvalσ, Nat.succ_eq_add_one]
+        simp only [isAdmissible, List.sorted_cons] at hL
+        obtain ⟨⟨hL₁, hL₂⟩, hL₃⟩ := hL
+        rw [simplicialEvalσ_of_lt_mem L j (fun x hx ↦ le_of_lt (hL₁ x hx)),
+          simplicialEvalσ_of_lt_mem L (j + 1) (fun x hx ↦ (hL₁ x hx))]
+        simp
+      · simp only [simplicialEvalσ, Nat.succ_eq_add_one]
+        obtain ⟨h_rec₁, h_rec₂⟩ := h_rec (isAdmissible_tail a L hL) h
+        split_ifs with h₁ h₂ h₂
+        · rw [h_rec₂]
+        · rw [h_rec₂]
+          rw [not_lt] at h₂
+          haveI : simplicialEvalσ L j ≤ simplicialEvalσ L (j + 1) :=
+            simplicialEvalσ_monotone L (by simp)
+          linarith
+        · rw [not_lt] at h₁
+          linarith
+        · rw [h_rec₂]
+
+/-- The key point: we can characterize elements in an admissible list as
+exactly those for which `simplicialEvalσ` takes the same value two times successively. -/
+lemma mem_isAdmissible_iff (hL : isAdmissible m L) (j : ℕ) :
+    j ∈ L ↔
+      j < m + L.length ∧
+      simplicialEvalσ L j =
+        simplicialEvalσ L j.succ := by
+  constructor
+  · intro hj
+    exact lt_and_eval_eq_eval_succ_of_mem_isAdmissible _ hL j hj
+  · rintro ⟨hj₁, hj₂⟩
+    exact mem_isAdmissible_of_lt_and_eval_eq_eval_succ L hL j hj₁ hj₂
+
+end MemIsAdmissible
+
+end NormalFormsP_σ
+
 end SimplexCategoryGenRel