def SimplexCategory.δ_zero_mkOfLe {n : ℕ} (i j : Fin (n + 1)) (h : i ≤ j) : CategoryTheory.CategoryStruct.comp (δ 0) (mkOfLe i j h) = { len := 0 }.const { len := n } j

Equations

• ⋯ = ⋯

def SimplexCategory.δ_one_mkOfLe {n : ℕ} (i j : Fin (n + 1)) (h : i ≤ j) : CategoryTheory.CategoryStruct.comp (δ 1) (mkOfLe i j h) = { len := 0 }.const { len := n } i

Equations

• ⋯ = ⋯