Commit 2025-12-12 09:27 8a37e1dc
View on Github →feat(AlgebraicTopology): relative morphisms of simplicial sets (#32345)
Given two simplicial sets X and Y, and subcomplexes A of X, and B of Y, we introduce a type RelativeMorphism A B φ of morphisms X ⟶ Y which induce a given morphism of simplicial sets A ⟶ B. We define homotopies between these relative morphisms and introduce the quotient type of homotopy classes.
(Homotopy groups of Kan complexes will be defined as a particular case of this construction.)
From https://github.com/joelriou/topcat-model-category