{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 : forall (u v : forall x : B', C (coeq (g' x))), ooExtendableAlong h (fun x => u x = v x)) : ooExtendableAlong (functor_coeq h k p q) C := fun n => extendable_functor_coeq n (ek n) (fun u v => eh u v n).
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.PathSplit Homotopy.IdentitySystems. Require Import Cubical.DPath Cubical.DPathSquare. Require Import Colimits.Coeq Colimits.MappingCylinder.