{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 1 k (C o coeq)) (eh : forall (u v : forall x : B', C (coeq (g' x))), ExtendableAlong 1 h (fun x => u x = v x)) (s : forall x, C (functor_coeq h k p q x)) : ExtensionAlong (functor_coeq h k p q) C s. Proof. set (C' := C o pr_cylcoeq p q). set (s' x := pr_cyl_cylcoeq p q x # s x). assert (e : ExtensionAlong (cyl_cylcoeq p q) C' s'). 2:{ pose (ex := fst (extendable_equiv 1 C (pr_cylcoeq p q)) e.1). exists (ex.1); intros x. apply (equiv_inj (transport C (pr_cyl_cylcoeq p q x))). exact (apD _ (pr_cyl_cylcoeq p q x) @ ex.2 _ @ e.2 x). } pose (ea1 := fun u => (fst (cyl_extendable' 1 _ _ ek) u).1). assert (eb'' : forall u v, ExtendableAlong 1 cyl (fun x:Cyl h => DPath C' (cglue x) (u x) (v x))). { intros u v. rapply extendable_postcompose'. 2:{ rapply (cancelL_extendable 1 _ cyl pr_cyl). - rapply extendable_equiv. - exact (eh (fun x => cglue x # u (cyr x)) (v o cyr)). } intros x; subst C'. refine ((dp_compose (pr_cylcoeq p q) C _)^-1 oE _). symmetry; srapply equiv_ds_fill_lr. 3:rapply ap_pr_cylcoeq_cglue. all:srapply (transport (fun r => DPath C r _ _)). 3:exact (dp_inverse (dp_compose _ C _ (apD u (eissect pr_cyl x) : DPath _ _ _ _))). 4:exact (dp_inverse (dp_compose _ C _ (apD v (eissect pr_cyl x) : DPath _ _ _ _))). 1:change (fun y => pr_cylcoeq p q (coeq (functor_cyl p y))) with (fun y => coeq (f := f') (g := g') (pr_cyl (functor_cyl p y))). 2:change (fun y => pr_cylcoeq p q (coeq (functor_cyl q y))) with (fun y => coeq (f := f') (g := g') (pr_cyl (functor_cyl q y))). all:refine ((ap_V _ (eissect pr_cyl x))^ @ _). all: exact (ap_compose (fun x => pr_cyl (functor_cyl _ x)) coeq _). } pose (eb1 := fun u v w => (fst (cyl_extendable _ _ _ (eb'' u v)) w).1). srefine (_;_); srapply Coeq_ind. + exact (ea1 (s' o coeq)). + apply eb1; intros b. rapply (dp_compose' _ _ (ap_cyl_cylcoeq_cglue p q b)). exact (apD s' (cglue b)). + intros a; reflexivity. + intros b. apply ds_dp. rapply ds_G1. refine (dp_apD_compose' _ _ (ap_cyl_cylcoeq_cglue p q b) _ @ _). apply moveR_equiv_V. nrapply Coeq_ind_beta_cglue. 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.