English
For the successor structure, a morphism in the arrow category from F to G induces corresponding morphisms in C that realize the attachment of I-cells along the image of the given morphism.
Русский
Для структуры-последовательности морфизм из F в G порождает соответствующие морфизмы в C, реализующие присоединение I-клеток вдоль образа данного морфизма.
LaTeX
$$$\\text{attachCellsOfSuccStructProp}(I,\\kappa):\\forall F\\to G,\\;\\text{prop}\\;\\varphi\\mapsto \\text{AttachCells}$$$
Lean4
/-- For the successor structure `succStruct I κ` on `Arrow C ⥤ Arrow C`,
the morphism from an object to its successor induces
morphisms in `C` which consists in attaching `I`-cells. -/
noncomputable def attachCellsOfSuccStructProp {F G : Arrow C ⥤ Arrow C} {φ : F ⟶ G} (h : (succStruct I κ).prop φ)
(f : Arrow C) : AttachCells.{w} I.homFamily (φ.app f).left :=
haveI := locallySmall I κ
haveI := isSmall I κ
haveI := hasColimitsOfShape_discrete I κ
haveI := hasPushouts I κ
AttachCells.ofArrowIso (attachCellsιFunctorObjOfSmall _ _)
((Functor.mapArrow ((evaluation _ _).obj f ⋙ Arrow.leftFunc)).mapIso h.arrowIso.symm)
