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