fact: Definition ooextendable_functor_coeq' {B A f g B' A' f' g'} {h : B -> B'} {k : A -> A'} {p : k o f == f' o h} {q : k o g == g' o h} {C : Coeq f' g' -> Type} (ek : ooExtendableAlong k (C o coeq)) (eh : ooExtendableAlong h (C o coeq o g')) : ooExtendableAlong (functor_coeq h k p q) C := fun n => extendable_functor_coeq' n (ek n) (eh n.+1).
imports: HoTT.Basics HoTT.Types Equiv.PathSplit PathAny Cubical.DPath Cubical.DPathSquare Colimits.Coeq Colimits.MappingCylinder