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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯