Commit 2024-11-27 18:16 db422a29
View on Github →feat(CategoryTheory): coskeletal simplicial objects (#19492)
A simplicial object X is n-coskeletal if the identity natural transformation X is a right extension of its
restriction along (Truncated.inclusion (n := n)).op recorded by rightExtensionInclusion X n.
Co-Authored-By: Mario Carneiro and Joël Riou