extendable_functor_coeq' (n : nat) {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 : ExtendableAlong n k (C o coeq)) (eh : ExtendableAlong n.+1 h (C o coeq o g')) : ExtendableAlong n (functor_coeq h k p q) C. Proof. apply extendable_functor_coeq. 1:assumption. exact (snd eh). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.PathSplit Homotopy.IdentitySystems. Require Import Cubical.DPath Cubical.DPathSquare. Require Import Colimits.Coeq Colimits.MappingCylinder.