Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. 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.
(* -*- mode: coq; mode: visual-line -*- *)

(** * Extensions and extendible maps *)

[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Equiv.PathSplit PathAny. 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 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
x: A

gd x = p x <~> 1 = gd x @ (p 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
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'. Global 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 P : B -> Type, ExtendableAlong n f P -> ExtendableAlong n f P
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 P : B -> Type, ExtendableAlong n f P -> ExtendableAlong n f P
P: B -> Type

ExtendableAlong n.+1 f P -> ExtendableAlong n.+1 f P
A, B: Type
f: A -> B
n: nat
IH: forall P : B -> Type, ExtendableAlong n f P -> ExtendableAlong n f P
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 P : B -> Type, ExtendableAlong n f P -> ExtendableAlong n f P
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 P : B -> Type, ExtendableAlong n f P -> ExtendableAlong n f P
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 P : B -> Type, ExtendableAlong n f P -> ExtendableAlong n f P
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 P : B -> Type, ExtendableAlong n f P -> ExtendableAlong n f P
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)
(** Unles we give the universe explicitly here, [kmin] gets collapsed to [k1]. *)
A, B: Type
f: A -> B
n: nat
IH: forall P : B -> Type, ExtendableAlong n f P -> ExtendableAlong n f P
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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C 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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C 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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C 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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C b => g oD f)
C: B -> Type
(forall h k : forall b : B, C b, (fix ExtendableAlong (n : nat) (A B : Type) (f : A -> B) (C : B -> Type) {struct n} : Type := match n with | 0 => Unit | n0.+1 => (forall g : forall a : A, C (f a), ExtensionAlong f C g) * (forall h0 k0 : forall b : B, C b, ExtendableAlong n0 A B f (fun b : B => 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 (n : nat) (A B : Type) (f : A -> B) {struct n} : Type := match n with | 0 => Unit | n0.+1 => (forall a : B, hfiber f a) * (forall x0 y0 : A, PathSplit n0 (x0 = y0) (f x0 = f y0) (ap f)) 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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C 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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C b => g oD f)
C: B -> Type
g: forall a : A, C (f a)

ExtensionAlong f C g <~> hfiber (fun g : forall b : B, C b => g oD f) g
H: Funext
A, B: Type
f: A -> B
n: nat
IHn: forall C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C b => g 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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C b => g oD f)
C: B -> Type

(forall h k : forall b : B, C b, (fix ExtendableAlong (n : nat) (A B : Type) (f : A -> B) (C : B -> Type) {struct n} : Type := match n with | 0 => Unit | n0.+1 => (forall g : forall a : A, C (f a), ExtensionAlong f C g) * (forall h0 k0 : forall b : B, C b, ExtendableAlong n0 A B f (fun b : B => 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 (n : nat) (A B : Type) (f : A -> B) {struct n} : Type := match n with | 0 => Unit | n0.+1 => (forall a : B, hfiber f a) * (forall x0 y0 : A, PathSplit n0 (x0 = y0) (f x0 = f y0) (ap f)) 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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C b => g oD f)
C: B -> Type
h: forall b : B, C b

(forall k : forall b : B, C b, (fix ExtendableAlong (n : nat) (A B : Type) (f : A -> B) (C : B -> Type) {struct n} : Type := match n with | 0 => Unit | n0.+1 => (forall g : forall a : A, C (f a), ExtensionAlong f C g) * (forall h k0 : forall b : B, C b, ExtendableAlong n0 A B f (fun b : B => h 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 (n : nat) (A B : Type) (f : A -> B) {struct n} : Type := match n with | 0 => Unit | n0.+1 => (forall a : B, hfiber f a) * (forall x y0 : A, PathSplit n0 (x = y0) (f x = f y0) (ap f)) 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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C b => g oD f)
C: B -> Type
h, k: forall b : B, C b

(fix ExtendableAlong (n : nat) (A B : Type) (f : A -> B) (C : B -> Type) {struct n} : Type := match n with | 0 => Unit | n0.+1 => (forall g : forall a : A, C (f a), ExtensionAlong f C g) * (forall h k : forall b : B, C b, ExtendableAlong n0 A B f (fun b : B => h b = k b)) end) n A B f (fun b : B => h b = k b) <~> (fix PathSplit (n : nat) (A B : Type) (f : A -> B) {struct n} : Type := match n with | 0 => Unit | n0.+1 => (forall a : B, hfiber f a) * (forall x y : A, PathSplit n0 (x = y) (f x = f y) (ap f)) 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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C 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 (n : nat) (A B : Type) (f : A -> B) {struct n} : Type := match n with | 0 => Unit | n0.+1 => (forall a : B, hfiber f a) * (forall x y : A, PathSplit n0 (x = y) (f x = f y) (ap f)) 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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C b => g oD f)
C: B -> Type
h, k: forall b : B, C b

(fix PathSplit (n : nat) (A B : Type) (f : A -> B) {struct n} : Type := match n with | 0 => Unit | n0.+1 => (forall a : B, hfiber f a) * (forall x y : A, PathSplit n0 (x = y) (f x = f y) (ap f)) 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 C : B -> Type, ExtendableAlong n f C <~> PathSplit n (fun g : forall b : B, C 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 g : forall b : B, C b => g 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 g : forall b : B, C b => g oD f)
g: forall x : A, C (f x)
e:= {| equiv_fun := fun g : forall b : B, C b => g 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 g : forall b : B, C b => g oD f)
g: forall x : A, C (f x)
e:= {| equiv_fun := fun g : forall b : B, C b => g oD f; equiv_isequiv := E |}: (forall b : B, C b) <~> (forall x : A, C (f x))

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

(fun x : A => (fun g : forall b : B, C b => g 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 D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
C, D: B -> Type
g: forall b : B, D b <~> C b
(forall g : forall a : A, D (f a), ExtensionAlong f D g) * (forall h k : forall b : B, D b, ExtendableAlong n f (fun b : B => h b = k b)) -> (forall g : forall a : A, C (f a), ExtensionAlong f C g) * (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 D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
C, D: B -> Type
g: forall b : B, D b <~> C b

(forall g : forall a : A, D (f a), ExtensionAlong f D g) * (forall h k : forall b : B, D b, ExtendableAlong n f (fun b : B => h b = k b)) -> (forall g : forall a : A, C (f a), ExtensionAlong f C g) * (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 D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
C, D: B -> Type
g: forall b : B, D b <~> C b

(forall g : forall a : A, D (f a), ExtensionAlong f D g) -> forall g : forall a : A, C (f a), ExtensionAlong f C g
A, B: Type
f: A -> B
n: nat
IH: forall D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
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 D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
C, D: B -> Type
g: forall b : B, D b <~> C b

(forall g : forall a : A, D (f a), ExtensionAlong f D g) -> forall g : forall a : A, C (f a), ExtensionAlong f C g
A, B: Type
f: A -> B
n: nat
IH: forall D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
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 D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
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 D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
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
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 D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
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 D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
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 D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
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 D C : B -> Type, (forall b : B, C b <~> D b) -> ExtendableAlong n f C -> ExtendableAlong n f D
C, D: B -> Type
g: forall b : B, D b <~> C b
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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))
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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))
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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))
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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
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 P : C -> Type, ExtendableAlong n g P -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n f (fun b : B => P (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))
apply (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 P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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 P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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 P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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 P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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 P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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)
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 P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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)
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 P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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 P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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 P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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 P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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 P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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))
apply (snd extf (h oD g) (k oD g)).
A, B, C: Type
f: A -> B
g: B -> C
n: nat
IHn: forall P : C -> Type, ExtendableAlong n.+1 f (fun b : B => P (g b)) -> ExtendableAlong n (fun x : A => g (f x)) P -> ExtendableAlong n g P
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)
apply (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 C : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C
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 C : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C
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 C : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C
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 C : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C
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 C : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C
C: B -> Type
extf: ExtendableAlong n.+1 f C
h: forall a : A, C (g a)
a: A

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

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

(fst extf (fun a : A => transport C (p a)^ (h a))).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 C : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C
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 C : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C
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 C : B -> Type, ExtendableAlong n f C
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 C : B -> Type, ExtendableAlong n f C
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 C : B -> Type, ExtendableAlong n f C
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 C : B -> Type, ExtendableAlong n f C
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 C : B -> Type, ExtendableAlong n f C
C: B -> Type
h: forall a : A, C (f a)
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 C : B -> Type, ExtendableAlong n f C
C: B -> Type
h: forall a : A, C (f a)
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 C : B -> Type, ExtendableAlong n f C
C: B -> Type
h: forall a : A, C (f a)
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 C : B -> Type, ExtendableAlong n f C
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 C : B -> Type, ExtendableAlong n f C
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 C : B -> Type, (forall b : B, Contr (C b)) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, Contr (C b)) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, Contr (C b)) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, Contr (C b)) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, Contr (C b)) -> ExtendableAlong n f C
C: B -> Type
H: forall b : B, Contr (C b)
h: forall a : A, C (f a)
a: A

center (C (f a)) = h a
apply contr.
A, B: Type
f: A -> B
n: nat
IHn: forall C : B -> Type, (forall b : B, Contr (C b)) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, Contr (C b)) -> ExtendableAlong n f C
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 (C : B -> Type) (h k : forall b : B, C b), ExtendableAlong n.+1 f C -> ExtendableAlong n f (fun b : B => h b = k 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 (C : B -> Type) (h k : forall b : B, C b), ExtendableAlong n.+1 f C -> ExtendableAlong n f (fun b : B => h b = k 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 (C : B -> Type) (h k : forall b : B, C b), ExtendableAlong n.+1 f C -> ExtendableAlong n f (fun b : B => h b = k 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 (C : B -> Type) (h k : forall b : B, C b), ExtendableAlong n.+1 f C -> ExtendableAlong n f (fun b : B => h b = k 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 (C : B -> Type) (h k : forall b : B, C b), ExtendableAlong n.+1 f C -> ExtendableAlong n f (fun b : B => h b = k 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 (C : B -> Type) (h k : forall b : B, C b), ExtendableAlong n.+1 f C -> ExtendableAlong n f (fun b : B => h b = k 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)
refine (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 C : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ExtendableAlong n f C
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))
g: forall a : A, C (f a)
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 C : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ExtendableAlong n f C
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))
g: forall a : A, C (f a)
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 C : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ExtendableAlong n f C
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 C : B -> Type, (forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) -> ExtendableAlong n f C
C: B -> Type
orth: forall b : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))
h, k: forall b : B, C b
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 a : A, C (cyl a)
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 a : A, C (cyl a)
ext: ExtensionAlong cyl C g
a: A
Cyl_ind C g (fun x : B => ext.1 (cyr x)) (fun a : A => ?Goal) (cyl a) = g a
A, B: Type
f: A -> B
C: Cyl f -> Type
g: forall a : A, C (cyl a)
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 a : A, C (cyl a)
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 a : A, C (cyl a)
ext: ExtensionAlong cyl C g
a: A

Cyl_ind C g (fun x : B => ext.1 (cyr x)) (fun a : A => ((ext.2 a)^ @Dl apD ext.1 (cyglue a))%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 C : Cyl f -> Type, ExtendableAlong n cyl C -> ExtendableAlong n cyl C
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 C : Cyl f -> Type, ExtendableAlong n cyl C -> ExtendableAlong n cyl C
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 C : Cyl f -> Type, ExtendableAlong n cyl C -> ExtendableAlong n cyl C
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 C : Cyl f -> Type, ExtendableAlong n cyl C -> ExtendableAlong n cyl C
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 C : Cyl f -> Type, ExtendableAlong n cyl C -> ExtendableAlong n cyl C
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 C : Cyl f -> Type, ExtendableAlong n cyl C -> ExtendableAlong n cyl C
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 C : Cyl f -> Type, ExtendableAlong n cyl C -> ExtendableAlong n cyl C
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' : 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'

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' : 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'

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 b : B => (fst (ef (g b)) (fun a : A => s (a, b))).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 a : A => s (a, 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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 P : A' * B' -> Type, (forall b' : B', ExtendableAlong n f (fun a' : A' => P (a', b'))) -> (forall a' : A', ExtendableAlong n g (fun b' : B' => P (a', b'))) -> ExtendableAlong n (functor_prod f g) P
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 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)
a: A

forall v : Q a, C (a; v)
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)
a: A

forall a0 : P a, C (a; f a a0)
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)
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 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)
a: A
u: P a

(fst (ef a) (fun u : P a => s (a; u))).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 C : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C
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 C : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C
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 C : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C
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 C : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C
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 C : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C
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 C : {x : _ & Q x} -> Type, (forall a : A, ExtendableAlong n (f a) (fun v : Q a => C (a; v))) -> ExtendableAlong n (functor_sigma idmap f) C
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 nonidentity 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 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)
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 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)
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 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)
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 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)
a: A
u: P a

(fst ef (fun a : A => (fst (eg a) (fun u : P a => s (a; u))).1)).1 (f a) (g a u) = 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)
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 C : {x : _ & Q x} -> Type, HomotopyExtendableAlong n f C -> (forall a : A, ExtendableAlong n (g a) (fun v : Q (f a) => C (f a; v))) -> ExtendableAlong n (functor_sigma f g) C
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 P : A' + B' -> Type, ExtendableAlong n f (fun x : A' => P (inl x)) -> ExtendableAlong n g (fun x : B' => P (inr x)) -> ExtendableAlong n (functor_sum f g) P
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 change 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 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
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 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
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 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
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
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 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
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 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
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 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
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 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
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 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
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 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
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 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
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
x: Cyl h

(fun b : Cyl h => (fun x : B' => (fun x0 : B' => transport C (cglue x0) (u (cyr x0))) x = (v o cyr) x) (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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
x: Cyl h

(ap (fun x : Cyl h => pr_cylcoeq p q (coeq (functor_cyl p x))) (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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
x: Cyl h

(ap (fun x : Cyl h => pr_cylcoeq p q (coeq (functor_cyl p x))) (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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
x: Cyl h
(ap (fun x : Cyl h => pr_cylcoeq p q (coeq (functor_cyl q x))) (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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
x: Cyl h
(ap (fun x : Cyl h => pr_cylcoeq p q (coeq (functor_cyl q x))) (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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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)
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
u: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl p x))
v: forall x : Cyl h, (C o pr_cylcoeq p q) (coeq (functor_cyl q x))
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 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) (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 b : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b) (apD s' (cglue b)))) (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 b : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b) (apD s' (cglue b)))) (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 b : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b) (apD s' (cglue b)))) (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 b : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b) (apD s' (cglue b)))) (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 b : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b) (apD s' (cglue b))))) (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 b : B => dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b) (apD s' (cglue b))))) (cglue (cyl b)) = dp_compose' (cyl_cylcoeq p q) C' (ap_cyl_cylcoeq_cglue p q b) (apD s' (cglue b))
nrapply 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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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)
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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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)
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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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)
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 C : Coeq f' g' -> Type, ExtendableAlong n k (fun x : A' => C (coeq x)) -> (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
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)
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).