mathlib3

d79c3671 - feat(algebraic_topology): extra degeneracy of augmented simplicial objects (#16411)

feat(algebraic_topology): extra degeneracy of augmented simplicial objects (#16411) This PR introduces the notion of extra degeneracy of augmented simplicial objects. In homotopy theory, this is a condition that is used to show that the connected components of simplicial sets are contractible. This notion is formalized for augmented simplicial objects in any category and it is shown that the standard `n`-simplex has an extra degeneracy. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>