(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 : forall (u v : forall x : B', C (coeq (g' x))), ExtendableAlong n h (fun x => u x = v x)) : ExtendableAlong n (functor_coeq h k p q) C. Proof. revert C ek eh; simple_induction n n IH; intros C ek eh; [ exact tt | split ]. - apply extension_functor_coeq. + exact (fst ek , fun _ _ => tt). + exact (fun u v => (fst (eh u v) , fun _ _ => tt)). - intros u v; apply IH. + exact (snd ek (u o coeq) (v o coeq)). + exact (snd (eh (u o coeq o g') (v o coeq o g'))). 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.