Commit 2023-12-27 13:14 d5dea345
View on Github →feat(CategoryTheory): another constructor for ComposableArrows (#8541)
In this PR, given objects obj : Fin (n + 1) → C and mapSucc i : obj i.castSucc ⟶ obj i.succ (i.e. a sequence of morphisms), we construct mkOfObjOfMapSucc obj mapSucc : ComposableArrows C n. On objects, this constructor has good definitional properties.