Built with Alectryon. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
(** * Extensions and extensible maps *)

Require Import HoTT.Basics HoTT.Types.
Require Import Equiv.PathSplit Homotopy.IdentitySystems.
Require Import Cubical.DPath Cubical.DPathSquare.
Require Import Colimits.Coeq Colimits.MappingCylinder.

Local Open Scope nat_scope.
Local Open Scope path_scope.

(** Given [C : B -> Type] and [f : A -> B], an extension of [g : forall a, C (f a)] along [f] is a section [h : forall b, C b] such that [h (f a) = g a] for all [a:A].  This is equivalently the existence of fillers for commutative squares, restricted to the case where the bottom of the square is the identity; type-theoretically, this approach is sometimes more convenient.  In this file we study the type of such extensions.  One of its crucial properties is that a path between extensions is equivalently an extension in a fibration of paths.

This turns out to be useful for several reasons.  For instance, by iterating it, we can to formulate universal properties without needing [Funext].  It also gives us a way to "quantify" a universal property by the connectedness of the type of extensions. *)

Section Extensions.

  (* TODO: consider naming for [ExtensionAlong] and subsequent lemmas.  As a name for the type itself, [Extension] or [ExtensionAlong] seems great; but resultant lemma names such as [path_extension] (following existing naming conventions) are rather misleading. *)

  (** This elimination rule (and others) can be seen as saying that, given a fibration over the codomain and a section of it over the domain, there is some *extension* of this to a section over the whole codomain.  It can also be considered as an equivalent form of an [hfiber] of precomposition-with-[f] that replaces paths by pointwise paths, thereby avoiding [Funext]. *)
  Definition ExtensionAlong@{a b p m} {A : Type@{a}} {B : Type@{b}} (f : A -> B)
             (P : B -> Type@{p}) (d : forall x:A, P (f x))
    := (* { s : forall y:B, P y & forall x:A, s (f x) = d x }. *)
       sig@{m m} (fun (s : forall y:B, P y) => forall x:A, s (f x) = d x).
   (** [ExtensionAlong] takes 4 universe parameters:
      - the size of A
      - the size of B
      - the size of P
      - >= max(A,B,P)
   *)

  (** It's occasionally useful to be able to modify those universes.  For each of the universes [a], [b], [p], we give an initial one, a final one, and a "minimum" one smaller than both and where the type actually lives. *)
  
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)

ExtensionAlong f P d -> ExtensionAlong f P d
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)

ExtensionAlong f P d -> ExtensionAlong f P d
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext: ExtensionAlong f P d

ExtensionAlong f P d
(** If we just give [ext], it will collapse the universes. (Anyone stepping through this proof should do [Set Printing Universes] and look at the universes to see that they're different in [ext] and in the goal.) So we decompose [ext] into two components and give them separately. *)
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext: ExtensionAlong f P d
e1:= ext.1: forall y : B, P y
e2: (fun s : forall y : B, P y => forall x : A, s (f x) = d x) e1

ExtensionAlong f P d
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext: ExtensionAlong f P d
e1:= ext.1: forall y : B, P y
e2: forall x : A, e1 (f x) = d x

ExtensionAlong f P d
exact (e1;e2). Defined. (** We called it [lift_extensionalong], but in fact it doesn't require the new universes to be bigger than the old ones, only that they both satisfy the max condition. *)
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext, ext': ExtensionAlong f P d

ExtensionAlong f (fun y : B => ext.1 y = ext'.1 y) (fun x : A => ext.2 x @ (ext'.2 x)^) <~> ext = ext'
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext, ext': ExtensionAlong f P d

ExtensionAlong f (fun y : B => ext.1 y = ext'.1 y) (fun x : A => ext.2 x @ (ext'.2 x)^) <~> ext = ext'
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext: ExtensionAlong f P d

forall ext' : ExtensionAlong f P d, ExtensionAlong f (fun y : B => ext.1 y = ext'.1 y) (fun x : A => ext.2 x @ (ext'.2 x)^) <~> ext = ext'
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext: ExtensionAlong f P d

(fun b : ExtensionAlong f P d => ExtensionAlong f (fun y : B => ext.1 y = b.1 y) (fun x : A => ext.2 x @ (b.2 x)^)) ext
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext: ExtensionAlong f P d
Contr {y : ExtensionAlong f P d & (fun b : ExtensionAlong f P d => ExtensionAlong f (fun y0 : B => ext.1 y0 = b.1 y0) (fun x : A => ext.2 x @ (b.2 x)^)) y}
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext: ExtensionAlong f P d

(fun b : ExtensionAlong f P d => ExtensionAlong f (fun y : B => ext.1 y = b.1 y) (fun x : A => ext.2 x @ (b.2 x)^)) ext
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext: ExtensionAlong f P d

{s : forall y : B, ext.1 y = ext.1 y & forall x : A, s (f x) = ext.2 x @ (ext.2 x)^}
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext: ExtensionAlong f P d

forall x : A, 1 = ext.2 x @ (ext.2 x)^
intros x; symmetry; apply concat_pV.
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
ext: ExtensionAlong f P d

Contr {y : ExtensionAlong f P d & (fun b : ExtensionAlong f P d => ExtensionAlong f (fun y0 : B => ext.1 y0 = b.1 y0) (fun x : A => ext.2 x @ (b.2 x)^)) y}
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
g: forall y : B, P y
gd: forall x : A, g (f x) = d x

Contr {y : {s : forall y : B, P y & forall x : A, s (f x) = d x} & {s : forall y0 : B, g y0 = y.1 y0 & forall x : A, s (f x) = gd x @ (y.2 x)^}}
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
g: forall y : B, P y
gd: forall x : A, g (f x) = d x

Contr {y : forall x : A, g (f x) = d x & forall x : A, 1 = gd x @ (y x)^}
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
g: forall y : B, P y
gd: forall x : A, g (f x) = d x

{p : (fun x : A => g (f x)) == d & gd == p} <~> {y : forall x : A, g (f x) = d x & forall x : A, 1 = gd x @ (y x)^}
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
g: forall y : B, P y
gd: forall x : A, g (f x) = d x

{p : (fun x : A => g (f x)) == d & gd == p} <~> {y : forall x : A, g (f x) = d x & forall x : A, 1 = gd x @ (y x)^}
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x : A, P (f x)
g: forall y : B, P y
gd: forall x : A, g (f x) = d x
p: (fun x : A => g (f x)) == d

gd == p <~> (forall x : A, 1 = gd x @ (p x)^)
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x0 : A, P (f x0)
g: forall y : B, P y
gd: forall x0 : A, g (f x0) = d x0
p: (fun x0 : A => g (f x0)) == d
x: A

gd x = p x <~> 1 = gd x @ (p x)^
H: Funext
A, B: Type
f: A -> B
P: B -> Type
d: forall x0 : A, P (f x0)
g: forall y : B, P y
gd: forall x0 : A, g (f x0) = d x0
p: (fun x0 : A => g (f x0)) == d
x: A

p x = gd x <~> 1 = gd x @ (p x)^
symmetry; apply equiv_moveR_1M. Defined. Definition path_extension `{Funext} {A B : Type} {f : A -> B} {P : B -> Type} {d : forall x:A, P (f x)} (ext ext' : ExtensionAlong f P d) : (ExtensionAlong f (fun y => pr1 ext y = pr1 ext' y) (fun x => pr2 ext x @ (pr2 ext' x)^)) -> ext = ext' := equiv_path_extension ext ext'. #[export] Instance isequiv_path_extension `{Funext} {A B : Type} {f : A -> B} {P : B -> Type} {d : forall x:A, P (f x)} (ext ext' : ExtensionAlong f P d) : IsEquiv (path_extension ext ext') | 0 := equiv_isequiv _. (** Here is the iterated version. *) Fixpoint ExtendableAlong@{i j k l} (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with | 0 => Unit | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l} f C g) * forall (h k : forall b, C b), ExtendableAlong n f (fun b => h b = k b) end. (** [ExtendableAlong] takes 4 universe parameters: - size of A - size of B - size of C - size of result (>= A,B,C) *) Global Arguments ExtendableAlong n%_nat_scope {A B}%_type_scope (f C)%_function_scope. (** We can modify the universes, as with [ExtensionAlong]. *)
n: nat
A, B: Type
f: A -> B
P: B -> Type

ExtendableAlong n f P -> ExtendableAlong n f P
n: nat
A, B: Type
f: A -> B
P: B -> Type

ExtendableAlong n f P -> ExtendableAlong n f P
A, B: Type
f: A -> B
P: B -> Type

ExtendableAlong 0 f P -> ExtendableAlong 0 f P
A, B: Type
f: A -> B
n: nat
IH: forall P0 : B -> Type, ExtendableAlong n f P0 -> ExtendableAlong n f P0
P: B -> Type
ExtendableAlong n.+1 f P -> ExtendableAlong n.+1 f P
A, B: Type
f: A -> B
P: B -> Type

ExtendableAlong 0 f P -> ExtendableAlong 0 f P
intros _; exact tt.
A, B: Type
f: A -> B
n: nat
IH: forall P0 : B -> Type, ExtendableAlong n f P0 -> ExtendableAlong n f P0
P: B -> Type

ExtendableAlong n.+1 f P -> ExtendableAlong n.+1 f P
A, B: Type
f: A -> B
n: nat
IH: forall P0 : B -> Type, ExtendableAlong n f P0 -> ExtendableAlong n f P0
P: B -> Type
ext: ExtendableAlong n.+1 f P

forall g : forall a : A, P (f a), ExtensionAlong f P g
A, B: Type
f: A -> B
n: nat
IH: forall P0 : B -> Type, ExtendableAlong n f P0 -> ExtendableAlong n f P0
P: B -> Type
ext: ExtendableAlong n.+1 f P
forall h k : forall b : B, P b, ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IH: forall P0 : B -> Type, ExtendableAlong n f P0 -> ExtendableAlong n f P0
P: B -> Type
ext: ExtendableAlong n.+1 f P

forall g : forall a : A, P (f a), ExtensionAlong f P g
intros g; exact (lift_extensionalong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} _ _ _ (fst ext g)).
A, B: Type
f: A -> B
n: nat
IH: forall P0 : B -> Type, ExtendableAlong n f P0 -> ExtendableAlong n f P0
P: B -> Type
ext: ExtendableAlong n.+1 f P

forall h k : forall b : B, P b, ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IH: forall P0 : B -> Type, ExtendableAlong n f P0 -> ExtendableAlong n f P0
P: B -> Type
ext: ExtendableAlong n.+1 f P
h, k: forall b : B, P b

ExtendableAlong n f (fun b : B => h b = k b)
(** Unless we give the universe explicitly here, [kmin] gets collapsed to [k1]. *)
A, B: Type
f: A -> B
n: nat
IH: forall P0 : B -> Type, ExtendableAlong n f P0 -> ExtendableAlong n f P0
P: B -> Type
ext: ExtendableAlong n.+1 f P
h, k: forall b : B, P b
P':= (fun b : B => h b = k b) : B -> Type: B -> Type

ExtendableAlong n f (fun b : B => h b = k b)
exact (IH P' (snd ext h k)). Defined.
H: Funext
n: nat
A, B: Type
C: B -> Type
f: A -> B

ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C b => g oD f)
H: Funext
n: nat
A, B: Type
C: B -> Type
f: A -> B

ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C b => g oD f)
H: Funext
A, B: Type
f: A -> B
C: B -> Type

ExtendableAlong 0 f C <~> PathSplit 0 (fun g : forall b : B, C b => g oD f)
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g : forall b : B, C0 b => g oD f)
C: B -> Type
ExtendableAlong n.+1 f C <~> PathSplit n.+1 (fun g : forall b : B, C b => g oD f)
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g : forall b : B, C0 b => g oD f)
C: B -> Type

ExtendableAlong n.+1 f C <~> PathSplit n.+1 (fun g : forall b : B, C b => g oD f)
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g : forall b : B, C0 b => g oD f)
C: B -> Type

(forall g : forall a : A, C (f a), ExtensionAlong f C g) <~> (forall a : forall x : A, C (f x), hfiber (fun g : forall b : B, C b => g oD f) a)
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g : forall b : B, C0 b => g oD f)
C: B -> Type
(forall h k : forall b : B, C b, (fix ExtendableAlong (n0 : nat) (A0 B0 : Type) (f0 : A0 -> B0) (C0 : B0 -> Type) {struct n0} : Type := match n0 with | 0 => Unit | n1.+1 => (forall g : forall a : A0, C0 (f0 a), ExtensionAlong f0 C0 g) * (forall h0 k0 : forall b : B0, C0 b, ExtendableAlong n1 A0 B0 f0 (fun b : B0 => h0 b = k0 b)) end) n A B f (fun b : B => h b = k b)) <~> (forall x y : forall b : B, C b, (fix PathSplit (n0 : nat) (A0 B0 : Type) (f0 : A0 -> B0) {struct n0} : Type := match n0 with | 0 => Unit | n1.+1 => (forall a : B0, hfiber f0 a) * (forall x0 y0 : A0, PathSplit n1 (x0 = y0) (f0 x0 = f0 y0) (ap f0)) end) n (x = y) (x oD f = y oD f) (ap (fun g : forall b : B, C b => g oD f)))
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g : forall b : B, C0 b => g oD f)
C: B -> Type

(forall g : forall a : A, C (f a), ExtensionAlong f C g) <~> (forall a : forall x : A, C (f x), hfiber (fun g : forall b : B, C b => g oD f) a)
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g0 : forall b : B, C0 b => g0 oD f)
C: B -> Type
g: forall a : A, C (f a)

ExtensionAlong f C g <~> hfiber (fun g0 : forall b : B, C b => g0 oD f) g
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g0 : forall b : B, C0 b => g0 oD f)
C: B -> Type
g: forall a : A, C (f a)
rec: forall y : B, C y

(forall x : A, rec (f x) = g x) <~> 1%equiv rec oD f = g
apply equiv_path_forall.
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g : forall b : B, C0 b => g oD f)
C: B -> Type

(forall h k : forall b : B, C b, (fix ExtendableAlong (n0 : nat) (A0 B0 : Type) (f0 : A0 -> B0) (C0 : B0 -> Type) {struct n0} : Type := match n0 with | 0 => Unit | n1.+1 => (forall g : forall a : A0, C0 (f0 a), ExtensionAlong f0 C0 g) * (forall h0 k0 : forall b : B0, C0 b, ExtendableAlong n1 A0 B0 f0 (fun b : B0 => h0 b = k0 b)) end) n A B f (fun b : B => h b = k b)) <~> (forall x y : forall b : B, C b, (fix PathSplit (n0 : nat) (A0 B0 : Type) (f0 : A0 -> B0) {struct n0} : Type := match n0 with | 0 => Unit | n1.+1 => (forall a : B0, hfiber f0 a) * (forall x0 y0 : A0, PathSplit n1 (x0 = y0) (f0 x0 = f0 y0) (ap f0)) end) n (x = y) (x oD f = y oD f) (ap (fun g : forall b : B, C b => g oD f)))
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g : forall b : B, C0 b => g oD f)
C: B -> Type
h: forall b : B, C b

(forall k : forall b : B, C b, (fix ExtendableAlong (n0 : nat) (A0 B0 : Type) (f0 : A0 -> B0) (C0 : B0 -> Type) {struct n0} : Type := match n0 with | 0 => Unit | n1.+1 => (forall g : forall a : A0, C0 (f0 a), ExtensionAlong f0 C0 g) * (forall h0 k0 : forall b : B0, C0 b, ExtendableAlong n1 A0 B0 f0 (fun b : B0 => h0 b = k0 b)) end) n A B f (fun b : B => 1%equiv h b = k b)) <~> (forall y : forall b : B, C b, (fix PathSplit (n0 : nat) (A0 B0 : Type) (f0 : A0 -> B0) {struct n0} : Type := match n0 with | 0 => Unit | n1.+1 => (forall a : B0, hfiber f0 a) * (forall x y0 : A0, PathSplit n1 (x = y0) (f0 x = f0 y0) (ap f0)) end) n (h = y) (h oD f = y oD f) (ap (fun g : forall b : B, C b => g oD f)))
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g : forall b : B, C0 b => g oD f)
C: B -> Type
h, k: forall b : B, C b

(fix ExtendableAlong (n0 : nat) (A0 B0 : Type) (f0 : A0 -> B0) (C0 : B0 -> Type) {struct n0} : Type := match n0 with | 0 => Unit | n1.+1 => (forall g : forall a : A0, C0 (f0 a), ExtensionAlong f0 C0 g) * (forall h0 k0 : forall b : B0, C0 b, ExtendableAlong n1 A0 B0 f0 (fun b : B0 => h0 b = k0 b)) end) n A B f (fun b : B => h b = k b) <~> (fix PathSplit (n0 : nat) (A0 B0 : Type) (f0 : A0 -> B0) {struct n0} : Type := match n0 with | 0 => Unit | n1.+1 => (forall a : B0, hfiber f0 a) * (forall x y : A0, PathSplit n1 (x = y) (f0 x = f0 y) (ap f0)) end) n (h = k) (h oD f = k oD f) (ap (fun g : forall b : B, C b => g oD f))
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g : forall b : B, C0 b => g oD f)
C: B -> Type
h, k: forall b : B, C b

PathSplit n (fun g : forall b : B, h b = k b => g oD f) <~> (fix PathSplit (n0 : nat) (A0 B0 : Type) (f0 : A0 -> B0) {struct n0} : Type := match n0 with | 0 => Unit | n1.+1 => (forall a : B0, hfiber f0 a) * (forall x y : A0, PathSplit n1 (x = y) (f0 x = f0 y) (ap f0)) end) n (h = k) (h oD f = k oD f) (ap (fun g : forall b : B, C b => g oD f))
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g : forall b : B, C0 b => g oD f)
C: B -> Type
h, k: forall b : B, C b

(fix PathSplit (n0 : nat) (A0 B0 : Type) (f0 : A0 -> B0) {struct n0} : Type := match n0 with | 0 => Unit | n1.+1 => (forall a : B0, hfiber f0 a) * (forall x y : A0, PathSplit n1 (x = y) (f0 x = f0 y) (ap f0)) end) n (h = k) (h oD f = k oD f) (ap (fun g : forall b : B, C b => g oD f)) <~> PathSplit n (fun g : forall b : B, h b = k b => g oD f)
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 <~> PathSplit n (fun g : forall b : B, C0 b => g oD f)
C: B -> Type
h, k: forall b : B, C b

(fun x : h = k => equiv_apD10 C h k x oD f) == (fun x : h = k => equiv_apD10 (fun x0 : A => C (f x0)) (h oD f) (k oD f) (ap (fun g : forall b : B, C b => g oD f) x))
intros []; reflexivity. Defined. Definition isequiv_extendable `{Funext} (n : nat) {A B : Type} {C : B -> Type} {f : A -> B} : ExtendableAlong n.+2 f C -> IsEquiv (fun g => g oD f) := isequiv_pathsplit n o (equiv_extendable_pathsplit n.+2 C f).
H: Funext
n: nat
A, B: Type
C: B -> Type
f: A -> B

IsHProp (ExtendableAlong n.+2 f C)
H: Funext
n: nat
A, B: Type
C: B -> Type
f: A -> B

IsHProp (ExtendableAlong n.+2 f C)
exact (istrunc_equiv_istrunc _ (equiv_extendable_pathsplit n.+2 C f)^-1). Defined.
H: Funext
n: nat
A, B: Type
C: B -> Type
f: A -> B

ExtendableAlong n.+2 f C <~> IsEquiv (fun g : forall b : B, C b => g oD f)
H: Funext
n: nat
A, B: Type
C: B -> Type
f: A -> B

ExtendableAlong n.+2 f C <~> IsEquiv (fun g : forall b : B, C b => g oD f)
H: Funext
n: nat
A, B: Type
C: B -> Type
f: A -> B

ExtendableAlong n.+2 f C <~> ?Goal
H: Funext
n: nat
A, B: Type
C: B -> Type
f: A -> B
?Goal <~> IsEquiv (fun g : forall b : B, C b => g oD f)
H: Funext
n: nat
A, B: Type
C: B -> Type
f: A -> B

ExtendableAlong n.+2 f C <~> ?Goal
apply equiv_extendable_pathsplit.
H: Funext
n: nat
A, B: Type
C: B -> Type
f: A -> B

PathSplit n.+2 (fun g : forall b : B, C b => g oD f) <~> IsEquiv (fun g : forall b : B, C b => g oD f)
apply equiv_pathsplit_isequiv. Defined. (* Without [Funext], we can prove a small part of the above equivalence. We suspect that the rest requires [Funext]. *)
A, B: Type
f: A -> B
C: B -> Type

IsEquiv (fun g : forall b : B, C b => g oD f) -> forall g : forall x : A, C (f x), ExtensionAlong f C g
A, B: Type
f: A -> B
C: B -> Type

IsEquiv (fun g : forall b : B, C b => g oD f) -> forall g : forall x : A, C (f x), ExtensionAlong f C g
A, B: Type
f: A -> B
C: B -> Type
E: IsEquiv (fun g0 : forall b : B, C b => g0 oD f)
g: forall x : A, C (f x)

ExtensionAlong f C g
A, B: Type
f: A -> B
C: B -> Type
E: IsEquiv (fun g0 : forall b : B, C b => g0 oD f)
g: forall x : A, C (f x)
e:= {| equiv_fun := fun g0 : forall b : B, C b => g0 oD f; equiv_isequiv := E |}: (forall b : B, C b) <~> (forall x : A, C (f x))

ExtensionAlong f C g
A, B: Type
f: A -> B
C: B -> Type
E: IsEquiv (fun g0 : forall b : B, C b => g0 oD f)
g: forall x : A, C (f x)
e:= {| equiv_fun := fun g0 : forall b : B, C b => g0 oD f; equiv_isequiv := E |}: (forall b : B, C b) <~> (forall x : A, C (f x))

forall x : A, (fun g0 : forall b : B, C b => g0 oD f)^-1 g (f x) = g x
A, B: Type
f: A -> B
C: B -> Type
E: IsEquiv (fun g0 : forall b : B, C b => g0 oD f)
g: forall x : A, C (f x)
e:= {| equiv_fun := fun g0 : forall b : B, C b => g0 oD f; equiv_isequiv := E |}: (forall b : B, C b) <~> (forall x : A, C (f x))

(fun x : A => (fun g0 : forall b : B, C b => g0 oD f)^-1 g (f x)) = g
exact (eisretr e g). Defined. (** Postcomposition with a known equivalence. Note that this does not require funext to define, although showing that it is an equivalence would require funext. *)
n: nat
A, B: Type
C, D: B -> Type
f: A -> B
g: forall b : B, C b <~> D b

ExtendableAlong n f C -> ExtendableAlong n f D
n: nat
A, B: Type
C, D: B -> Type
f: A -> B
g: forall b : B, C b <~> D b

ExtendableAlong n f C -> ExtendableAlong n f D
n: nat
A, B: Type
f: A -> B

forall D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
A, B: Type
f: A -> B
C, D: B -> Type
g: forall b : B, D b <~> C b

Unit -> Unit
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b : B, C0 b <~> D0 b) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b : B, D b <~> C b
(forall g0 : forall a : A, D (f a), ExtensionAlong f D g0) * (forall h k : forall b : B, D b, ExtendableAlong n f (fun b : B => h b = k b)) -> (forall g0 : forall a : A, C (f a), ExtensionAlong f C g0) * (forall h k : forall b : B, C b, ExtendableAlong n f (fun b : B => h b = k b))
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b : B, C0 b <~> D0 b) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b : B, D b <~> C b

(forall g0 : forall a : A, D (f a), ExtensionAlong f D g0) * (forall h k : forall b : B, D b, ExtendableAlong n f (fun b : B => h b = k b)) -> (forall g0 : forall a : A, C (f a), ExtensionAlong f C g0) * (forall h k : forall b : B, C b, ExtendableAlong n f (fun b : B => h b = k b))
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b : B, C0 b <~> D0 b) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b : B, D b <~> C b

(forall g0 : forall a : A, D (f a), ExtensionAlong f D g0) -> forall g0 : forall a : A, C (f a), ExtensionAlong f C g0
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b : B, C0 b <~> D0 b) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b : B, D b <~> C b
(forall h k : forall b : B, D b, ExtendableAlong n f (fun b : B => h b = k b)) -> forall h k : forall b : B, C b, ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b : B, C0 b <~> D0 b) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b : B, D b <~> C b

(forall g0 : forall a : A, D (f a), ExtensionAlong f D g0) -> forall g0 : forall a : A, C (f a), ExtensionAlong f C g0
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b : B, C0 b <~> D0 b) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b : B, D b <~> C b
h: forall a : A, C (f a)

ExtensionAlong f D (functor_forall idmap (fun a : A => (g (f a))^-1) h) -> ExtensionAlong f C h
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b : B, C0 b <~> D0 b) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b : B, D b <~> C b
h: forall a : A, C (f a)
k: forall a : B, D a

(forall x : A, k (f x) = functor_forall idmap (fun a : A => (g (f a))^-1) h x) -> forall x : A, functor_forall idmap (fun b : B => g b) k (f x) = h x
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b : B, C0 b <~> D0 b) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b : B, D b <~> C b
h: forall a0 : A, C (f a0)
k: forall a0 : B, D a0
a: A

k (f a) = (g (f a))^-1 (h a) -> g (f a) (k (f a)) = h a
apply moveR_equiv_M.
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b : B, C0 b <~> D0 b) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b : B, D b <~> C b

(forall h k : forall b : B, D b, ExtendableAlong n f (fun b : B => h b = k b)) -> forall h k : forall b : B, C b, ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b : B, C0 b <~> D0 b) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b : B, D b <~> C b
h: forall a : B, C a

(forall k : forall b : B, D b, ExtendableAlong n f (fun b : B => functor_forall idmap (fun b0 : B => (g b0)^-1) h b = k b)) -> forall k : forall b : B, C b, ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b : B, C0 b <~> D0 b) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b : B, D b <~> C b
h, k: forall a : B, C a

ExtendableAlong n f (fun b : B => (g b)^-1 (h b) = (g b)^-1 (k b)) -> ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IH: forall D0 C0 : B -> Type, (forall b0 : B, C0 b0 <~> D0 b0) -> ExtendableAlong n f C0 -> ExtendableAlong n f D0
C, D: B -> Type
g: forall b0 : B, D b0 <~> C b0
h, k: forall a : B, C a
b: B

(g b)^-1 (h b) = (g b)^-1 (k b) <~> h b = k b
apply equiv_inverse, equiv_ap; exact _. Defined. Definition extendable_postcompose (n : nat) {A B : Type} (C D : B -> Type) (f : A -> B) (g : forall b, C b -> D b) `{forall b, IsEquiv (g b)} : ExtendableAlong n f C -> ExtendableAlong n f D := extendable_postcompose' n C D f (fun b => Build_Equiv _ _ (g b) _). (** Composition of the maps we extend along. This also does not require funext. *)
n: nat
A, B, C: Type
P: C -> Type
f: A -> B
g: B -> C

ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (g o f) P
n: nat
A, B, C: Type
P: C -> Type
f: A -> B
g: B -> C

ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (g o f) P
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))

forall g0 : forall a : A, P (g (f a)), ExtensionAlong (fun x : A => g (f x)) P g0
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))
forall h k : forall b : C, P b, ExtendableAlong n (fun x : A => g (f x)) (fun b : C => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))

forall g0 : forall a : A, P (g (f a)), ExtensionAlong (fun x : A => g (f x)) P g0
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))
h: forall a : A, P (g (f a))

ExtensionAlong (fun x : A => g (f x)) P h
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))
h: forall a0 : A, P (g (f a0))
a: A

(fst extg (fst extf h).1).1 (g (f a)) = h a
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))
h: forall a0 : A, P (g (f a0))
a: A

(fst extf h).1 (f a) = h a
exact ((fst extf h).2 a).
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))

forall h k : forall b : C, P b, ExtendableAlong n (fun x : A => g (f x)) (fun b : C => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))
h, k: forall b : C, P b

ExtendableAlong n (fun x : A => g (f x)) (fun b : C => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))
h, k: forall b : C, P b

ExtendableAlong n g (fun b : C => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))
h, k: forall b : C, P b
ExtendableAlong n f (fun b : B => h (g b) = k (g b))
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))
h, k: forall b : C, P b

ExtendableAlong n g (fun b : C => h b = k b)
exact (snd extg h k).
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0
P: C -> Type
extg: ExtendableAlong n.+1 g P
extf: ExtendableAlong n.+1 f (fun b : B => P (g b))
h, k: forall b : C, P b

ExtendableAlong n f (fun b : B => h (g b) = k (g b))
exact (snd extf (h oD g) (k oD g)). Defined. (** And cancellation *)
n: nat
A, B, C: Type
P: C -> Type
f: A -> B
g: B -> C

ExtendableAlong n g P -> ExtendableAlong n (g o f) P -> ExtendableAlong n f (fun b : B => P (g b))
n: nat
A, B, C: Type
P: C -> Type
f: A -> B
g: B -> C

ExtendableAlong n g P -> ExtendableAlong n (g o f) P -> ExtendableAlong n f (fun b : B => P (g b))
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P

forall g0 : forall a : A, P (g (f a)), ExtensionAlong f (fun b : B => P (g b)) g0
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
forall h k : forall b : B, P (g b), ExtendableAlong n f (fun b : B => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P

forall g0 : forall a : A, P (g (f a)), ExtensionAlong f (fun b : B => P (g b)) g0
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h: forall a : A, P (g (f a))

ExtensionAlong f (fun b : B => P (g b)) h
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h: forall a0 : A, P (g (f a0))
a: A

((fst extgf h).1 oD g) (f a) = h a
exact ((fst extgf h).2 a).
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P

forall h k : forall b : B, P (g b), ExtendableAlong n f (fun b : B => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : B, P (g b)

ExtendableAlong n f (fun b : B => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : B, P (g b)
h':= (fst extg h).1: forall y : C, P y

ExtendableAlong n f (fun b : B => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : B, P (g b)
h':= (fst extg h).1: forall y : C, P y
k':= (fst extg k).1: forall y : C, P y

ExtendableAlong n f (fun b : B => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : B, P (g b)
h':= (fst extg h).1: forall y : C, P y
k':= (fst extg k).1: forall y : C, P y

forall b : B, h' (g b) = k' (g b) <~> h b = k b
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : B, P (g b)
h':= (fst extg h).1: forall y : C, P y
k':= (fst extg k).1: forall y : C, P y
ExtendableAlong n f (fun b : B => h' (g b) = k' (g b))
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : B, P (g b)
h':= (fst extg h).1: forall y : C, P y
k':= (fst extg k).1: forall y : C, P y

forall b : B, h' (g b) = k' (g b) <~> h b = k b
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b0 : B => P0 (g b0))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b0 : B, P (g b0)
h':= (fst extg h).1: forall y : C, P y
k':= (fst extg k).1: forall y : C, P y
b: B

h' (g b) = k' (g b) <~> h b = k b
exact (equiv_concat_lr ((fst extg h).2 b)^ ((fst extg k).2 b)).
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n g P0 -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n f (fun b : B => P0 (g b))
P: C -> Type
extg: ExtendableAlong n.+1 g P
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : B, P (g b)
h':= (fst extg h).1: forall y : C, P y
k':= (fst extg k).1: forall y : C, P y

ExtendableAlong n f (fun b : B => h' (g b) = k' (g b))
exact (IHn (fun c => h' c = k' c) (snd extg h' k') (snd extgf h' k')). Defined.
n: nat
A, B, C: Type
P: C -> Type
f: A -> B
g: B -> C

ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (g o f) P -> ExtendableAlong n g P
n: nat
A, B, C: Type
P: C -> Type
f: A -> B
g: B -> C

ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (g o f) P -> ExtendableAlong n g P
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b : B => P (g b))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P

forall g0 : forall a : B, P (g a), ExtensionAlong g P g0
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b : B => P (g b))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
forall h k : forall b : C, P b, ExtendableAlong n g (fun b : C => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b : B => P (g b))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P

forall g0 : forall a : B, P (g a), ExtensionAlong g P g0
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b : B => P (g b))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h: forall a : B, P (g a)

ExtensionAlong g P h
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b0 : B => P0 (g b0)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b0 : B => P (g b0))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h: forall a : B, P (g a)
b: B

(fst extgf (h oD f)).1 (g b) = h b
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b0 : B => P0 (g b0)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b0 : B => P (g b0))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h: forall a0 : B, P (g a0)
b: B
a: A

((fst extgf (h oD f)).1 oD g) (f a) = h (f a)
apply ((fst extgf (h oD f)).2).
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b : B => P (g b))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P

forall h k : forall b : C, P b, ExtendableAlong n g (fun b : C => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b : B => P (g b))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : C, P b

ExtendableAlong n g (fun b : C => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b : B => P (g b))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : C, P b

ExtendableAlong n.+1 f (fun b : B => h (g b) = k (g b))
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b : B => P (g b))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : C, P b
ExtendableAlong n (fun x : A => g (f x)) (fun b : C => h b = k b)
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b : B => P (g b))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : C, P b

ExtendableAlong n.+1 f (fun b : B => h (g b) = k (g b))
exact (snd extf (h oD g) (k oD g)).
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P0 : C -> Type, ExtendableAlong n.+1 f (fun b : B => P0 (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P0 -> ExtendableAlong n g P0
P: C -> Type
extf: ExtendableAlong n.+2 f (fun b : B => P (g b))
extgf: ExtendableAlong n.+1 (fun x : A => g (f x)) P
h, k: forall b : C, P b

ExtendableAlong n (fun x : A => g (f x)) (fun b : C => h b = k b)
exact (snd extgf h k). Defined. (** And transfer across homotopies *)
n: nat
A, B: Type
C: B -> Type
f, g: A -> B
p: f == g

ExtendableAlong n f C -> ExtendableAlong n g C
n: nat
A, B: Type
C: B -> Type
f, g: A -> B
p: f == g

ExtendableAlong n f C -> ExtendableAlong n g C
A, B: Type
f, g: A -> B
p: f == g
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 -> ExtendableAlong n g C0
C: B -> Type
extf: ExtendableAlong n.+1 f C

forall g0 : forall a : A, C (g a), ExtensionAlong g C g0
A, B: Type
f, g: A -> B
p: f == g
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 -> ExtendableAlong n g C0
C: B -> Type
extf: ExtendableAlong n.+1 f C
forall h k : forall b : B, C b, ExtendableAlong n g (fun b : B => h b = k b)
A, B: Type
f, g: A -> B
p: f == g
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 -> ExtendableAlong n g C0
C: B -> Type
extf: ExtendableAlong n.+1 f C

forall g0 : forall a : A, C (g a), ExtensionAlong g C g0
A, B: Type
f, g: A -> B
p: f == g
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 -> ExtendableAlong n g C0
C: B -> Type
extf: ExtendableAlong n.+1 f C
h: forall a : A, C (g a)

ExtensionAlong g C h
A, B: Type
f, g: A -> B
p: f == g
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 -> ExtendableAlong n g C0
C: B -> Type
extf: ExtendableAlong n.+1 f C
h: forall a0 : A, C (g a0)
a: A

(fst extf (fun a0 : A => transport C (p a0)^ (h a0))).1 (g a) = h a
A, B: Type
f, g: A -> B
p: f == g
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 -> ExtendableAlong n g C0
C: B -> Type
extf: ExtendableAlong n.+1 f C
h: forall a0 : A, C (g a0)
a: A

transport C (p a) ((fst extf (fun a0 : A => transport C (p a0)^ (h a0))).1 (f a)) = h a
A, B: Type
f, g: A -> B
p: f == g
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 -> ExtendableAlong n g C0
C: B -> Type
extf: ExtendableAlong n.+1 f C
h: forall a0 : A, C (g a0)
a: A

(fst extf (fun a0 : A => transport C (p a0)^ (h a0))).1 (f a) = transport C (p a)^ (h a)
exact ((fst extf (fun a => (p a)^ # h a)).2 a).
A, B: Type
f, g: A -> B
p: f == g
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 -> ExtendableAlong n g C0
C: B -> Type
extf: ExtendableAlong n.+1 f C

forall h k : forall b : B, C b, ExtendableAlong n g (fun b : B => h b = k b)
A, B: Type
f, g: A -> B
p: f == g
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0 -> ExtendableAlong n g C0
C: B -> Type
extf: ExtendableAlong n.+1 f C
h, k: forall b : B, C b

ExtendableAlong n g (fun b : B => h b = k b)
apply IHn, (snd extf h k). Defined. (** We can extend along equivalences *)
n: nat
A, B: Type
C: B -> Type
f: A -> B
H: IsEquiv f

ExtendableAlong n f C
n: nat
A, B: Type
C: B -> Type
f: A -> B
H: IsEquiv f

ExtendableAlong n f C
A, B: Type
f: A -> B
H: IsEquiv f
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0
C: B -> Type

forall g : forall a : A, C (f a), ExtensionAlong f C g
A, B: Type
f: A -> B
H: IsEquiv f
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0
C: B -> Type
forall h k : forall b : B, C b, ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
H: IsEquiv f
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0
C: B -> Type

forall g : forall a : A, C (f a), ExtensionAlong f C g
A, B: Type
f: A -> B
H: IsEquiv f
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0
C: B -> Type
h: forall a : A, C (f a)

ExtensionAlong f C h
A, B: Type
f: A -> B
H: IsEquiv f
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0
C: B -> Type
h: forall a0 : A, C (f a0)
a: A

transport C (eisretr f (f a)) (h (f^-1 (f a))) = h a
A, B: Type
f: A -> B
H: IsEquiv f
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0
C: B -> Type
h: forall a0 : A, C (f a0)
a: A

transport C (ap f (eissect f a)) (h (f^-1 (f a))) = h a
A, B: Type
f: A -> B
H: IsEquiv f
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0
C: B -> Type
h: forall a0 : A, C (f a0)
a: A

transport (fun x : A => C (f x)) (eissect f a) (h (f^-1 (f a))) = h a
exact (apD h (eissect f a)).
A, B: Type
f: A -> B
H: IsEquiv f
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0
C: B -> Type

forall h k : forall b : B, C b, ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
H: IsEquiv f
n: nat
IHn: forall C0 : B -> Type, ExtendableAlong n f C0
C: B -> Type
h, k: forall b : B, C b

ExtendableAlong n f (fun b : B => h b = k b)
apply IHn. Defined. (** And into contractible types *)
n: nat
A, B: Type
C: B -> Type
f: A -> B
H: forall b : B, Contr (C b)

ExtendableAlong n f C
n: nat
A, B: Type
C: B -> Type
f: A -> B
H: forall b : B, Contr (C b)

ExtendableAlong n f C
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, Contr (C0 b)) -> ExtendableAlong n f C0
C: B -> Type
H: forall b : B, Contr (C b)

forall g : forall a : A, C (f a), ExtensionAlong f C g
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, Contr (C0 b)) -> ExtendableAlong n f C0
C: B -> Type
H: forall b : B, Contr (C b)
forall h k : forall b : B, C b, ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, Contr (C0 b)) -> ExtendableAlong n f C0
C: B -> Type
H: forall b : B, Contr (C b)

forall g : forall a : A, C (f a), ExtensionAlong f C g
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, Contr (C0 b)) -> ExtendableAlong n f C0
C: B -> Type
H: forall b : B, Contr (C b)
h: forall a : A, C (f a)

ExtensionAlong f C h
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, Contr (C0 b)) -> ExtendableAlong n f C0
C: B -> Type
H: forall b : B, Contr (C b)
h: forall a0 : A, C (f a0)
a: A

center (C (f a)) = h a
apply contr.
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, Contr (C0 b)) -> ExtendableAlong n f C0
C: B -> Type
H: forall b : B, Contr (C b)

forall h k : forall b : B, C b, ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, Contr (C0 b)) -> ExtendableAlong n f C0
C: B -> Type
H: forall b : B, Contr (C b)
h, k: forall b : B, C b

ExtendableAlong n f (fun b : B => h b = k b)
apply IHn; exact _. Defined. (** This is inherited by types of homotopies. *)
n: nat
A, B: Type
C: B -> Type
f: A -> B
h, k: forall b : B, C b

ExtendableAlong n.+1 f C -> ExtendableAlong n f (fun b : B => h b = k b)
n: nat
A, B: Type
C: B -> Type
f: A -> B
h, k: forall b : B, C b

ExtendableAlong n.+1 f C -> ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IHn: forall (C0 : B -> Type) (h0 k0 : forall b : B, C0 b), ExtendableAlong n.+1 f C0 -> ExtendableAlong n f (fun b : B => h0 b = k0 b)
C: B -> Type
h, k: forall b : B, C b
ext: ExtendableAlong n.+2 f C

forall g : forall a : A, h (f a) = k (f a), ExtensionAlong f (fun b : B => h b = k b) g
A, B: Type
f: A -> B
n: nat
IHn: forall (C0 : B -> Type) (h0 k0 : forall b : B, C0 b), ExtendableAlong n.+1 f C0 -> ExtendableAlong n f (fun b : B => h0 b = k0 b)
C: B -> Type
h, k: forall b : B, C b
ext: ExtendableAlong n.+2 f C
forall h0 k0 : forall b : B, h b = k b, ExtendableAlong n f (fun b : B => h0 b = k0 b)
A, B: Type
f: A -> B
n: nat
IHn: forall (C0 : B -> Type) (h0 k0 : forall b : B, C0 b), ExtendableAlong n.+1 f C0 -> ExtendableAlong n f (fun b : B => h0 b = k0 b)
C: B -> Type
h, k: forall b : B, C b
ext: ExtendableAlong n.+2 f C

forall g : forall a : A, h (f a) = k (f a), ExtensionAlong f (fun b : B => h b = k b) g
A, B: Type
f: A -> B
n: nat
IHn: forall (C0 : B -> Type) (h0 k0 : forall b : B, C0 b), ExtendableAlong n.+1 f C0 -> ExtendableAlong n f (fun b : B => h0 b = k0 b)
C: B -> Type
h, k: forall b : B, C b
ext: ExtendableAlong n.+2 f C
p: forall a : A, h (f a) = k (f a)

ExtensionAlong f (fun b : B => h b = k b) p
exact (fst (snd ext h k) p).
A, B: Type
f: A -> B
n: nat
IHn: forall (C0 : B -> Type) (h0 k0 : forall b : B, C0 b), ExtendableAlong n.+1 f C0 -> ExtendableAlong n f (fun b : B => h0 b = k0 b)
C: B -> Type
h, k: forall b : B, C b
ext: ExtendableAlong n.+2 f C

forall h0 k0 : forall b : B, h b = k b, ExtendableAlong n f (fun b : B => h0 b = k0 b)
A, B: Type
f: A -> B
n: nat
IHn: forall (C0 : B -> Type) (h0 k0 : forall b : B, C0 b), ExtendableAlong n.+1 f C0 -> ExtendableAlong n f (fun b : B => h0 b = k0 b)
C: B -> Type
h, k: forall b : B, C b
ext: ExtendableAlong n.+2 f C
p, q: forall b : B, h b = k b

ExtendableAlong n f (fun b : B => p b = q b)
apply IHn, ext. Defined. (** And the oo-version. *) Definition ooExtendableAlong@{i j k l} {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := forall n : nat, ExtendableAlong@{i j k l} n f C. (** Universe parameters are the same as for [ExtendableAlong]. *) Global Arguments ooExtendableAlong {A B}%_type_scope (f C)%_function_scope. (** Universe modification. *) Definition lift_ooextendablealong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} {A : Type@{amin}} {B : Type@{bmin}} (f : A -> B) (P : B -> Type@{pmin}) : ooExtendableAlong@{a1 b1 p1 m1} f P -> ooExtendableAlong@{a2 b2 p2 m2} f P := fun ext n => lift_extendablealong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} n f P (ext n). (** We take part of the data from [ps 1] and part from [ps 2] so that the inverse chosen is the expected one. *) Definition isequiv_ooextendable `{Funext} {A B : Type} (C : B -> Type) (f : A -> B) : ooExtendableAlong f C -> IsEquiv (fun g => g oD f) := fun ps => isequiv_extendable 0 (fst (ps 1%nat), snd (ps 2)).
H: Funext
A, B: Type
C: B -> Type
f: A -> B

ooExtendableAlong f C <~> ooPathSplit (fun g : forall b : B, C b => g oD f)
H: Funext
A, B: Type
C: B -> Type
f: A -> B

ooExtendableAlong f C <~> ooPathSplit (fun g : forall b : B, C b => g oD f)
H: Funext
A, B: Type
C: B -> Type
f: A -> B
n: nat

ExtendableAlong (1%equiv n) f C <~> PathSplit n (fun g : forall b : B, C b => g oD f)
apply equiv_extendable_pathsplit. Defined.
H: Funext
A, B: Type
C: B -> Type
f: A -> B

IsHProp (ooExtendableAlong f C)
H: Funext
A, B: Type
C: B -> Type
f: A -> B

IsHProp (ooExtendableAlong f C)
exact (istrunc_equiv_istrunc _ (equiv_ooextendable_pathsplit C f)^-1). Defined. Definition equiv_ooextendable_isequiv `{Funext} {A B : Type} (C : B -> Type) (f : A -> B) : ooExtendableAlong f C <~> IsEquiv (fun (g : forall b, C b) => g oD f) := equiv_oopathsplit_isequiv _ oE equiv_ooextendable_pathsplit _ _. Definition ooextendable_postcompose {A B : Type} (C D : B -> Type) (f : A -> B) (g : forall b, C b -> D b) `{forall b, IsEquiv (g b)} : ooExtendableAlong f C -> ooExtendableAlong f D := fun ppp n => extendable_postcompose n C D f g (ppp n). Definition ooextendable_postcompose' {A B : Type} (C D : B -> Type) (f : A -> B) (g : forall b, C b <~> D b) : ooExtendableAlong f C -> ooExtendableAlong f D := fun ppp n => extendable_postcompose' n C D f g (ppp n). Definition ooextendable_compose {A B C : Type} (P : C -> Type) (f : A -> B) (g : B -> C) : ooExtendableAlong g P -> ooExtendableAlong f (fun b => P (g b)) -> ooExtendableAlong (g o f) P := fun extg extf n => extendable_compose n P f g (extg n) (extf n). Definition cancelL_ooextendable {A B C : Type} (P : C -> Type) (f : A -> B) (g : B -> C) : ooExtendableAlong g P -> ooExtendableAlong (g o f) P -> ooExtendableAlong f (fun b => P (g b)) := fun extg extgf n => cancelL_extendable n P f g (extg n) (extgf n). Definition cancelR_ooextendable {A B C : Type} (P : C -> Type) (f : A -> B) (g : B -> C) : ooExtendableAlong f (fun b => P (g b)) -> ooExtendableAlong (g o f) P -> ooExtendableAlong g P := fun extf extgf n => cancelR_extendable n P f g (extf n.+1) (extgf n). Definition ooextendable_homotopic {A B : Type} (C : B -> Type) (f : A -> B) {g : A -> B} (p : f == g) : ooExtendableAlong f C -> ooExtendableAlong g C := fun extf n => extendable_homotopic n C f p (extf n). Definition ooextendable_equiv {A B : Type} (C : B -> Type) (f : A -> B) `{IsEquiv _ _ f} : ooExtendableAlong f C := fun n => extendable_equiv n C f. Definition ooextendable_contr {A B : Type} (C : B -> Type) (f : A -> B) `{forall b, Contr (C b)} : ooExtendableAlong f C := fun n => extendable_contr n C f.
A, B: Type
C: B -> Type
f: A -> B
h, k: forall b : B, C b

ooExtendableAlong f C -> ooExtendableAlong f (fun b : B => h b = k b)
A, B: Type
C: B -> Type
f: A -> B
h, k: forall b : B, C b

ooExtendableAlong f C -> ooExtendableAlong f (fun b : B => h b = k b)
intros ext n; apply extendable_homotopy, ext. Defined. (** Extendability of a family [C] along a map [f] can be detected by extendability of the constant family [C b] along the projection from the corresponding fiber of [f] to [Unit]. Note that this is *not* an if-and-only-if; the hypothesis can be genuinely stronger than the conclusion. *)
A, B: Type
f: A -> B
C: B -> Type

(forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ooExtendableAlong f C
A, B: Type
f: A -> B
C: B -> Type

(forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ooExtendableAlong f C
A, B: Type
f: A -> B
n: nat

forall C : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ExtendableAlong n f C
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C0 b))) -> ExtendableAlong n f C0
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))

forall g : forall a : A, C (f a), ExtensionAlong f C g
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C0 b))) -> ExtendableAlong n f C0
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))
forall h k : forall b : B, C b, ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C0 b))) -> ExtendableAlong n f C0
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))

forall g : forall a : A, C (f a), ExtensionAlong f C g
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C0 b))) -> ExtendableAlong n f C0
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))
g: forall a : A, C (f a)

ExtensionAlong f C g
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C0 b))) -> ExtendableAlong n f C0
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))
g: forall a : A, C (f a)

forall x : A, (fst (orth (f x) 1) (fun x0 : hfiber f (f x) => transport C x0.2 (g x0.1))).1 tt = g x
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C0 b))) -> ExtendableAlong n f C0
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))
g: forall a0 : A, C (f a0)
a: A

(fst (orth (f a) 1) (fun x : hfiber f (f a) => transport C x.2 (g x.1))).1 tt = g a
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C0 b))) -> ExtendableAlong n f C0
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))
g: forall a0 : A, C (f a0)
a: A

(fst (orth (f a) 1) (fun x : hfiber f (f a) => transport C x.2 (g x.1))).1 (const_tt A a) = g a
exact ((fst (orth (f a) 1%nat) _).2 (a ; 1)).
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C0 b))) -> ExtendableAlong n f C0
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))

forall h k : forall b : B, C b, ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C0 b))) -> ExtendableAlong n f C0
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))
h, k: forall b : B, C b

ExtendableAlong n f (fun b : B => h b = k b)
A, B: Type
f: A -> B
n: nat
IHn: forall C0 : B -> Type, (forall b0 : B, ooExtendableAlong (const_tt (hfiber f b0)) (unit_name (C0 b0))) -> ExtendableAlong n f C0
C: B -> Type
orth: forall b0 : B, ooExtendableAlong (const_tt (hfiber f b0)) (unit_name (C b0))
h, k: forall b0 : B, C b0
b: B

ooExtendableAlong (const_tt (hfiber f b)) (unit_name (h b = k b))
apply ooextendable_homotopy, orth. Defined. End Extensions. (** ** Extendability along cofibrations *) (** If a family is extendable along a cofibration (i.e. a mapping cylinder), it is extendable definitionally. *)
A, B: Type
f: A -> B
C: Cyl f -> Type
g: forall a : A, C (cyl a)
ext: ExtensionAlong cyl C g

ExtensionAlong cyl C g
A, B: Type
f: A -> B
C: Cyl f -> Type
g: forall a : A, C (cyl a)
ext: ExtensionAlong cyl C g

ExtensionAlong cyl C g
A, B: Type
f: A -> B
C: Cyl f -> Type
g: forall a0 : A, C (cyl a0)
ext: ExtensionAlong cyl C g
a: A

DPath C (cyglue a) (g a) ((ext.1 o cyr) (f a))
A, B: Type
f: A -> B
C: Cyl f -> Type
g: forall a0 : A, C (cyl a0)
ext: ExtensionAlong cyl C g
a: A
Cyl_ind C g (fun x : B => ext.1 (cyr x)) (fun a0 : A => ?Goal@{a:=a0}) (cyl a) = g a
A, B: Type
f: A -> B
C: Cyl f -> Type
g: forall a0 : A, C (cyl a0)
ext: ExtensionAlong cyl C g
a: A

DPath C (cyglue a) (g a) ((ext.1 o cyr) (f a))
A, B: Type
f: A -> B
C: Cyl f -> Type
g: forall a0 : A, C (cyl a0)
ext: ExtensionAlong cyl C g
a: A

DPath C (cyglue a) (ext.1 (cyl a)) (ext.1 (cyr (f a)))
apply apD.
A, B: Type
f: A -> B
C: Cyl f -> Type
g: forall a0 : A, C (cyl a0)
ext: ExtensionAlong cyl C g
a: A

Cyl_ind C g (fun x : B => ext.1 (cyr x)) (fun a0 : A => ((ext.2 a0)^ @Dl apD ext.1 (cyglue a0))%dpath) (cyl a) = g a
reflexivity. (** The point is that this equality is now definitional. *) Defined.
n: nat
A, B: Type
f: A -> B
C: Cyl f -> Type
ext: ExtendableAlong n cyl C

ExtendableAlong n cyl C
n: nat
A, B: Type
f: A -> B
C: Cyl f -> Type
ext: ExtendableAlong n cyl C

ExtendableAlong n cyl C
A, B: Type
f: A -> B
n: nat
IH: forall C0 : Cyl f -> Type, ExtendableAlong n cyl C0 -> ExtendableAlong n cyl C0
C: Cyl f -> Type
ext: ExtendableAlong n.+1 cyl C

forall g : forall a : A, C (cyl a), ExtensionAlong cyl C g
A, B: Type
f: A -> B
n: nat
IH: forall C0 : Cyl f -> Type, ExtendableAlong n cyl C0 -> ExtendableAlong n cyl C0
C: Cyl f -> Type
ext: ExtendableAlong n.+1 cyl C
forall h k : forall b : Cyl f, C b, ExtendableAlong n cyl (fun b : Cyl f => h b = k b)
A, B: Type
f: A -> B
n: nat
IH: forall C0 : Cyl f -> Type, ExtendableAlong n cyl C0 -> ExtendableAlong n cyl C0
C: Cyl f -> Type
ext: ExtendableAlong n.+1 cyl C

forall g : forall a : A, C (cyl a), ExtensionAlong cyl C g
A, B: Type
f: A -> B
n: nat
IH: forall C0 : Cyl f -> Type, ExtendableAlong n cyl C0 -> ExtendableAlong n cyl C0
C: Cyl f -> Type
ext: ExtendableAlong n.+1 cyl C
g: forall a : A, C (cyl a)

ExtensionAlong cyl C g
A, B: Type
f: A -> B
n: nat
IH: forall C0 : Cyl f -> Type, ExtendableAlong n cyl C0 -> ExtendableAlong n cyl C0
C: Cyl f -> Type
ext: ExtendableAlong n.+1 cyl C
g: forall a : A, C (cyl a)

ExtensionAlong cyl C g
exact (fst ext g).
A, B: Type
f: A -> B
n: nat
IH: forall C0 : Cyl f -> Type, ExtendableAlong n cyl C0 -> ExtendableAlong n cyl C0
C: Cyl f -> Type
ext: ExtendableAlong n.+1 cyl C

forall h k : forall b : Cyl f, C b, ExtendableAlong n cyl (fun b : Cyl f => h b = k b)
A, B: Type
f: A -> B
n: nat
IH: forall C0 : Cyl f -> Type, ExtendableAlong n cyl C0 -> ExtendableAlong n cyl C0
C: Cyl f -> Type
ext: ExtendableAlong n.+1 cyl C
h, k: forall b : Cyl f, C b

ExtendableAlong n cyl (fun b : Cyl f => h b = k b)
exact (snd ext h k). Defined. Definition cyl_ooextendable {A B} (f : A -> B) (C : Cyl f -> Type) (ext : ooExtendableAlong cyl C) : ooExtendableAlong cyl C := fun n => cyl_extendable n f C (ext n).
A, B: Type
f: A -> B
C: B -> Type
g: forall a : A, C (pr_cyl (cyl a))
ext: ExtensionAlong f C g

ExtensionAlong cyl (C o pr_cyl) g
A, B: Type
f: A -> B
C: B -> Type
g: forall a : A, C (pr_cyl (cyl a))
ext: ExtensionAlong f C g

ExtensionAlong cyl (C o pr_cyl) g
A, B: Type
f: A -> B
C: B -> Type
g: forall a : A, C (pr_cyl (cyl a))
ext: ExtensionAlong f C g

ExtensionAlong cyl (fun x : Cyl f => C (pr_cyl x)) g
A, B: Type
f: A -> B
C: B -> Type
g: forall a : A, C (pr_cyl (cyl a))
ext: ExtensionAlong f C g

forall x : A, ext.1 (pr_cyl (cyl x)) = g x
intros x; apply ext.2. Defined.
n: nat
A, B: Type
f: A -> B
C: B -> Type
ext: ExtendableAlong n f C

ExtendableAlong n cyl (C o pr_cyl' f)
n: nat
A, B: Type
f: A -> B
C: B -> Type
ext: ExtendableAlong n f C

ExtendableAlong n cyl (C o pr_cyl' f)
n: nat
A, B: Type
f: A -> B
C: B -> Type
ext: ExtendableAlong n f C

ExtendableAlong n cyl (fun x : Cyl f => C (pr_cyl' f x))
n: nat
A, B: Type
f: A -> B
C: B -> Type
ext: ExtendableAlong n f C

ExtendableAlong n pr_cyl C
rapply extendable_equiv. Defined. Definition cyl_ooextendable' {A B} (f : A -> B) (C : B -> Type) (ext : ooExtendableAlong f C) : ooExtendableAlong cyl (C o (pr_cyl' f)) := fun n => cyl_extendable' n f C (ext n). (** ** Extendability along [functor_prod] *)
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
s: forall z : A * B, P (functor_prod f g z)

ExtensionAlong (functor_prod f g) P s
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
s: forall z : A * B, P (functor_prod f g z)

ExtensionAlong (functor_prod f g) P s
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
s: forall z : A * B, P (functor_prod f g z)

forall y : A' * B', P y
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
s: forall z : A * B, P (functor_prod f g z)
(fun s0 : forall y : A' * B', P y => forall x : A * B, s0 (functor_prod f g x) = s x) ?proj1
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
s: forall z : A * B, P (functor_prod f g z)

forall y : A' * B', P y
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a'0 : A' => P (a'0, b'))
eg: forall a'0 : A', ExtendableAlong 1 g (fun b' : B' => P (a'0, b'))
s: forall z : A * B, P (functor_prod f g z)
a': A'

forall b' : B', P (a', b')
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a'0 : A' => P (a'0, b'))
eg: forall a'0 : A', ExtendableAlong 1 g (fun b' : B' => P (a'0, b'))
s: forall z : A * B, P (functor_prod f g z)
a': A'

forall a : B, P (a', g a)
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
s: forall z : A * B, P (functor_prod f g z)
b: B

forall a' : A', P (a', g b)
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
s: forall z : A * B, P (functor_prod f g z)
b: B

forall a : A, P (f a, g b)
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
s: forall z : A * B, P (functor_prod f g z)
b: B
a: A

P (f a, g b)
exact (s (a,b)).
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
s: forall z : A * B, P (functor_prod f g z)

(fun s0 : forall y : A' * B', P y => forall x : A * B, s0 (functor_prod f g x) = s x) (fun y : A' * B' => (fun (a' : A') (b' : B') => (fst (eg a') (fun b : B => (fst (ef (g b)) (fun a : A => s (a, b))).1 a')).1 b') (fst y) (snd y))
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
s: forall z : A * B, P (functor_prod f g z)
a: A
b: B

(fst (eg (f a)) (fun b0 : B => (fst (ef (g b0)) (fun a0 : A => s (a0, b0))).1 (f a))).1 (g b) = s (a, b)
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
s: forall z : A * B, P (functor_prod f g z)
a: A
b: B

(fst (ef (g b)) (fun a0 : A => s (a0, b))).1 (f a) = s (a, b)
exact ((fst (ef (g b)) _).2 a). Defined.
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))

ExtendableAlong n (functor_prod f g) P
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))

ExtendableAlong n (functor_prod f g) P
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))

forall g0 : forall a : A * B, P (functor_prod f g a), ExtensionAlong (functor_prod f g) P g0
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))
forall h k : forall b : A' * B', P b, ExtendableAlong n (functor_prod f g) (fun b : A' * B' => h b = k b)
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))

forall g0 : forall a : A * B, P (functor_prod f g a), ExtensionAlong (functor_prod f g) P g0
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))

forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))
forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))

forall b' : B', ExtendableAlong 1 f (fun a' : A' => P (a', b'))
intros b'; exact (fst (ef b'), fun _ _ => tt).
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))

forall a' : A', ExtendableAlong 1 g (fun b' : B' => P (a', b'))
intros a'; exact (fst (eg a'), fun _ _ => tt).
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))

forall h k : forall b : A' * B', P b, ExtendableAlong n (functor_prod f g) (fun b : A' * B' => h b = k b)
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))
h, k: forall b : A' * B', P b

forall b' : B', ExtendableAlong n f (fun a' : A' => h (a', b') = k (a', b'))
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))
h, k: forall b : A' * B', P b
forall a' : A', ExtendableAlong n g (fun b' : B' => h (a', b') = k (a', b'))
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))
h, k: forall b : A' * B', P b

forall b' : B', ExtendableAlong n f (fun a' : A' => h (a', b') = k (a', b'))
intros b'; apply (snd (ef b')).
A, B, A', B': Type
f: A -> A'
g: B -> B'
n: nat
IH: forall P0 : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P0 (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P0 (a', b'))) -> ExtendableAlong n (functor_prod f g) P0
P: A' * B' -> Type
ef: forall b' : B', ExtendableAlong n.+1 f (fun a' : A' => P (a', b'))
eg: forall a' : A', ExtendableAlong n.+1 g (fun b' : B' => P (a', b'))
h, k: forall b : A' * B', P b

forall a' : A', ExtendableAlong n g (fun b' : B' => h (a', b') = k (a', b'))
intros a'; apply (snd (eg a')). Defined. Definition ooextendable_functor_prod {A B A' B'} (f : A -> A') (g : B -> B') (P : A' * B' -> Type) (ef : forall b', ooExtendableAlong f (fun a' => P (a',b'))) (eg : forall a', ooExtendableAlong g (fun b' => P (a',b'))) : ooExtendableAlong (functor_prod f g) P := fun n => extendable_functor_prod n f g P (fun b' => ef b' n) (fun a' => eg a' n). (** ** Extendability along [functor_sigma] *)
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong 1 (f a) (fun v : Q a => C (a; v))
s: forall z : {x : _ & P x}, C (functor_sigma idmap f z)

ExtensionAlong (functor_sigma idmap f) C s
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong 1 (f a) (fun v : Q a => C (a; v))
s: forall z : {x : _ & P x}, C (functor_sigma idmap f z)

ExtensionAlong (functor_sigma idmap f) C s
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong 1 (f a) (fun v : Q a => C (a; v))
s: forall z : {x : _ & P x}, C (functor_sigma idmap f z)

forall y : {x : _ & Q x}, C y
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong 1 (f a) (fun v : Q a => C (a; v))
s: forall z : {x : _ & P x}, C (functor_sigma idmap f z)
(fun s0 : forall y : {x : _ & Q x}, C y => forall x : {x : _ & P x}, s0 (functor_sigma idmap f x) = s x) ?proj1
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong 1 (f a) (fun v : Q a => C (a; v))
s: forall z : {x : _ & P x}, C (functor_sigma idmap f z)

forall y : {x : _ & Q x}, C y
A: Type
P, Q: A -> Type
f: forall a0 : A, P a0 -> Q a0
C: {x : _ & Q x} -> Type
ef: forall a0 : A, ExtendableAlong 1 (f a0) (fun v : Q a0 => C (a0; v))
s: forall z : {x : _ & P x}, C (functor_sigma idmap f z)
a: A

forall v : Q a, C (a; v)
A: Type
P, Q: A -> Type
f: forall a0 : A, P a0 -> Q a0
C: {x : _ & Q x} -> Type
ef: forall a0 : A, ExtendableAlong 1 (f a0) (fun v : Q a0 => C (a0; v))
s: forall z : {x : _ & P x}, C (functor_sigma idmap f z)
a: A

forall a0 : P a, C (a; f a a0)
A: Type
P, Q: A -> Type
f: forall a0 : A, P a0 -> Q a0
C: {x : _ & Q x} -> Type
ef: forall a0 : A, ExtendableAlong 1 (f a0) (fun v : Q a0 => C (a0; v))
s: forall z : {x : _ & P x}, C (functor_sigma idmap f z)
a: A
u: P a

C (a; f a u)
exact (s (a;u)).
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong 1 (f a) (fun v : Q a => C (a; v))
s: forall z : {x : _ & P x}, C (functor_sigma idmap f z)

(fun s0 : forall y : {x : _ & Q x}, C y => forall x : {x : _ & P x}, s0 (functor_sigma idmap f x) = s x) (fun y : {x : _ & Q x} => (fun (a : A) (v : Q a) => (fst (ef a) (fun u : P a => s (a; u))).1 v) y.1 y.2)
A: Type
P, Q: A -> Type
f: forall a0 : A, P a0 -> Q a0
C: {x : _ & Q x} -> Type
ef: forall a0 : A, ExtendableAlong 1 (f a0) (fun v : Q a0 => C (a0; v))
s: forall z : {x : _ & P x}, C (functor_sigma idmap f z)
a: A
u: P a

(fst (ef a) (fun u0 : P a => s (a; u0))).1 (f a u) = s (a; u)
exact ((fst (ef a) _).2 u). Defined.
n: nat
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong n (f a) (fun v : Q a => C (a; v))

ExtendableAlong n (functor_sigma idmap f) C
n: nat
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong n (f a) (fun v : Q a => C (a; v))

ExtendableAlong n (functor_sigma idmap f) C
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C0 (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C0
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong n.+1 (f a) (fun v : Q a => C (a; v))

forall g : forall a : {x : _ & P x}, C (functor_sigma idmap f a), ExtensionAlong (functor_sigma idmap f) C g
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C0 (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C0
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong n.+1 (f a) (fun v : Q a => C (a; v))
forall h k : forall b : {x : _ & Q x}, C b, ExtendableAlong n (functor_sigma idmap f) (fun b : {x : _ & Q x} => h b = k b)
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C0 (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C0
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong n.+1 (f a) (fun v : Q a => C (a; v))

forall g : forall a : {x : _ & P x}, C (functor_sigma idmap f a), ExtensionAlong (functor_sigma idmap f) C g
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C0 (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C0
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong n.+1 (f a) (fun v : Q a => C (a; v))

forall a : A, ExtendableAlong 1 (f a) (fun v : Q a => C (a; v))
intros a; exact (fst (ef a) , fun _ _ => tt).
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C0 (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C0
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong n.+1 (f a) (fun v : Q a => C (a; v))

forall h k : forall b : {x : _ & Q x}, C b, ExtendableAlong n (functor_sigma idmap f) (fun b : {x : _ & Q x} => h b = k b)
A: Type
P, Q: A -> Type
f: forall a : A, P a -> Q a
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C0 (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C0
C: {x : _ & Q x} -> Type
ef: forall a : A, ExtendableAlong n.+1 (f a) (fun v : Q a => C (a; v))
h, k: forall b : {x : _ & Q x}, C b

forall a : A, ExtendableAlong n (f a) (fun v : Q a => h (a; v) = k (a; v))
intros a; apply (snd (ef a)). Defined. Definition ooextendable_functor_sigma_id {A} {P Q : A -> Type} (f : forall a, P a -> Q a) (C : sig Q -> Type) (ef : forall a, ooExtendableAlong (f a) (fun v => C (a;v))) : ooExtendableAlong (functor_sigma idmap f) C := fun n => extendable_functor_sigma_id n f C (fun a => ef a n). (** Unfortunately, the technology of [ExtensionAlong] seems to be insufficient to state a general, funext-free version of [extension_functor_sigma] with a non-identity map on the bases; the hypothesis on the fiberwise map would have to be the existence of an extension in a function-type "up to pointwise equality". With wild oo-groupoids we could probably manage it. For now, we say something a bit hacky. *) Definition HomotopyExtensionAlong {A B} {Q : B -> Type} (f : A -> B) (C : sig Q -> Type) (p : forall (a:A) (v:Q (f a)), C (f a;v)) := { q : forall (b:B) (v:Q b), C (b;v) & forall a v, q (f a) v = p a v }. Fixpoint HomotopyExtendableAlong (n : nat) {A B} {Q : B -> Type} (f : A -> B) (C : sig Q -> Type) : Type := match n with | 0 => Unit | S n => ((forall (p : forall (a:A) (v:Q (f a)), C (f a;v)), HomotopyExtensionAlong f C p) * (forall (h k : forall z, C z), HomotopyExtendableAlong n f (fun z => h z = k z))) end. Definition ooHomotopyExtendableAlong {A B} {Q : B -> Type} (f : A -> B) (C : sig Q -> Type) := forall n, HomotopyExtendableAlong n f C.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a : A, ExtendableAlong 1 (g a) (fun v : Q (f a) => C (f a; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)

ExtensionAlong (functor_sigma f g) C s
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a : A, ExtendableAlong 1 (g a) (fun v : Q (f a) => C (f a; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)

ExtensionAlong (functor_sigma f g) C s
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a : A, ExtendableAlong 1 (g a) (fun v : Q (f a) => C (f a; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)

forall y : {x : _ & Q x}, C y
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a : A, ExtendableAlong 1 (g a) (fun v : Q (f a) => C (f a; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)
(fun s0 : forall y : {x : _ & Q x}, C y => forall x : {x : _ & P x}, s0 (functor_sigma f g x) = s x) ?proj1
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a : A, ExtendableAlong 1 (g a) (fun v : Q (f a) => C (f a; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)

forall y : {x : _ & Q x}, C y
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a : A, ExtendableAlong 1 (g a) (fun v : Q (f a) => C (f a; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)

forall (b : B) (v : Q b), C (b; v)
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a : A, ExtendableAlong 1 (g a) (fun v : Q (f a) => C (f a; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)

forall (a : A) (v : Q (f a)), C (f a; v)
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a0 : A, P a0 -> Q (f a0)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a0 : A, ExtendableAlong 1 (g a0) (fun v : Q (f a0) => C (f a0; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)
a: A

forall v : Q (f a), C (f a; v)
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a0 : A, P a0 -> Q (f a0)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a0 : A, ExtendableAlong 1 (g a0) (fun v : Q (f a0) => C (f a0; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)
a: A

forall a0 : P a, C (f a; g a a0)
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a0 : A, P a0 -> Q (f a0)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a0 : A, ExtendableAlong 1 (g a0) (fun v : Q (f a0) => C (f a0; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)
a: A
u: P a

C (f a; g a u)
exact (s (a;u)).
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a : A, ExtendableAlong 1 (g a) (fun v : Q (f a) => C (f a; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)

(fun s0 : forall y : {x : _ & Q x}, C y => forall x : {x : _ & P x}, s0 (functor_sigma f g x) = s x) (fun y : {x : _ & Q x} => (fun (b : B) (v : Q b) => (fst ef (fun a : A => (fst (eg a) (fun u : P a => s (a; u))).1)).1 b v) y.1 y.2)
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a0 : A, P a0 -> Q (f a0)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a0 : A, ExtendableAlong 1 (g a0) (fun v : Q (f a0) => C (f a0; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)
a: A
u: P a

(fst ef (fun a0 : A => (fst (eg a0) (fun u0 : P a0 => s (a0; u0))).1)).1 (f a) (g a u) = s (a; u)
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a0 : A, P a0 -> Q (f a0)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong 1 f C
eg: forall a0 : A, ExtendableAlong 1 (g a0) (fun v : Q (f a0) => C (f a0; v))
s: forall z : {x : _ & P x}, C (functor_sigma f g z)
a: A
u: P a

(fst (eg (a; u).1) (fun u0 : P (a; u).1 => s ((a; u).1; u0))).1 (g (a; u).1 (a; u).2) = s (a; u)
exact ((fst (eg a) _).2 u). Defined.
n: nat
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n f C
eg: forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))

ExtendableAlong n (functor_sigma f g) C
n: nat
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n f C
eg: forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))

ExtendableAlong n (functor_sigma f g) C
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))

forall g0 : forall a : {x : _ & P x}, C (functor_sigma f g a), ExtensionAlong (functor_sigma f g) C g0
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))
forall h k : forall b : {x : _ & Q x}, C b, ExtendableAlong n (functor_sigma f g) (fun b : {x : _ & Q x} => h b = k b)
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))

forall g0 : forall a : {x : _ & P x}, C (functor_sigma f g a), ExtensionAlong (functor_sigma f g) C g0
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))

HomotopyExtendableAlong 1 f C
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))
forall a : A, ExtendableAlong 1 (g a) (fun v : Q (f a) => C (f a; v))
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))

HomotopyExtendableAlong 1 f C
exact (fst ef, fun _ _ => tt).
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))

forall a : A, ExtendableAlong 1 (g a) (fun v : Q (f a) => C (f a; v))
intros a; exact (fst (eg a) , fun _ _ => tt).
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))

forall h k : forall b : {x : _ & Q x}, C b, ExtendableAlong n (functor_sigma f g) (fun b : {x : _ & Q x} => h b = k b)
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))
h, k: forall b : {x : _ & Q x}, C b

HomotopyExtendableAlong n f (fun b : {x : _ & Q x} => h b = k b)
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))
h, k: forall b : {x : _ & Q x}, C b
forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => h (f a; v) = k (f a; v))
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))
h, k: forall b : {x : _ & Q x}, C b

HomotopyExtendableAlong n f (fun b : {x : _ & Q x} => h b = k b)
exact (snd ef h k).
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
n: nat
IH: forall C0 : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C0 -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C0 (f a; v))) -> ExtendableAlong n (functor_sigma f g) C0
C: {x : _ & Q x} -> Type
ef: HomotopyExtendableAlong n.+1 f C
eg: forall a : A, ExtendableAlong n.+1 (g a) (fun v : Q (f a) => C (f a; v))
h, k: forall b : {x : _ & Q x}, C b

forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => h (f a; v) = k (f a; v))
intros a; apply (snd (eg a)). Defined. Definition ooextendable_functor_sigma {A B} {P : A -> Type} {Q : B -> Type} (f : A -> B) (g : forall a, P a -> Q (f a)) (C : sig Q -> Type) (ef : ooHomotopyExtendableAlong f C) (eg : forall a, ooExtendableAlong (g a) (fun v => C (f a ; v))) : ooExtendableAlong (functor_sigma f g) C := fun n => extendable_functor_sigma n f g C (ef n) (fun a => eg a n). (** ** Extendability along [functor_sum] *)
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong 1 f (P o inl)
eg: ExtendableAlong 1 g (P o inr)
h: forall z : A + B, P (functor_sum f g z)

ExtensionAlong (functor_sum f g) P h
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong 1 f (P o inl)
eg: ExtendableAlong 1 g (P o inr)
h: forall z : A + B, P (functor_sum f g z)

ExtensionAlong (functor_sum f g) P h
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong 1 f (P o inl)
eg: ExtendableAlong 1 g (P o inr)
h: forall z : A + B, P (functor_sum f g z)

forall a : A', P (inl a)
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong 1 f (P o inl)
eg: ExtendableAlong 1 g (P o inr)
h: forall z : A + B, P (functor_sum f g z)
forall b : B', P (inr b)
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong 1 f (P o inl)
eg: ExtendableAlong 1 g (P o inr)
h: forall z : A + B, P (functor_sum f g z)
forall a : A, (fun s : A + B => sum_ind P ?f ?g (functor_sum f g s) = h s) (inl a)
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong 1 f (P o inl)
eg: ExtendableAlong 1 g (P o inr)
h: forall z : A + B, P (functor_sum f g z)
forall b : B, (fun s : A + B => sum_ind P ?f ?g (functor_sum f g s) = h s) (inr b)
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong 1 f (P o inl)
eg: ExtendableAlong 1 g (P o inr)
h: forall z : A + B, P (functor_sum f g z)

forall a : A', P (inl a)
exact (fst ef (h o inl)).1.
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong 1 f (P o inl)
eg: ExtendableAlong 1 g (P o inr)
h: forall z : A + B, P (functor_sum f g z)

forall b : B', P (inr b)
exact (fst eg (h o inr)).1.
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong 1 f (P o inl)
eg: ExtendableAlong 1 g (P o inr)
h: forall z : A + B, P (functor_sum f g z)

forall a : A, (fun s : A + B => sum_ind P (fst ef (h o inl)).1 (fst eg (h o inr)).1 (functor_sum f g s) = h s) (inl a)
exact (fst ef (h o inl)).2.
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong 1 f (P o inl)
eg: ExtendableAlong 1 g (P o inr)
h: forall z : A + B, P (functor_sum f g z)

forall b : B, (fun s : A + B => sum_ind P (fst ef (h o inl)).1 (fst eg (h o inr)).1 (functor_sum f g s) = h s) (inr b)
exact (fst eg (h o inr)).2. Defined.
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong n f (P o inl)
eg: ExtendableAlong n g (P o inr)

ExtendableAlong n (functor_sum f g) P
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ExtendableAlong n f (P o inl)
eg: ExtendableAlong n g (P o inr)

ExtendableAlong n (functor_sum f g) P
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))

forall g0 : forall a : A + B, P (functor_sum f g a), ExtensionAlong (functor_sum f g) P g0
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))
forall h k : forall b : A' + B', P b, ExtendableAlong n (functor_sum f g) (fun b : A' + B' => h b = k b)
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))

forall g0 : forall a : A + B, P (functor_sum f g a), ExtensionAlong (functor_sum f g) P g0
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))
h: forall a : A + B, P (functor_sum f g a)

ExtendableAlong 1 f (fun x : A' => P (inl x))
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))
h: forall a : A + B, P (functor_sum f g a)
ExtendableAlong 1 g (fun x : B' => P (inr x))
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))
h: forall a : A + B, P (functor_sum f g a)

ExtendableAlong 1 f (fun x : A' => P (inl x))
exact (fst ef, fun _ _ => tt).
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))
h: forall a : A + B, P (functor_sum f g a)

ExtendableAlong 1 g (fun x : B' => P (inr x))
exact (fst eg, fun _ _ => tt).
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))

forall h k : forall b : A' + B', P b, ExtendableAlong n (functor_sum f g) (fun b : A' + B' => h b = k b)
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))
h, k: forall b : A' + B', P b

ExtendableAlong n (functor_sum f g) (fun b : A' + B' => h b = k b)
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))
h, k: forall b : A' + B', P b

ExtendableAlong n f (fun x : A' => h (inl x) = k (inl x))
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))
h, k: forall b : A' + B', P b
ExtendableAlong n g (fun x : B' => h (inr x) = k (inr x))
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))
h, k: forall b : A' + B', P b

ExtendableAlong n f (fun x : A' => h (inl x) = k (inl x))
exact (snd ef (h o inl) (k o inl)).
n: nat
A, B, A', B': Type
f: A -> A'
g: B -> B'
IH: forall P0 : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P0 (inl x)) -> ExtendableAlong n g (fun x : B' => P0 (inr x)) -> ExtendableAlong n (functor_sum f g) P0
P: A' + B' -> Type
ef: ExtendableAlong n.+1 f (fun x : A' => P (inl x))
eg: ExtendableAlong n.+1 g (fun x : B' => P (inr x))
h, k: forall b : A' + B', P b

ExtendableAlong n g (fun x : B' => h (inr x) = k (inr x))
exact (snd eg (h o inr) (k o inr)). Defined.
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ooExtendableAlong f (P o inl)
eg: ooExtendableAlong g (P o inr)

ooExtendableAlong (functor_sum f g) P
A, B, A', B': Type
f: A -> A'
g: B -> B'
P: A' + B' -> Type
ef: ooExtendableAlong f (P o inl)
eg: ooExtendableAlong g (P o inr)

ooExtendableAlong (functor_sum f g) P
intros n; apply extendable_functor_sum; [ apply ef | apply eg ]. Defined. (** ** Extendability along [functor_coeq] *) (** The path algebra in these proofs is terrible on its own. But by replacing the maps with cofibrations so that many equalities hold definitionally, and modifying the extensions to also be strict, it becomes manageable with a bit of dependent-path technology. *) (** First we show that if we can extend in [C] along [k], and we can extend in appropriate path-types of [C] along [h], then we can extend in [C] along [functor_coeq]. This is where the hard work is. *)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)

ExtensionAlong (functor_coeq h k p q) C s
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)

ExtensionAlong (functor_coeq h k p q) C s
(** We start by changing the problem to involve [CylCoeq] with cofibrations. *)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type

ExtensionAlong (functor_coeq h k p q) C s
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))

ExtensionAlong (functor_coeq h k p q) C s
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))

ExtensionAlong (cyl_cylcoeq p q) C' s'
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
e: ExtensionAlong (cyl_cylcoeq p q) C' s'
ExtensionAlong (functor_coeq h k p q) C s
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
e: ExtensionAlong (cyl_cylcoeq p q) C' s'

ExtensionAlong (functor_coeq h k p q) C s
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
e: ExtensionAlong (cyl_cylcoeq p q) C' s'
ex:= fst (extendable_equiv 1 C (pr_cylcoeq p q)) e.1: ExtensionAlong (pr_cylcoeq p q) C e.1

ExtensionAlong (functor_coeq h k p q) C s
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u x0 = v x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
e: ExtensionAlong (cyl_cylcoeq p q) C' s'
ex:= fst (extendable_equiv 1 C (pr_cylcoeq p q)) e.1: ExtensionAlong (pr_cylcoeq p q) C e.1
x: Coeq f g

ex.1 (functor_coeq h k p q x) = s x
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u x0 = v x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
e: ExtensionAlong (cyl_cylcoeq p q) C' s'
ex:= fst (extendable_equiv 1 C (pr_cylcoeq p q)) e.1: ExtensionAlong (pr_cylcoeq p q) C e.1
x: Coeq f g

transport C (pr_cyl_cylcoeq p q x) (ex.1 (functor_coeq h k p q x)) = transport C (pr_cyl_cylcoeq p q x) (s x)
exact (apD _ (pr_cyl_cylcoeq p q x) @ ex.2 _ @ e.2 x).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))

ExtensionAlong (cyl_cylcoeq p q) C' s'
(** We have to transfer the hypotheses along those equivalences too. We do it using [cyl_extendable] so that the resulting extensions compute definitionally. Note that this means we never need to refer to the [.2] parts of the extensions, since they are identity paths. *)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y

ExtensionAlong (cyl_cylcoeq p q) C' s'
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y

forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
ExtensionAlong (cyl_cylcoeq p q) C' s'
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y

forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong 1 h (fun x : B' => u0 x = v0 x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u0 : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u0).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
u: forall x : Cyl h, C' (coeq (functor_cyl p x))
v: forall x : Cyl h, C' (coeq (functor_cyl q x))

ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong 1 h (fun x : B' => u0 x = v0 x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u0 : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u0).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
u: forall x : Cyl h, C' (coeq (functor_cyl p x))
v: forall x : Cyl h, C' (coeq (functor_cyl q x))

forall b : Cyl h, ?Goal0 b <~> DPath C' (cglue b) (u b) (v b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong 1 h (fun x : B' => u0 x = v0 x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u0 : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u0).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
u: forall x : Cyl h, C' (coeq (functor_cyl p x))
v: forall x : Cyl h, C' (coeq (functor_cyl q x))
ExtendableAlong 1 cyl ?Goal0
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong 1 h (fun x : B' => u0 x = v0 x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u0 : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u0).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
u: forall x : Cyl h, C' (coeq (functor_cyl p x))
v: forall x : Cyl h, C' (coeq (functor_cyl q x))

ExtendableAlong 1 cyl ?Goal0
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong 1 h (fun x : B' => u0 x = v0 x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u0 : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u0).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
u: forall x : Cyl h, C' (coeq (functor_cyl p x))
v: forall x : Cyl h, C' (coeq (functor_cyl q x))

ExtendableAlong 1 pr_cyl ?Goal1
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong 1 h (fun x : B' => u0 x = v0 x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u0 : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u0).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
u: forall x : Cyl h, C' (coeq (functor_cyl p x))
v: forall x : Cyl h, C' (coeq (functor_cyl q x))
ExtendableAlong 1 (fun x : B => pr_cyl (cyl x)) ?Goal1
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong 1 h (fun x : B' => u0 x = v0 x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u0 : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u0).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
u: forall x : Cyl h, C' (coeq (functor_cyl p x))
v: forall x : Cyl h, C' (coeq (functor_cyl q x))

ExtendableAlong 1 pr_cyl ?Goal1
rapply extendable_equiv.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong 1 h (fun x : B' => u0 x = v0 x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u0 : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u0).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
u: forall x : Cyl h, C' (coeq (functor_cyl p x))
v: forall x : Cyl h, C' (coeq (functor_cyl q x))

ExtendableAlong 1 (fun x : B => pr_cyl (cyl x)) ?Goal1
exact (eh (fun x => cglue x # u (cyr x)) (v o cyr)).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong 1 h (fun x : B' => u0 x = v0 x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u0 : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u0).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
u: forall x : Cyl h, C' (coeq (functor_cyl p x))
v: forall x : Cyl h, C' (coeq (functor_cyl q x))

forall b : Cyl h, (fun b0 : Cyl h => (fun x : B' => (fun x0 : B' => transport C (cglue x0) (u (cyr x0))) x = (v o cyr) x) (pr_cyl b0)) b <~> DPath C' (cglue b) (u b) (v b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h

(fun b : Cyl h => (fun x0 : B' => (fun x1 : B' => transport C (cglue x1) (u (cyr x1))) x0 = (v o cyr) x0) (pr_cyl b)) x <~> DPath (C o pr_cylcoeq p q) (cglue x) (u x) (v x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h

transport C (cglue (pr_cyl x)) (u (cyr (pr_cyl x))) = v (cyr (pr_cyl x)) <~> DPath C (ap (pr_cylcoeq p q) (cglue x)) (u x) (v x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h

pr_cylcoeq p q (coeq (functor_cyl p x)) = coeq (f' (pr_cyl x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
pr_cylcoeq p q (coeq (functor_cyl q x)) = coeq (g' (pr_cyl x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
PathSquare.PathSquare (ap (pr_cylcoeq p q) (cglue x)) (cglue (pr_cyl x)) ?p0x ?p1x
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
DPath C ?p0x (u x) (u (cyr (pr_cyl x)))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
DPath C ?p1x (v x) (v (cyr (pr_cyl x)))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h

DPath C (ap coeq (pr_functor_cyl p x)) (u x) (u (cyr (pr_cyl x)))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
DPath C (ap coeq (pr_functor_cyl q x)) (v x) (v (cyr (pr_cyl x)))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h

pr_cylcoeq p q (coeq (functor_cyl p x)) = coeq (f' (pr_cyl x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
?x = ap coeq (pr_functor_cyl p x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
(fun r : pr_cylcoeq p q (coeq (functor_cyl p x)) = coeq (f' (pr_cyl x)) => DPath C r (u x) (u (cyr (pr_cyl x)))) ?x
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
pr_cylcoeq p q (coeq (functor_cyl q x)) = coeq (g' (pr_cyl x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
?x0 = ap coeq (pr_functor_cyl q x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
(fun r : pr_cylcoeq p q (coeq (functor_cyl q x)) = coeq (g' (pr_cyl x)) => DPath C r (v x) (v (cyr (pr_cyl x)))) ?x0
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h

(ap (fun x0 : Cyl h => pr_cylcoeq p q (coeq (functor_cyl p x0))) (eissect pr_cyl x))^ = ap coeq (pr_functor_cyl p x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
pr_cylcoeq p q (coeq (functor_cyl q x)) = coeq (g' (pr_cyl x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
?x = ap coeq (pr_functor_cyl q x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
(fun r : pr_cylcoeq p q (coeq (functor_cyl q x)) = coeq (g' (pr_cyl x)) => DPath C r (v x) (v (cyr (pr_cyl x)))) ?x
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h

(ap (fun x0 : Cyl h => pr_cylcoeq p q (coeq (functor_cyl p x0))) (eissect pr_cyl x))^ = ap coeq (pr_functor_cyl p x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
(ap (fun x0 : Cyl h => pr_cylcoeq p q (coeq (functor_cyl q x0))) (eissect pr_cyl x))^ = ap coeq (pr_functor_cyl q x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h

(ap (fun y : Cyl h => coeq (pr_cyl (functor_cyl p y))) (eissect pr_cyl x))^ = ap coeq (pr_functor_cyl p x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
(ap (fun x0 : Cyl h => pr_cylcoeq p q (coeq (functor_cyl q x0))) (eissect pr_cyl x))^ = ap coeq (pr_functor_cyl q x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h

(ap (fun y : Cyl h => coeq (pr_cyl (functor_cyl p y))) (eissect pr_cyl x))^ = ap coeq (pr_functor_cyl p x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
(ap (fun y : Cyl h => coeq (pr_cyl (functor_cyl q y))) (eissect pr_cyl x))^ = ap coeq (pr_functor_cyl q x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h

ap (fun y : Cyl h => coeq (pr_cyl (functor_cyl p y))) (eissect pr_cyl x)^ = ap coeq (pr_functor_cyl p x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 u0 v0 : forall x0 : B', C (coeq (g' x0)), ExtendableAlong 1 h (fun x0 : B' => u0 x0 = v0 x0)
s: forall x0 : Coeq f g, C (functor_coeq h k p q x0)
s':= fun x0 : Coeq f g => transport C (pr_cyl_cylcoeq p q x0) (s x0): forall x0 : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x0))
ea1:= fun u0 : forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x0 : A' => C (coeq x0)) ek) u0).1: (forall a : A, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x0 : A' => C (coeq x0)) o pr_cyl' k) y
u: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x0))
v: forall x0 : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x0))
x: Cyl h
ap (fun y : Cyl h => coeq (pr_cyl (functor_cyl q y))) (eissect pr_cyl x)^ = ap coeq (pr_functor_cyl q x)
all: exact (ap_compose (fun x => pr_cyl (functor_cyl _ x)) coeq _).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))

ExtensionAlong (cyl_cylcoeq p q) C' s'
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y

ExtensionAlong (cyl_cylcoeq p q) C' s'
(** Now we construct an extension using Coeq-induction, and prove that it *is* an extension also using Coeq-induction. *)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y

forall a : Cyl k, C' (coeq a)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y
forall b : Cyl h, transport C' (cglue b) (?coeq' (functor_cyl p b)) = ?coeq' (functor_cyl q b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y
forall a : A, (fun w : Coeq f g => Coeq_ind C' ?coeq' ?cglue' (cyl_cylcoeq p q w) = s' w) (coeq a)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y
forall b : B, transport (fun w : Coeq f g => Coeq_ind C' ?coeq' ?cglue' (cyl_cylcoeq p q w) = s' w) (cglue b) (?coeq'0 (f b)) = ?coeq'0 (g b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y

forall a : Cyl k, C' (coeq a)
exact (ea1 (s' o coeq)).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y

forall b : Cyl h, transport C' (cglue b) (ea1 (s' o coeq) (functor_cyl p b)) = ea1 (s' o coeq) (functor_cyl q b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y
b: B

DPath C' (cglue (cyl b)) (ea1 (fun x : A => s' (coeq x)) (functor_cyl p (cyl b))) (ea1 (fun x : A => s' (coeq x)) (functor_cyl q (cyl b)))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y
b: B

DPath (fun x : Coeq f g => C' (cyl_cylcoeq p q x)) (cglue b) (ea1 (fun x : A => s' (coeq x)) (functor_cyl p (cyl b))) (ea1 (fun x : A => s' (coeq x)) (functor_cyl q (cyl b)))
exact (apD s' (cglue b)).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y

forall a : A, (fun w : Coeq f g => Coeq_ind C' (ea1 (s' o coeq)) (eb1 (fun y : Cyl h => ea1 (fun x : A => s' (coeq x)) (functor_cyl p y)) (fun y : Cyl h => ea1 (fun x : A => s' (coeq x)) (functor_cyl q y)) (fun b : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b) (apD s' (cglue b)))) (cyl_cylcoeq p q w) = s' w) (coeq a)
intros a; reflexivity.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y

forall b : B, transport (fun w : Coeq f g => Coeq_ind C' (ea1 (s' o coeq)) (eb1 (fun y : Cyl h => ea1 (fun x : A => s' (coeq x)) (functor_cyl p y)) (fun y : Cyl h => ea1 (fun x : A => s' (coeq x)) (functor_cyl q y)) (fun b0 : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b0) (apD s' (cglue b0)))) (cyl_cylcoeq p q w) = s' w) (cglue b) ((fun a : A => 1) (f b)) = (fun a : A => 1) (g b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y
b: B

transport (fun w : Coeq f g => Coeq_ind C' (ea1 (s' o coeq)) (eb1 (fun y : Cyl h => ea1 (fun x : A => s' (coeq x)) (functor_cyl p y)) (fun y : Cyl h => ea1 (fun x : A => s' (coeq x)) (functor_cyl q y)) (fun b0 : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b0) (apD s' (cglue b0)))) (cyl_cylcoeq p q w) = s' w) (cglue b) ((fun a : A => 1) (f b)) = (fun a : A => 1) (g b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y
b: B

DPathSquare (fun x : Coeq f g => C' (cyl_cylcoeq p q x)) (PathSquare.sq_refl_h (cglue b)) (apD (fun x : Coeq f g => Coeq_ind C' (ea1 (fun x0 : A => s' (coeq x0))) (eb1 (fun y : Cyl h => ea1 (fun x0 : A => s' (coeq x0)) (functor_cyl p y)) (fun y : Cyl h => ea1 (fun x0 : A => s' (coeq x0)) (functor_cyl q y)) (fun b0 : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b0) (apD s' (cglue b0)))) (cyl_cylcoeq p q x)) (cglue b)) (apD s' (cglue b)) 1 1
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y
b: B

DPath (fun x : coeq (f b) = coeq (g b) => DPath (fun x0 : Coeq f g => C' (cyl_cylcoeq p q x0)) x (Coeq_ind C' (ea1 (fun x0 : A => s' (coeq x0))) (eb1 (fun y : Cyl h => ea1 (fun x0 : A => s' (coeq x0)) (functor_cyl p y)) (fun y : Cyl h => ea1 (fun x0 : A => s' (coeq x0)) (functor_cyl q y)) (fun b0 : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b0) (apD s' (cglue b0)))) (cyl_cylcoeq p q (coeq (f b)))) (Coeq_ind C' (ea1 (fun x0 : A => s' (coeq x0))) (eb1 (fun y : Cyl h => ea1 (fun x0 : A => s' (coeq x0)) (functor_cyl p y)) (fun y : Cyl h => ea1 (fun x0 : A => s' (coeq x0)) (functor_cyl q y)) (fun b0 : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b0) (apD s' (cglue b0)))) (cyl_cylcoeq p q (coeq (g b))))) 1 (apD (fun x : Coeq f g => Coeq_ind C' (ea1 (fun x0 : A => s' (coeq x0))) (eb1 (fun y : Cyl h => ea1 (fun x0 : A => s' (coeq x0)) (functor_cyl p y)) (fun y : Cyl h => ea1 (fun x0 : A => s' (coeq x0)) (functor_cyl q y)) (fun b0 : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b0) (apD s' (cglue b0)))) (cyl_cylcoeq p q x)) (cglue b)) (apD s' (cglue b))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y
b: B

(dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b))^-1 (apD (Coeq_ind C' (ea1 (fun x : A => s' (coeq x))) (eb1 (fun y : Cyl h => ea1 (fun x : A => s' (coeq x)) (functor_cyl p y)) (fun y : Cyl h => ea1 (fun x : A => s' (coeq x)) (functor_cyl q y)) (fun b0 : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b0) (apD s' (cglue b0))))) (cglue (cyl b))) = apD s' (cglue b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)
s: forall x : Coeq f g, C (functor_coeq h k p q x)
C':= C o pr_cylcoeq p q: CylCoeq p q -> Type
s':= fun x : Coeq f g => transport C (pr_cyl_cylcoeq p q x) (s x): forall x : Coeq f g, C (pr_cylcoeq p q (cyl_cylcoeq p q x))
ea1:= fun u : forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a) => (fst (cyl_extendable' 1 k (fun x : A' => C (coeq x)) ek) u).1: (forall a : A, ((fun x : A' => C (coeq x)) o pr_cyl' k) (cyl a)) -> forall y : Cyl k, ((fun x : A' => C (coeq x)) o pr_cyl' k) y
eb'': forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), ExtendableAlong 1 cyl (fun x : Cyl h => DPath C' (cglue x) (u x) (v x))
eb1:= fun (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))) (w : forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) => (fst (cyl_extendable 1 h (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (eb'' u v)) w).1: forall (u : forall x : Cyl h, C' (coeq (functor_cyl p x))) (v : forall x : Cyl h, C' (coeq (functor_cyl q x))), (forall a : B, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) (cyl a)) -> forall y : Cyl h, (fun x : Cyl h => DPath C' (cglue x) (u x) (v x)) y
b: B

apD (Coeq_ind C' (ea1 (fun x : A => s' (coeq x))) (eb1 (fun y : Cyl h => ea1 (fun x : A => s' (coeq x)) (functor_cyl p y)) (fun y : Cyl h => ea1 (fun x : A => s' (coeq x)) (functor_cyl q y)) (fun b0 : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b0) (apD s' (cglue b0))))) (cglue (cyl b)) = dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b) (apD s' (cglue b))
napply Coeq_ind_beta_cglue. Defined. (** Now we can easily iterate into higher extendability. *)
n: nat
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)

ExtendableAlong n (functor_coeq h k p q) C
n: nat
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 : B' => u x = v x)

ExtendableAlong n (functor_coeq h k p q) C
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u v : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u x = v x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u x = v x)

forall g0 : forall a : Coeq f g, C (functor_coeq h k p q a), ExtensionAlong (functor_coeq h k p q) C g0
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u v : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u x = v x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u x = v x)
forall h0 k0 : forall b : Coeq f' g', C b, ExtendableAlong n (functor_coeq h k p q) (fun b : Coeq f' g' => h0 b = k0 b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u v : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u x = v x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u x = v x)

forall g0 : forall a : Coeq f g, C (functor_coeq h k p q a), ExtensionAlong (functor_coeq h k p q) C g0
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u v : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u x = v x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u x = v x)

ExtendableAlong 1 k (fun x : A' => C (coeq x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u v : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u x = v x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u x = v x)
forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong 1 h (fun x : B' => u x = v x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u v : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u x = v x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u x = v x)

ExtendableAlong 1 k (fun x : A' => C (coeq x))
exact (fst ek , fun _ _ => tt).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u v : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u x = v x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u x = v x)

forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong 1 h (fun x : B' => u x = v x)
exact (fun u v => (fst (eh u v) , fun _ _ => tt)).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u v : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u x = v x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u x = v x)

forall h0 k0 : forall b : Coeq f' g', C b, ExtendableAlong n (functor_coeq h k p q) (fun b : Coeq f' g' => h0 b = k0 b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u0 v0 : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u0 x = v0 x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u0 x = v0 x)
u, v: forall b : Coeq f' g', C b

ExtendableAlong n k (fun x : A' => u (coeq x) = v (coeq x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u0 v0 : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u0 x = v0 x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u0 x = v0 x)
u, v: forall b : Coeq f' g', C b
forall u0 v0 : forall x : B', u (coeq (g' x)) = v (coeq (g' x)), ExtendableAlong n h (fun x : B' => u0 x = v0 x)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u0 v0 : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u0 x = v0 x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u0 x = v0 x)
u, v: forall b : Coeq f' g', C b

ExtendableAlong n k (fun x : A' => u (coeq x) = v (coeq x))
exact (snd ek (u o coeq) (v o coeq)).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
n: nat
IH: forall C0 : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C0 (coeq x)) -> (forall u0 v0 : forall x : B', C0 (coeq (g' x)), ExtendableAlong n h (fun x : B' => u0 x = v0 x)) -> ExtendableAlong n (functor_coeq h k p q) C0
C: Coeq f' g' -> Type
ek: ExtendableAlong n.+1 k (fun x : A' => C (coeq x))
eh: forall u0 v0 : forall x : B', C (coeq (g' x)), ExtendableAlong n.+1 h (fun x : B' => u0 x = v0 x)
u, v: forall b : Coeq f' g', C b

forall u0 v0 : forall x : B', u (coeq (g' x)) = v (coeq (g' x)), ExtendableAlong n h (fun x : B' => u0 x = v0 x)
exact (snd (eh (u o coeq o g') (v o coeq o g'))). Defined. 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 : 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). (** Since extending at level [n.+1] into [C] implies extending at level [n] into path-types of [C], we get the following corollary. *)
n: nat
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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
n: nat
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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
n: nat
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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 k (fun x : A' => C (coeq x))
n: nat
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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')
forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong n h (fun x : B' => u x = v x)
n: nat
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
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')

forall u v : forall x : B', C (coeq (g' x)), ExtendableAlong n h (fun x : B' => u x = v x)
exact (snd eh). Defined. 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).