Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.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.
(** * Extensions and extensible maps *)
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Equiv.PathSplit Homotopy.IdentitySystems.Require Import Cubical.DPath Cubical.DPathSquare.Require Import Colimits.Coeq Colimits.MappingCylinder.LocalOpen Scope nat_scope.LocalOpen 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. *)SectionExtensions.(* 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]. *)DefinitionExtensionAlong@{a b p m} {A : Type@{a}} {B : Type@{b}} (f : A -> B)
(P : B -> Type@{p}) (d : forallx:A, P (f x))
:= (* { s : forall y:B, P y & forall x:A, s (f x) = d x }. *)
sig@{m m} (fun (s : forally:B, P y) => forallx: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: forallx : A, P (f x)
ExtensionAlong f P d -> ExtensionAlong f P d
A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x)
ExtensionAlong f P d -> ExtensionAlong f P d
A, B: Type f: A -> B P: B -> Type d: forallx : 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: forallx : A, P (f x) ext: ExtensionAlong f P d e1:= ext.1: forally : B, P y e2: (funs : forally : B, P y =>
forallx : A, s (f x) = d x) e1
ExtensionAlong f P d
A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) ext: ExtensionAlong f P d e1:= ext.1: forally : B, P y e2: forallx : 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: forallx : A, P (f x) ext, ext': ExtensionAlong f P d
ExtensionAlong f (funy : B => ext.1 y = ext'.1 y)
(funx : A => ext.2 x @ (ext'.2 x)^) <~> ext = ext'
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) ext, ext': ExtensionAlong f P d
ExtensionAlong f (funy : B => ext.1 y = ext'.1 y)
(funx : A => ext.2 x @ (ext'.2 x)^) <~> ext = ext'
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) ext: ExtensionAlong f P d
forallext' : ExtensionAlong f P d,
ExtensionAlong f (funy : B => ext.1 y = ext'.1 y)
(funx : A => ext.2 x @ (ext'.2 x)^) <~> ext = ext'
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) ext: ExtensionAlong f P d
(funb : ExtensionAlong f P d =>
ExtensionAlong f (funy : B => ext.1 y = b.1 y)
(funx : A => ext.2 x @ (b.2 x)^)) ext
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) ext: ExtensionAlong f P d
Contr
{y : ExtensionAlong f P d &
(funb : ExtensionAlong f P d =>
ExtensionAlong f (funy0 : B => ext.1 y0 = b.1 y0)
(funx : A => ext.2 x @ (b.2 x)^)) y}
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) ext: ExtensionAlong f P d
(funb : ExtensionAlong f P d =>
ExtensionAlong f (funy : B => ext.1 y = b.1 y)
(funx : A => ext.2 x @ (b.2 x)^)) ext
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) ext: ExtensionAlong f P d
{s : forally : B, ext.1 y = ext.1 y &
forallx : A, s (f x) = ext.2 x @ (ext.2 x)^}
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) ext: ExtensionAlong f P d
forallx : 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: forallx : A, P (f x) ext: ExtensionAlong f P d
Contr
{y : ExtensionAlong f P d &
(funb : ExtensionAlong f P d =>
ExtensionAlong f (funy0 : B => ext.1 y0 = b.1 y0)
(funx : A => ext.2 x @ (b.2 x)^)) y}
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) g: forally : B, P y gd: forallx : A, g (f x) = d x
Contr
{y
: {s : forally : B, P y &
forallx : A, s (f x) = d x} &
{s : forally0 : B, g y0 = y.1 y0 &
forallx : A, s (f x) = gd x @ (y.2 x)^}}
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) g: forally : B, P y gd: forallx : A, g (f x) = d x
Contr
{y : forallx : A, g (f x) = d x &
forallx : A, 1 = gd x @ (y x)^}
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) g: forally : B, P y gd: forallx : A, g (f x) = d x
{p : (funx : A => g (f x)) == d & gd == p} <~>
{y : forallx : A, g (f x) = d x &
forallx : A, 1 = gd x @ (y x)^}
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) g: forally : B, P y gd: forallx : A, g (f x) = d x
{p : (funx : A => g (f x)) == d & gd == p} <~>
{y : forallx : A, g (f x) = d x &
forallx : A, 1 = gd x @ (y x)^}
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) g: forally : B, P y gd: forallx : A, g (f x) = d x p: (funx : A => g (f x)) == d
gd == p <~> (forallx : A, 1 = gd x @ (p x)^)
H: Funext A, B: Type f: A -> B P: B -> Type d: forallx : A, P (f x) g: forally : B, P y gd: forallx : A, g (f x) = d x p: (funx : 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: forallx : A, P (f x) g: forally : B, P y gd: forallx : A, g (f x) = d x p: (funx : A => g (f x)) == d x: A
p x = gd x <~> 1 = gd x @ (p x)^
symmetry; apply equiv_moveR_1M.Defined.Definitionpath_extension `{Funext} {A B : Type} {f : A -> B}
{P : B -> Type} {d : forallx:A, P (f x)}
(ext ext' : ExtensionAlong f P d)
: (ExtensionAlong f
(funy => pr1 ext y = pr1 ext' y)
(funx => pr2 ext x @ (pr2 ext' x)^))
-> ext = ext'
:= equiv_path_extension ext ext'.#[export] Instanceisequiv_path_extension `{Funext} {A B : Type} {f : A -> B}
{P : B -> Type} {d : forallx:A, P (f x)}
(ext ext' : ExtensionAlong f P d)
: IsEquiv (path_extension ext ext') | 0
:= equiv_isequiv _.(** Here is the iterated version. *)FixpointExtendableAlong@{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 : foralla, C (f a)),
ExtensionAlong@{i j k l} f C g) *
forall (hk : forallb, C b),
ExtendableAlong n f (funb => 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) *)GlobalArguments 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: forallP : 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: forallP : 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: forallP : B -> Type,
ExtendableAlong n f P -> ExtendableAlong n f P P: B -> Type ext: ExtendableAlong n.+1 f P
forallg : foralla : A, P (f a), ExtensionAlong f P g
A, B: Type f: A -> B n: nat IH: forallP : B -> Type,
ExtendableAlong n f P -> ExtendableAlong n f P P: B -> Type ext: ExtendableAlong n.+1 f P
forallhk : forallb : B, P b,
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IH: forallP : B -> Type,
ExtendableAlong n f P -> ExtendableAlong n f P P: B -> Type ext: ExtendableAlong n.+1 f P
forallg : foralla : A, P (f a), ExtensionAlong f P g
A, B: Type f: A -> B n: nat IH: forallP : B -> Type,
ExtendableAlong n f P -> ExtendableAlong n f P P: B -> Type ext: ExtendableAlong n.+1 f P
forallhk : forallb : B, P b,
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IH: forallP : B -> Type,
ExtendableAlong n f P -> ExtendableAlong n f P P: B -> Type ext: ExtendableAlong n.+1 f P h, k: forallb : B, P b
ExtendableAlong n f (funb : B => h b = k b)
(** Unless we give the universe explicitly here, [kmin] gets collapsed to [k1]. *)
A, B: Type f: A -> B n: nat IH: forallP : B -> Type,
ExtendableAlong n f P -> ExtendableAlong n f P P: B -> Type ext: ExtendableAlong n.+1 f P h, k: forallb : B, P b P':= (funb : B => h b = k b) : B -> Type: B -> Type
ExtendableAlong n f (funb : 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 (fung : forallb : 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 (fung : forallb : B, C b => g oD f)
H: Funext A, B: Type f: A -> B C: B -> Type
ExtendableAlong 0 f C <~>
PathSplit 0 (fung : forallb : B, C b => g oD f)
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type
ExtendableAlong n.+1 f C <~>
PathSplit n.+1 (fung : forallb : B, C b => g oD f)
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type
ExtendableAlong n.+1 f C <~>
PathSplit n.+1 (fung : forallb : B, C b => g oD f)
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type
(forallg : foralla : A, C (f a),
ExtensionAlong f C g) <~>
(foralla : forallx : A, C (f x),
hfiber (fung : forallb : B, C b => g oD f) a)
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type
(forallhk : forallb : 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 =>
(forallg : foralla : A, C (f a),
ExtensionAlong f C g) *
(forallh0k0 : forallb : B, C b,
ExtendableAlong n0 A B f
(funb : B => h0 b = k0 b))
end) n A B f (funb : B => h b = k b)) <~>
(forallxy : forallb : B, C b,
(fix PathSplit
(n : nat) (A B : Type) (f : A -> B) {struct n} :
Type :=
match n with
| 0 => Unit
| n0.+1 =>
(foralla : B, hfiber f a) *
(forallx0y0 : A,
PathSplit n0 (x0 = y0) (f x0 = f y0) (ap f))
end) n (x = y) (x oD f = y oD f)
(ap (fung : forallb : B, C b => g oD f)))
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type
(forallg : foralla : A, C (f a),
ExtensionAlong f C g) <~>
(foralla : forallx : A, C (f x),
hfiber (fung : forallb : B, C b => g oD f) a)
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type g: foralla : A, C (f a)
ExtensionAlong f C g <~>
hfiber (fung : forallb : B, C b => g oD f) g
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type g: foralla : A, C (f a) rec: forally : B, C y
(forallx : 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: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type
(forallhk : forallb : 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 =>
(forallg : foralla : A, C (f a),
ExtensionAlong f C g) *
(forallh0k0 : forallb : B, C b,
ExtendableAlong n0 A B f
(funb : B => h0 b = k0 b))
end) n A B f (funb : B => h b = k b)) <~>
(forallxy : forallb : B, C b,
(fix PathSplit
(n : nat) (A B : Type) (f : A -> B) {struct n} :
Type :=
match n with
| 0 => Unit
| n0.+1 =>
(foralla : B, hfiber f a) *
(forallx0y0 : A,
PathSplit n0 (x0 = y0) (f x0 = f y0) (ap f))
end) n (x = y) (x oD f = y oD f)
(ap (fung : forallb : B, C b => g oD f)))
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type h: forallb : B, C b
(forallk : forallb : 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 =>
(forallg : foralla : A, C (f a),
ExtensionAlong f C g) *
(forallhk0 : forallb : B, C b,
ExtendableAlong n0 A B f
(funb : B => h b = k0 b))
end) n A B f (funb : B => 1%equiv h b = k b)) <~>
(forally : forallb : B, C b,
(fix PathSplit
(n : nat) (A B : Type) (f : A -> B) {struct n} :
Type :=
match n with
| 0 => Unit
| n0.+1 =>
(foralla : B, hfiber f a) *
(forallxy0 : A,
PathSplit n0 (x = y0) (f x = f y0) (ap f))
end) n (h = y) (h oD f = y oD f)
(ap (fung : forallb : B, C b => g oD f)))
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type h, k: forallb : 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 =>
(forallg : foralla : A, C (f a),
ExtensionAlong f C g) *
(forallhk : forallb : B, C b,
ExtendableAlong n0 A B f
(funb : B => h b = k b))
end) n A B f (funb : 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 =>
(foralla : B, hfiber f a) *
(forallxy : A,
PathSplit n0 (x = y) (f x = f y) (ap f))
end) n (h = k) (h oD f = k oD f)
(ap (fung : forallb : B, C b => g oD f))
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type h, k: forallb : B, C b
PathSplit n
(fung : forallb : 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 =>
(foralla : B, hfiber f a) *
(forallxy : A,
PathSplit n0 (x = y) (f x = f y) (ap f))
end) n (h = k) (h oD f = k oD f)
(ap (fung : forallb : B, C b => g oD f))
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type h, k: forallb : B, C b
(fix PathSplit
(n : nat) (A B : Type) (f : A -> B) {struct n} :
Type :=
match n with
| 0 => Unit
| n0.+1 =>
(foralla : B, hfiber f a) *
(forallxy : A,
PathSplit n0 (x = y) (f x = f y) (ap f))
end) n (h = k) (h oD f = k oD f)
(ap (fung : forallb : B, C b => g oD f)) <~>
PathSplit n
(fung : forallb : B, h b = k b => g oD f)
H: Funext A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C <~> PathSplit n (fung : forallb : B, C b => g oD f) C: B -> Type h, k: forallb : B, C b
(funx : h = k => equiv_apD10 C h k x oD f) ==
(funx : h = k =>
equiv_apD10 (funx0 : A => C (f x0)) (h oD f)
(k oD f)
(ap (fung : forallb : B, C b => g oD f) x))
intros []; reflexivity.Defined.Definitionisequiv_extendable `{Funext} (n : nat)
{A B : Type} {C : B -> Type} {f : A -> B}
: ExtendableAlong n.+2 f C
-> IsEquiv (fung => 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 (fung : forallb : 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 (fung : forallb : 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 (fung : forallb : 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 (fung : forallb : B, C b => g oD f) <~>
IsEquiv (fung : forallb : 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 (fung : forallb : B, C b => g oD f) ->
forallg : forallx : A, C (f x), ExtensionAlong f C g
A, B: Type f: A -> B C: B -> Type
IsEquiv (fung : forallb : B, C b => g oD f) ->
forallg : forallx : A, C (f x), ExtensionAlong f C g
A, B: Type f: A -> B C: B -> Type E: IsEquiv (fung : forallb : B, C b => g oD f) g: forallx : A, C (f x)
ExtensionAlong f C g
A, B: Type f: A -> B C: B -> Type E: IsEquiv (fung : forallb : B, C b => g oD f) g: forallx : A, C (f x) e:= {|
equiv_fun := fung : forallb : B, C b => g oD f;
equiv_isequiv := E
|}: (forallb : B, C b) <~> (forallx : A, C (f x))
ExtensionAlong f C g
A, B: Type f: A -> B C: B -> Type E: IsEquiv (fung : forallb : B, C b => g oD f) g: forallx : A, C (f x) e:= {|
equiv_fun := fung : forallb : B, C b => g oD f;
equiv_isequiv := E
|}: (forallb : B, C b) <~> (forallx : A, C (f x))
forallx : A,
(fung : forallb : B, C b => g oD f)^-1 g (f x) = g x
A, B: Type f: A -> B C: B -> Type E: IsEquiv (fung : forallb : B, C b => g oD f) g: forallx : A, C (f x) e:= {|
equiv_fun := fung : forallb : B, C b => g oD f;
equiv_isequiv := E
|}: (forallb : B, C b) <~> (forallx : A, C (f x))
(funx : A =>
(fung : forallb : 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: forallb : 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: forallb : B, C b <~> D b
ExtendableAlong n f C -> ExtendableAlong n f D
n: nat A, B: Type f: A -> B
forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D
A, B: Type f: A -> B C, D: B -> Type g: forallb : B, D b <~> C b
Unit -> Unit
A, B: Type f: A -> B n: nat IH: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b
(forallg : foralla : A, D (f a),
ExtensionAlong f D g) *
(forallhk : forallb : B, D b,
ExtendableAlong n f (funb : B => h b = k b)) ->
(forallg : foralla : A, C (f a),
ExtensionAlong f C g) *
(forallhk : forallb : B, C b,
ExtendableAlong n f (funb : B => h b = k b))
A, B: Type f: A -> B n: nat IH: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b
(forallg : foralla : A, D (f a),
ExtensionAlong f D g) *
(forallhk : forallb : B, D b,
ExtendableAlong n f (funb : B => h b = k b)) ->
(forallg : foralla : A, C (f a),
ExtensionAlong f C g) *
(forallhk : forallb : B, C b,
ExtendableAlong n f (funb : B => h b = k b))
A, B: Type f: A -> B n: nat IH: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b
(forallg : foralla : A, D (f a),
ExtensionAlong f D g) ->
forallg : foralla : A, C (f a), ExtensionAlong f C g
A, B: Type f: A -> B n: nat IH: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b
(forallhk : forallb : B, D b,
ExtendableAlong n f (funb : B => h b = k b)) ->
forallhk : forallb : B, C b,
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IH: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b
(forallg : foralla : A, D (f a),
ExtensionAlong f D g) ->
forallg : foralla : A, C (f a), ExtensionAlong f C g
A, B: Type f: A -> B n: nat IH: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b h: foralla : A, C (f a)
ExtensionAlong f D
(functor_forall idmap (funa : A => (g (f a))^-1) h) ->
ExtensionAlong f C h
A, B: Type f: A -> B n: nat IH: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b h: foralla : A, C (f a) k: foralla : B, D a
(forallx : A,
k (f x) =
functor_forall idmap (funa : A => (g (f a))^-1) h x) ->
forallx : A,
functor_forall idmap (funb : B => g b) k (f x) = h x
A, B: Type f: A -> B n: nat IH: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b h: foralla : A, C (f a) k: foralla : 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: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b
(forallhk : forallb : B, D b,
ExtendableAlong n f (funb : B => h b = k b)) ->
forallhk : forallb : B, C b,
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IH: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b h: foralla : B, C a
(forallk : forallb : B, D b,
ExtendableAlong n f
(funb : B =>
functor_forall idmap (funb0 : B => (g b0)^-1) h b =
k b)) ->
forallk : forallb : B, C b,
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IH: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b h, k: foralla : B, C a
ExtendableAlong n f
(funb : B => (g b)^-1 (h b) = (g b)^-1 (k b)) ->
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IH: forallDC : B -> Type,
(forallb : B, C b <~> D b) ->
ExtendableAlong n f C -> ExtendableAlong n f D C, D: B -> Type g: forallb : B, D b <~> C b h, k: foralla : 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.Definitionextendable_postcompose (n : nat)
{AB : Type} (CD : B -> Type) (f : A -> B)
(g : forallb, C b -> D b) `{forallb, IsEquiv (g b)}
: ExtendableAlong n f C -> ExtendableAlong n f D
:= extendable_postcompose' n C D f (funb => 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 (funb : 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 (funb : B => P (g b)) ->
ExtendableAlong n (g o f) P
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b))
forallg0 : foralla : A, P (g (f a)),
ExtensionAlong (funx : A => g (f x)) P g0
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b))
forallhk : forallb : C, P b,
ExtendableAlong n (funx : A => g (f x))
(funb : C => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b))
forallg0 : foralla : A, P (g (f a)),
ExtensionAlong (funx : A => g (f x)) P g0
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b)) h: foralla : A, P (g (f a))
ExtensionAlong (funx : A => g (f x)) P h
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b)) h: foralla : 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: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b)) h: foralla : 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: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b))
forallhk : forallb : C, P b,
ExtendableAlong n (funx : A => g (f x))
(funb : C => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b)) h, k: forallb : C, P b
ExtendableAlong n (funx : A => g (f x))
(funb : C => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b)) h, k: forallb : C, P b
ExtendableAlong n g (funb : C => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b)) h, k: forallb : C, P b
ExtendableAlong n f (funb : B => h (g b) = k (g b))
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b)) h, k: forallb : C, P b
ExtendableAlong n g (funb : C => h b = k b)
exact (snd extg h k).
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P P: C -> Type extg: ExtendableAlong n.+1 g P extf: ExtendableAlong n.+1 f (funb : B => P (g b)) h, k: forallb : C, P b
ExtendableAlong n f (funb : 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 (funb : 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 (funb : B => P (g b))
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P
forallg0 : foralla : A, P (g (f a)),
ExtensionAlong f (funb : B => P (g b)) g0
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P
forallhk : forallb : B, P (g b),
ExtendableAlong n f (funb : B => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P
forallg0 : foralla : A, P (g (f a)),
ExtensionAlong f (funb : B => P (g b)) g0
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h: foralla : A, P (g (f a))
ExtensionAlong f (funb : B => P (g b)) h
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h: foralla : 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: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P
forallhk : forallb : B, P (g b),
ExtendableAlong n f (funb : B => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : B, P (g b)
ExtendableAlong n f (funb : B => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : B, P (g b) h':= (fst extg h).1: forally : C, P y
ExtendableAlong n f (funb : B => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : B, P (g b) h':= (fst extg h).1: forally : C, P y k':= (fst extg k).1: forally : C, P y
ExtendableAlong n f (funb : B => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : B, P (g b) h':= (fst extg h).1: forally : C, P y k':= (fst extg k).1: forally : C, P y
forallb : B, h' (g b) = k' (g b) <~> h b = k b
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : B, P (g b) h':= (fst extg h).1: forally : C, P y k':= (fst extg k).1: forally : C, P y
ExtendableAlong n f (funb : B => h' (g b) = k' (g b))
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : B, P (g b) h':= (fst extg h).1: forally : C, P y k':= (fst extg k).1: forally : C, P y
forallb : B, h' (g b) = k' (g b) <~> h b = k b
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : B, P (g b) h':= (fst extg h).1: forally : C, P y k':= (fst extg k).1: forally : C, P y b: B
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n g P ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n f (funb : B => P (g b)) P: C -> Type extg: ExtendableAlong n.+1 g P extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : B, P (g b) h':= (fst extg h).1: forally : C, P y k':= (fst extg k).1: forally : C, P y
ExtendableAlong n f (funb : B => h' (g b) = k' (g b))
exact (IHn (func => 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 (funb : 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 (funb : 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: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P -> ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P
forallg0 : foralla : B, P (g a),
ExtensionAlong g P g0
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P
forallhk : forallb : C, P b,
ExtendableAlong n g (funb : C => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P -> ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P
forallg0 : foralla : B, P (g a),
ExtensionAlong g P g0
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P -> ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h: foralla : B, P (g a)
ExtensionAlong g P h
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P -> ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h: foralla : 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: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P -> ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h: foralla : 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: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P -> ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P
forallhk : forallb : C, P b,
ExtendableAlong n g (funb : C => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P -> ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : C, P b
ExtendableAlong n g (funb : C => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P -> ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : C, P b
ExtendableAlong n.+1 f
(funb : B => h (g b) = k (g b))
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P ->
ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : C, P b
ExtendableAlong n (funx : A => g (f x))
(funb : C => h b = k b)
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P -> ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : C, P b
ExtendableAlong n.+1 f
(funb : B => h (g b) = k (g b))
exact (snd extf (h oD g) (k oD g)).
A, B, C: Type f: A -> B g: B -> C n: nat IHn: forallP : C -> Type,
ExtendableAlong n.+1 f (funb : B => P (g b)) ->
ExtendableAlong n (funx : A => g (f x)) P -> ExtendableAlong n g P P: C -> Type extf: ExtendableAlong n.+2 f (funb : B => P (g b)) extgf: ExtendableAlong n.+1 (funx : A => g (f x)) P h, k: forallb : C, P b
ExtendableAlong n (funx : A => g (f x))
(funb : C => h b = k b)
exact (snd extgf h k).Defined.(** And transfer across homotopies *)
n: nat A, B: Type C: B -> Type f, g: A -> B p: f == g
ExtendableAlong n f C -> ExtendableAlong n g C
n: nat A, B: Type C: B -> Type f, g: A -> B p: f == g
ExtendableAlong n f C -> ExtendableAlong n g C
A, B: Type f, g: A -> B p: f == g n: nat IHn: forallC : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C C: B -> Type extf: ExtendableAlong n.+1 f C
forallg0 : foralla : A, C (g a),
ExtensionAlong g C g0
A, B: Type f, g: A -> B p: f == g n: nat IHn: forallC : B -> Type,
ExtendableAlong n f C -> ExtendableAlong n g C C: B -> Type extf: ExtendableAlong n.+1 f C
forallhk : forallb : B, C b,
ExtendableAlong n g (funb : B => h b = k b)
A, B: Type f, g: A -> B p: f == g n: nat IHn: forallC : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C C: B -> Type extf: ExtendableAlong n.+1 f C
forallg0 : foralla : A, C (g a),
ExtensionAlong g C g0
A, B: Type f, g: A -> B p: f == g n: nat IHn: forallC : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C C: B -> Type extf: ExtendableAlong n.+1 f C h: foralla : A, C (g a)
ExtensionAlong g C h
A, B: Type f, g: A -> B p: f == g n: nat IHn: forallC : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C C: B -> Type extf: ExtendableAlong n.+1 f C h: foralla : A, C (g a) a: A
(fst extf (funa : 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: forallC : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C C: B -> Type extf: ExtendableAlong n.+1 f C h: foralla : A, C (g a) a: A
transport C (p a)
((fst extf (funa : 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: forallC : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C C: B -> Type extf: ExtendableAlong n.+1 f C h: foralla : A, C (g a) a: A
(fst extf (funa : A => transport C (p a)^ (h a))).1
(f a) = transport C (p a)^ (h a)
exact ((fst extf (funa => (p a)^ # h a)).2 a).
A, B: Type f, g: A -> B p: f == g n: nat IHn: forallC : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C C: B -> Type extf: ExtendableAlong n.+1 f C
forallhk : forallb : B, C b,
ExtendableAlong n g (funb : B => h b = k b)
A, B: Type f, g: A -> B p: f == g n: nat IHn: forallC : B -> Type, ExtendableAlong n f C -> ExtendableAlong n g C C: B -> Type extf: ExtendableAlong n.+1 f C h, k: forallb : B, C b
ExtendableAlong n g (funb : 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: forallC : B -> Type, ExtendableAlong n f C C: B -> Type
forallg : foralla : A, C (f a), ExtensionAlong f C g
A, B: Type f: A -> B H: IsEquiv f n: nat IHn: forallC : B -> Type, ExtendableAlong n f C C: B -> Type
forallhk : forallb : B, C b,
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B H: IsEquiv f n: nat IHn: forallC : B -> Type, ExtendableAlong n f C C: B -> Type
forallg : foralla : A, C (f a), ExtensionAlong f C g
A, B: Type f: A -> B H: IsEquiv f n: nat IHn: forallC : B -> Type, ExtendableAlong n f C C: B -> Type h: foralla : A, C (f a)
ExtensionAlong f C h
A, B: Type f: A -> B H: IsEquiv f n: nat IHn: forallC : B -> Type, ExtendableAlong n f C C: B -> Type h: foralla : 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: forallC : B -> Type, ExtendableAlong n f C C: B -> Type h: foralla : 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: forallC : B -> Type, ExtendableAlong n f C C: B -> Type h: foralla : A, C (f a) a: A
transport (funx : 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: forallC : B -> Type, ExtendableAlong n f C C: B -> Type
forallhk : forallb : B, C b,
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B H: IsEquiv f n: nat IHn: forallC : B -> Type, ExtendableAlong n f C C: B -> Type h, k: forallb : B, C b
ExtendableAlong n f (funb : B => h b = k b)
apply IHn.Defined.(** And into contractible types *)
n: nat A, B: Type C: B -> Type f: A -> B H: forallb : B, Contr (C b)
ExtendableAlong n f C
n: nat A, B: Type C: B -> Type f: A -> B H: forallb : B, Contr (C b)
ExtendableAlong n f C
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type, (forallb : B, Contr (C b)) -> ExtendableAlong n f C C: B -> Type H: forallb : B, Contr (C b)
forallg : foralla : A, C (f a), ExtensionAlong f C g
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type, (forallb : B, Contr (C b)) -> ExtendableAlong n f C C: B -> Type H: forallb : B, Contr (C b)
forallhk : forallb : B, C b,
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type, (forallb : B, Contr (C b)) -> ExtendableAlong n f C C: B -> Type H: forallb : B, Contr (C b)
forallg : foralla : A, C (f a), ExtensionAlong f C g
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type, (forallb : B, Contr (C b)) -> ExtendableAlong n f C C: B -> Type H: forallb : B, Contr (C b) h: foralla : A, C (f a)
ExtensionAlong f C h
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type, (forallb : B, Contr (C b)) -> ExtendableAlong n f C C: B -> Type H: forallb : B, Contr (C b) h: foralla : A, C (f a) a: A
center (C (f a)) = h a
apply contr.
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type, (forallb : B, Contr (C b)) -> ExtendableAlong n f C C: B -> Type H: forallb : B, Contr (C b)
forallhk : forallb : B, C b,
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type, (forallb : B, Contr (C b)) -> ExtendableAlong n f C C: B -> Type H: forallb : B, Contr (C b) h, k: forallb : B, C b
ExtendableAlong n f (funb : 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: forallb : B, C b
ExtendableAlong n.+1 f C ->
ExtendableAlong n f (funb : B => h b = k b)
n: nat A, B: Type C: B -> Type f: A -> B h, k: forallb : B, C b
ExtendableAlong n.+1 f C ->
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IHn: forall (C : B -> Type) (hk : forallb : B, C b),
ExtendableAlong n.+1 f C -> ExtendableAlong n f (funb : B => h b = k b) C: B -> Type h, k: forallb : B, C b ext: ExtendableAlong n.+2 f C
forallg : foralla : A, h (f a) = k (f a),
ExtensionAlong f (funb : B => h b = k b) g
A, B: Type f: A -> B n: nat IHn: forall (C : B -> Type) (hk : forallb : B, C b),
ExtendableAlong n.+1 f C -> ExtendableAlong n f (funb : B => h b = k b) C: B -> Type h, k: forallb : B, C b ext: ExtendableAlong n.+2 f C
forallh0k0 : forallb : B, h b = k b,
ExtendableAlong n f (funb : B => h0 b = k0 b)
A, B: Type f: A -> B n: nat IHn: forall (C : B -> Type) (hk : forallb : B, C b),
ExtendableAlong n.+1 f C -> ExtendableAlong n f (funb : B => h b = k b) C: B -> Type h, k: forallb : B, C b ext: ExtendableAlong n.+2 f C
forallg : foralla : A, h (f a) = k (f a),
ExtensionAlong f (funb : B => h b = k b) g
A, B: Type f: A -> B n: nat IHn: forall (C : B -> Type) (hk : forallb : B, C b),
ExtendableAlong n.+1 f C -> ExtendableAlong n f (funb : B => h b = k b) C: B -> Type h, k: forallb : B, C b ext: ExtendableAlong n.+2 f C p: foralla : A, h (f a) = k (f a)
ExtensionAlong f (funb : 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) (hk : forallb : B, C b),
ExtendableAlong n.+1 f C -> ExtendableAlong n f (funb : B => h b = k b) C: B -> Type h, k: forallb : B, C b ext: ExtendableAlong n.+2 f C
forallh0k0 : forallb : B, h b = k b,
ExtendableAlong n f (funb : B => h0 b = k0 b)
A, B: Type f: A -> B n: nat IHn: forall (C : B -> Type) (hk : forallb : B, C b),
ExtendableAlong n.+1 f C -> ExtendableAlong n f (funb : B => h b = k b) C: B -> Type h, k: forallb : B, C b ext: ExtendableAlong n.+2 f C p, q: forallb : B, h b = k b
ExtendableAlong n f (funb : B => p b = q b)
apply IHn, ext.Defined.(** And the oo-version. *)DefinitionooExtendableAlong@{i j k l}
{A : Type@{i}} {B : Type@{j}}
(f : A -> B) (C : B -> Type@{k}) : Type@{l}
:= foralln : nat, ExtendableAlong@{i j k l} n f C.(** Universe parameters are the same as for [ExtendableAlong]. *)GlobalArguments ooExtendableAlong {A B}%_type_scope (f C)%_function_scope.(** Universe modification. *)Definitionlift_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
:= funextn => 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. *)Definitionisequiv_ooextendable `{Funext}
{A B : Type} (C : B -> Type) (f : A -> B)
: ooExtendableAlong f C -> IsEquiv (fung => g oD f)
:= funps => 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 (fung : forallb : B, C b => g oD f)
H: Funext A, B: Type C: B -> Type f: A -> B
ooExtendableAlong f C <~>
ooPathSplit (fung : forallb : 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 (fung : forallb : B, C b => g oD f)
apply equiv_extendable_pathsplit.Defined.
H: Funext A, B: Type C: B -> Type f: A -> B
IsHProp (ooExtendableAlong f C)
H: Funext A, B: Type C: B -> Type f: A -> B
IsHProp (ooExtendableAlong f C)
exact (istrunc_equiv_istrunc _ (equiv_ooextendable_pathsplit C f)^-1).Defined.Definitionequiv_ooextendable_isequiv `{Funext}
{A B : Type} (C : B -> Type) (f : A -> B)
: ooExtendableAlong f C
<~> IsEquiv (fun (g : forallb, C b) => g oD f)
:= equiv_oopathsplit_isequiv _ oE equiv_ooextendable_pathsplit _ _.Definitionooextendable_postcompose
{AB : Type} (CD : B -> Type) (f : A -> B)
(g : forallb, C b -> D b) `{forallb, IsEquiv (g b)}
: ooExtendableAlong f C -> ooExtendableAlong f D
:= funpppn => extendable_postcompose n C D f g (ppp n).Definitionooextendable_postcompose'
{AB : Type} (CD : B -> Type) (f : A -> B)
(g : forallb, C b <~> D b)
: ooExtendableAlong f C -> ooExtendableAlong f D
:= funpppn => extendable_postcompose' n C D f g (ppp n).Definitionooextendable_compose
{ABC : Type} (P : C -> Type) (f : A -> B) (g : B -> C)
: ooExtendableAlong g P -> ooExtendableAlong f (funb => P (g b)) -> ooExtendableAlong (g o f) P
:= funextgextfn => extendable_compose n P f g (extg n) (extf n).DefinitioncancelL_ooextendable
{ABC : Type} (P : C -> Type) (f : A -> B) (g : B -> C)
: ooExtendableAlong g P -> ooExtendableAlong (g o f) P -> ooExtendableAlong f (funb => P (g b))
:= funextgextgfn => cancelL_extendable n P f g (extg n) (extgf n).DefinitioncancelR_ooextendable
{ABC : Type} (P : C -> Type) (f : A -> B) (g : B -> C)
: ooExtendableAlong f (funb => P (g b)) -> ooExtendableAlong (g o f) P -> ooExtendableAlong g P
:= funextfextgfn => cancelR_extendable n P f g (extf n.+1) (extgf n).Definitionooextendable_homotopic
{AB : Type} (C : B -> Type) (f : A -> B) {g : A -> B} (p : f == g)
: ooExtendableAlong f C -> ooExtendableAlong g C
:= funextfn => extendable_homotopic n C f p (extf n).Definitionooextendable_equiv
{AB : Type} (C : B -> Type) (f : A -> B) `{IsEquiv _ _ f}
: ooExtendableAlong f C
:= funn => extendable_equiv n C f.Definitionooextendable_contr
{AB : Type} (C : B -> Type) (f : A -> B)
`{forallb, Contr (C b)}
: ooExtendableAlong f C
:= funn => extendable_contr n C f.
A, B: Type C: B -> Type f: A -> B h, k: forallb : B, C b
ooExtendableAlong f C ->
ooExtendableAlong f (funb : B => h b = k b)
A, B: Type C: B -> Type f: A -> B h, k: forallb : B, C b
ooExtendableAlong f C ->
ooExtendableAlong f (funb : 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
(forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b))) -> ooExtendableAlong f C
A, B: Type f: A -> B C: B -> Type
(forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b))) -> ooExtendableAlong f C
A, B: Type f: A -> B n: nat
forallC : B -> Type,
(forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b))) -> ExtendableAlong n f C
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
(forallb : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) ->
ExtendableAlong n f C C: B -> Type orth: forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b))
forallg : foralla : A, C (f a), ExtensionAlong f C g
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
(forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b))) ->
ExtendableAlong n f C C: B -> Type orth: forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b))
forallhk : forallb : B, C b,
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
(forallb : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) ->
ExtendableAlong n f C C: B -> Type orth: forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b))
forallg : foralla : A, C (f a), ExtensionAlong f C g
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
(forallb : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) ->
ExtendableAlong n f C C: B -> Type orth: forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b)) g: foralla : A, C (f a)
ExtensionAlong f C g
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
(forallb : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) ->
ExtendableAlong n f C C: B -> Type orth: forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b)) g: foralla : A, C (f a)
forallx : A,
(fst (orth (f x) 1)
(funx0 : hfiber f (f x) =>
transport C x0.2 (g x0.1))).1 tt = g x
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
(forallb : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) ->
ExtendableAlong n f C C: B -> Type orth: forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b)) g: foralla : A, C (f a) a: A
(fst (orth (f a) 1)
(funx : hfiber f (f a) => transport C x.2 (g x.1))).1
tt = g a
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
(forallb : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) ->
ExtendableAlong n f C C: B -> Type orth: forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b)) g: foralla : A, C (f a) a: A
(fst (orth (f a) 1)
(funx : 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: forallC : B -> Type,
(forallb : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) ->
ExtendableAlong n f C C: B -> Type orth: forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b))
forallhk : forallb : B, C b,
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
(forallb : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) ->
ExtendableAlong n f C C: B -> Type orth: forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b)) h, k: forallb : B, C b
ExtendableAlong n f (funb : B => h b = k b)
A, B: Type f: A -> B n: nat IHn: forallC : B -> Type,
(forallb : B, ooExtendableAlong (const_tt (hfiber f b)) (unit_name (C b))) ->
ExtendableAlong n f C C: B -> Type orth: forallb : B,
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (C b)) h, k: forallb : B, C b b: B
ooExtendableAlong (const_tt (hfiber f b))
(unit_name (h b = k b))
apply ooextendable_homotopy, orth.Defined.EndExtensions.(** ** 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: foralla : A, C (cyl a) ext: ExtensionAlong cyl C g
ExtensionAlong cyl C g
A, B: Type f: A -> B C: Cyl f -> Type g: foralla : A, C (cyl a) ext: ExtensionAlong cyl C g
ExtensionAlong cyl C g
A, B: Type f: A -> B C: Cyl f -> Type g: foralla : 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: foralla : A, C (cyl a) ext: ExtensionAlong cyl C g a: A
Cyl_ind C g (funx : B => ext.1 (cyr x))
(funa : A => ?Goal) (cyl a) = g a
A, B: Type f: A -> B C: Cyl f -> Type g: foralla : 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: foralla : 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: foralla : A, C (cyl a) ext: ExtensionAlong cyl C g a: A
Cyl_ind C g (funx : B => ext.1 (cyr x))
(funa : 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: forallC : Cyl f -> Type,
ExtendableAlong n cyl C ->
ExtendableAlong n cyl C C: Cyl f -> Type ext: ExtendableAlong n.+1 cyl C
forallg : foralla : A, C (cyl a),
ExtensionAlong cyl C g
A, B: Type f: A -> B n: nat IH: forallC : Cyl f -> Type,
ExtendableAlong n cyl C ->
ExtendableAlong n cyl C C: Cyl f -> Type ext: ExtendableAlong n.+1 cyl C
forallhk : forallb : Cyl f, C b,
ExtendableAlong n cyl (funb : Cyl f => h b = k b)
A, B: Type f: A -> B n: nat IH: forallC : Cyl f -> Type,
ExtendableAlong n cyl C ->
ExtendableAlong n cyl C C: Cyl f -> Type ext: ExtendableAlong n.+1 cyl C
forallg : foralla : A, C (cyl a),
ExtensionAlong cyl C g
A, B: Type f: A -> B n: nat IH: forallC : Cyl f -> Type,
ExtendableAlong n cyl C ->
ExtendableAlong n cyl C C: Cyl f -> Type ext: ExtendableAlong n.+1 cyl C g: foralla : A, C (cyl a)
ExtensionAlong cyl C g
A, B: Type f: A -> B n: nat IH: forallC : Cyl f -> Type,
ExtendableAlong n cyl C ->
ExtendableAlong n cyl C C: Cyl f -> Type ext: ExtendableAlong n.+1 cyl C g: foralla : A, C (cyl a)
ExtensionAlong cyl C g
exact (fst ext g).
A, B: Type f: A -> B n: nat IH: forallC : Cyl f -> Type,
ExtendableAlong n cyl C ->
ExtendableAlong n cyl C C: Cyl f -> Type ext: ExtendableAlong n.+1 cyl C
forallhk : forallb : Cyl f, C b,
ExtendableAlong n cyl (funb : Cyl f => h b = k b)
A, B: Type f: A -> B n: nat IH: forallC : Cyl f -> Type,
ExtendableAlong n cyl C ->
ExtendableAlong n cyl C C: Cyl f -> Type ext: ExtendableAlong n.+1 cyl C h, k: forallb : Cyl f, C b
ExtendableAlong n cyl (funb : Cyl f => h b = k b)
exact (snd ext h k).Defined.Definitioncyl_ooextendable
{AB} (f : A -> B) (C : Cyl f -> Type)
(ext : ooExtendableAlong cyl C)
: ooExtendableAlong cyl C
:= funn => cyl_extendable n f C (ext n).
A, B: Type f: A -> B C: B -> Type g: foralla : 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: foralla : 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: foralla : A, C (pr_cyl (cyl a)) ext: ExtensionAlong f C g
ExtensionAlong cyl (funx : Cyl f => C (pr_cyl x)) g
A, B: Type f: A -> B C: B -> Type g: foralla : A, C (pr_cyl (cyl a)) ext: ExtensionAlong f C g
forallx : 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
(funx : 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.Definitioncyl_ooextendable'
{AB} (f : A -> B) (C : B -> Type)
(ext : ooExtendableAlong f C)
: ooExtendableAlong cyl (C o (pr_cyl' f))
:= funn => 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: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : 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: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : 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: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : A * B, P (functor_prod f g z)
forally : A' * B', P y
A, B, A', B': Type f: A -> A' g: B -> B' P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : A * B, P (functor_prod f g z)
(funs0 : forally : A' * B', P y =>
forallx : 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: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : A * B, P (functor_prod f g z)
forally : A' * B', P y
A, B, A', B': Type f: A -> A' g: B -> B' P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : A * B, P (functor_prod f g z) a': A'
forallb' : B', P (a', b')
A, B, A', B': Type f: A -> A' g: B -> B' P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : A * B, P (functor_prod f g z) a': A'
foralla : B, P (a', g a)
A, B, A', B': Type f: A -> A' g: B -> B' P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : A * B, P (functor_prod f g z) b: B
foralla' : A', P (a', g b)
A, B, A', B': Type f: A -> A' g: B -> B' P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : A * B, P (functor_prod f g z) b: B
foralla : A, P (f a, g b)
A, B, A', B': Type f: A -> A' g: B -> B' P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : 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: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : A * B, P (functor_prod f g z)
(funs0 : forally : A' * B', P y =>
forallx : A * B, s0 (functor_prod f g x) = s x)
(funy : A' * B' =>
(fun (a' : A') (b' : B') =>
(fst (eg a')
(funb : B =>
(fst (ef (g b)) (funa : 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: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : A * B, P (functor_prod f g z) a: A b: B
(fst (eg (f a))
(funb : B =>
(fst (ef (g b)) (funa : 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: forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b')) s: forallz : A * B, P (functor_prod f g z) a: A b: B
(fst (ef (g b)) (funa : 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: forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n g (funb' : 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: forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n g (funb' : 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: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b'))
forallg0 : foralla : 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: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b'))
forallhk : forallb : A' * B', P b,
ExtendableAlong n (functor_prod f g)
(funb : A' * B' => h b = k b)
A, B, A', B': Type f: A -> A' g: B -> B' n: nat IH: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b'))
forallg0 : foralla : 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: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b'))
forallb' : B',
ExtendableAlong 1 f (funa' : A' => P (a', b'))
A, B, A', B': Type f: A -> A' g: B -> B' n: nat IH: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b'))
foralla' : A',
ExtendableAlong 1 g (funb' : B' => P (a', b'))
A, B, A', B': Type f: A -> A' g: B -> B' n: nat IH: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b'))
forallb' : B',
ExtendableAlong 1 f (funa' : 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: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b'))
foralla' : A',
ExtendableAlong 1 g (funb' : 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: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b'))
forallhk : forallb : A' * B', P b,
ExtendableAlong n (functor_prod f g)
(funb : A' * B' => h b = k b)
A, B, A', B': Type f: A -> A' g: B -> B' n: nat IH: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b')) h, k: forallb : A' * B', P b
forallb' : B',
ExtendableAlong n f
(funa' : A' => h (a', b') = k (a', b'))
A, B, A', B': Type f: A -> A' g: B -> B' n: nat IH: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b')) h, k: forallb : A' * B', P b
foralla' : A',
ExtendableAlong n g
(funb' : B' => h (a', b') = k (a', b'))
A, B, A', B': Type f: A -> A' g: B -> B' n: nat IH: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b')) h, k: forallb : A' * B', P b
forallb' : B',
ExtendableAlong n f
(funa' : 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: forallP : A' * B' -> Type,
(forallb' : B',
ExtendableAlong n f (funa' : A' => P (a', b'))) ->
(foralla' : A',
ExtendableAlong n g (funb' : B' => P (a', b'))) ->
ExtendableAlong n (functor_prod f g) P P: A' * B' -> Type ef: forallb' : B',
ExtendableAlong n.+1 f
(funa' : A' => P (a', b')) eg: foralla' : A',
ExtendableAlong n.+1 g
(funb' : B' => P (a', b')) h, k: forallb : A' * B', P b
foralla' : A',
ExtendableAlong n g
(funb' : B' => h (a', b') = k (a', b'))
intros a'; apply (snd (eg a')).Defined.Definitionooextendable_functor_prod
{ABA'B'} (f : A -> A') (g : B -> B')
(P : A' * B' -> Type)
(ef : forallb', ooExtendableAlong f (funa' => P (a',b')))
(eg : foralla', ooExtendableAlong g (funb' => P (a',b')))
: ooExtendableAlong (functor_prod f g) P
:= funn => extendable_functor_prod n f g P (funb' => ef b' n) (funa' => eg a' n).(** ** Extendability along [functor_sigma] *)
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong 1 (f a) (funv : Q a => C (a; v)) s: forallz : {x : _ & P x},
C (functor_sigma idmap f z)
ExtensionAlong (functor_sigma idmap f) C s
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong 1 (f a) (funv : Q a => C (a; v)) s: forallz : {x : _ & P x},
C (functor_sigma idmap f z)
ExtensionAlong (functor_sigma idmap f) C s
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong 1 (f a) (funv : Q a => C (a; v)) s: forallz : {x : _ & P x},
C (functor_sigma idmap f z)
forally : {x : _ & Q x}, C y
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong 1 (f a) (funv : Q a => C (a; v)) s: forallz : {x : _ & P x},
C (functor_sigma idmap f z)
(funs0 : forally : {x : _ & Q x}, C y =>
forallx : {x : _ & P x},
s0 (functor_sigma idmap f x) = s x) ?proj1
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong 1 (f a) (funv : Q a => C (a; v)) s: forallz : {x : _ & P x},
C (functor_sigma idmap f z)
forally : {x : _ & Q x}, C y
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong 1 (f a) (funv : Q a => C (a; v)) s: forallz : {x : _ & P x},
C (functor_sigma idmap f z) a: A
forallv : Q a, C (a; v)
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong 1 (f a) (funv : Q a => C (a; v)) s: forallz : {x : _ & P x},
C (functor_sigma idmap f z) a: A
foralla0 : P a, C (a; f a a0)
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong 1 (f a) (funv : Q a => C (a; v)) s: forallz : {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: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong 1 (f a) (funv : Q a => C (a; v)) s: forallz : {x : _ & P x},
C (functor_sigma idmap f z)
(funs0 : forally : {x : _ & Q x}, C y =>
forallx : {x : _ & P x},
s0 (functor_sigma idmap f x) = s x)
(funy : {x : _ & Q x} =>
(fun (a : A) (v : Q a) =>
(fst (ef a) (funu : P a => s (a; u))).1 v) y.1
y.2)
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong 1 (f a) (funv : Q a => C (a; v)) s: forallz : {x : _ & P x},
C (functor_sigma idmap f z) a: A u: P a
(fst (ef a) (funu : 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: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong n (f a) (funv : Q a => C (a; v))
ExtendableAlong n (functor_sigma idmap f) C
n: nat A: Type P, Q: A -> Type f: foralla : A, P a -> Q a C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong n (f a) (funv : Q a => C (a; v))
ExtendableAlong n (functor_sigma idmap f) C
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a n: nat IH: forallC : {x : _ & Q x} -> Type,
(foralla : A,
ExtendableAlong n (f a)
(funv : Q a => C (a; v))) ->
ExtendableAlong n (functor_sigma idmap f) C C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong n.+1 (f a)
(funv : Q a => C (a; v))
forallg : foralla : {x : _ & P x},
C (functor_sigma idmap f a),
ExtensionAlong (functor_sigma idmap f) C g
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a n: nat IH: forallC : {x : _ & Q x} -> Type,
(foralla : A,
ExtendableAlong n (f a)
(funv : Q a => C (a; v))) ->
ExtendableAlong n (functor_sigma idmap f) C C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong n.+1 (f a)
(funv : Q a => C (a; v))
forallhk : forallb : {x : _ & Q x}, C b,
ExtendableAlong n (functor_sigma idmap f)
(funb : {x : _ & Q x} => h b = k b)
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a n: nat IH: forallC : {x : _ & Q x} -> Type,
(foralla : A,
ExtendableAlong n (f a)
(funv : Q a => C (a; v))) ->
ExtendableAlong n (functor_sigma idmap f) C C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong n.+1 (f a)
(funv : Q a => C (a; v))
forallg : foralla : {x : _ & P x},
C (functor_sigma idmap f a),
ExtensionAlong (functor_sigma idmap f) C g
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a n: nat IH: forallC : {x : _ & Q x} -> Type,
(foralla : A,
ExtendableAlong n (f a)
(funv : Q a => C (a; v))) ->
ExtendableAlong n (functor_sigma idmap f) C C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong n.+1 (f a)
(funv : Q a => C (a; v))
foralla : A,
ExtendableAlong 1 (f a) (funv : Q a => C (a; v))
intros a; exact (fst (ef a) , fun__ => tt).
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a n: nat IH: forallC : {x : _ & Q x} -> Type,
(foralla : A,
ExtendableAlong n (f a)
(funv : Q a => C (a; v))) ->
ExtendableAlong n (functor_sigma idmap f) C C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong n.+1 (f a)
(funv : Q a => C (a; v))
forallhk : forallb : {x : _ & Q x}, C b,
ExtendableAlong n (functor_sigma idmap f)
(funb : {x : _ & Q x} => h b = k b)
A: Type P, Q: A -> Type f: foralla : A, P a -> Q a n: nat IH: forallC : {x : _ & Q x} -> Type,
(foralla : A,
ExtendableAlong n (f a)
(funv : Q a => C (a; v))) ->
ExtendableAlong n (functor_sigma idmap f) C C: {x : _ & Q x} -> Type ef: foralla : A,
ExtendableAlong n.+1 (f a)
(funv : Q a => C (a; v)) h, k: forallb : {x : _ & Q x}, C b
foralla : A,
ExtendableAlong n (f a)
(funv : Q a => h (a; v) = k (a; v))
intros a; apply (snd (ef a)).Defined.Definitionooextendable_functor_sigma_id
{A} {PQ : A -> Type} (f : foralla, P a -> Q a)
(C : sig Q -> Type)
(ef : foralla, ooExtendableAlong (f a) (funv => C (a;v)))
: ooExtendableAlong (functor_sigma idmap f) C
:= funn => extendable_functor_sigma_id n f C (funa => ef a n).(** Unfortunately, the technology of [ExtensionAlong] seems to be insufficient to state a general, funext-free version of [extension_functor_sigma] with a non-identity map on the bases; the hypothesis on the fiberwise map would have to be the existence of an extension in a function-type "up to pointwise equality". With wild oo-groupoids we could probably manage it. For now, we say something a bit hacky. *)DefinitionHomotopyExtensionAlong {AB} {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) & forallav, q (f a) v = p a v }.FixpointHomotopyExtendableAlong (n : nat)
{AB} {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 (hk : forallz, C z),
HomotopyExtendableAlong n f (funz => h z = k z)))
end.DefinitionooHomotopyExtendableAlong
{AB} {Q : B -> Type} (f : A -> B) (C : sig Q -> Type)
:= foralln, HomotopyExtendableAlong n f C.
A, B: Type P: A -> Type Q: B -> Type f: A -> B g: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {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: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {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: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {x : _ & P x}, C (functor_sigma f g z)
forally : {x : _ & Q x}, C y
A, B: Type P: A -> Type Q: B -> Type f: A -> B g: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {x : _ & P x}, C (functor_sigma f g z)
(funs0 : forally : {x : _ & Q x}, C y =>
forallx : {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: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {x : _ & P x}, C (functor_sigma f g z)
forally : {x : _ & Q x}, C y
A, B: Type P: A -> Type Q: B -> Type f: A -> B g: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {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: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {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: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {x : _ & P x}, C (functor_sigma f g z) a: A
forallv : Q (f a), C (f a; v)
A, B: Type P: A -> Type Q: B -> Type f: A -> B g: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {x : _ & P x}, C (functor_sigma f g z) a: A
foralla0 : P a, C (f a; g a a0)
A, B: Type P: A -> Type Q: B -> Type f: A -> B g: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {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: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {x : _ & P x}, C (functor_sigma f g z)
(funs0 : forally : {x : _ & Q x}, C y =>
forallx : {x : _ & P x},
s0 (functor_sigma f g x) = s x)
(funy : {x : _ & Q x} =>
(fun (b : B) (v : Q b) =>
(fst ef
(funa : A =>
(fst (eg a) (funu : 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: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {x : _ & P x}, C (functor_sigma f g z) a: A u: P a
(fst ef
(funa : A =>
(fst (eg a) (funu : 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: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong 1 f C eg: foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v)) s: forallz : {x : _ & P x}, C (functor_sigma f g z) a: A u: P a
(fst (eg (a; u).1)
(funu0 : 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: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong n f C eg: foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A, P a -> Q (f a) C: {x : _ & Q x} -> Type ef: HomotopyExtendableAlong n f C eg: foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : Q (f a) => C (f a; v))
forallg0 : foralla : {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: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : Q (f a) => C (f a; v))
forallhk : forallb : {x : _ & Q x}, C b,
ExtendableAlong n (functor_sigma f g)
(funb : {x : _ & Q x} => h b = k b)
A, B: Type P: A -> Type Q: B -> Type f: A -> B g: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : Q (f a) => C (f a; v))
forallg0 : foralla : {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: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : Q (f a) => C (f a; v))
HomotopyExtendableAlong 1 f C
A, B: Type P: A -> Type Q: B -> Type f: A -> B g: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : Q (f a) => C (f a; v))
foralla : A,
ExtendableAlong 1 (g a)
(funv : Q (f a) => C (f a; v))
A, B: Type P: A -> Type Q: B -> Type f: A -> B g: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : 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: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : Q (f a) => C (f a; v))
foralla : A,
ExtendableAlong 1 (g a)
(funv : 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: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : Q (f a) => C (f a; v))
forallhk : forallb : {x : _ & Q x}, C b,
ExtendableAlong n (functor_sigma f g)
(funb : {x : _ & Q x} => h b = k b)
A, B: Type P: A -> Type Q: B -> Type f: A -> B g: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : Q (f a) => C (f a; v)) h, k: forallb : {x : _ & Q x}, C b
HomotopyExtendableAlong n f
(funb : {x : _ & Q x} => h b = k b)
A, B: Type P: A -> Type Q: B -> Type f: A -> B g: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : Q (f a) => C (f a; v)) h, k: forallb : {x : _ & Q x}, C b
foralla : A,
ExtendableAlong n (g a)
(funv : Q (f a) => h (f a; v) = k (f a; v))
A, B: Type P: A -> Type Q: B -> Type f: A -> B g: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : Q (f a) => C (f a; v)) h, k: forallb : {x : _ & Q x}, C b
HomotopyExtendableAlong n f
(funb : {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: foralla : A, P a -> Q (f a) n: nat IH: forallC : {x : _ & Q x} -> Type,
HomotopyExtendableAlong n f C ->
(foralla : A,
ExtendableAlong n (g a)
(funv : 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: foralla : A,
ExtendableAlong n.+1 (g a)
(funv : Q (f a) => C (f a; v)) h, k: forallb : {x : _ & Q x}, C b
foralla : A,
ExtendableAlong n (g a)
(funv : Q (f a) => h (f a; v) = k (f a; v))
intros a; apply (snd (eg a)).Defined.Definitionooextendable_functor_sigma
{AB} {P : A -> Type} {Q : B -> Type}
(f : A -> B) (g : foralla, P a -> Q (f a))
(C : sig Q -> Type)
(ef : ooHomotopyExtendableAlong f C)
(eg : foralla, ooExtendableAlong (g a) (funv => C (f a ; v)))
: ooExtendableAlong (functor_sigma f g) C
:= funn => extendable_functor_sigma n f g C (ef n) (funa => 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: forallz : 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: forallz : 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: forallz : A + B, P (functor_sum f g z)
foralla : 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: forallz : A + B, P (functor_sum f g z)
forallb : 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: forallz : A + B, P (functor_sum f g z)
foralla : A,
(funs : 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: forallz : A + B, P (functor_sum f g z)
forallb : B,
(funs : 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: forallz : A + B, P (functor_sum f g z)
foralla : 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: forallz : A + B, P (functor_sum f g z)
forallb : 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: forallz : A + B, P (functor_sum f g z)
foralla : A,
(funs : 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: forallz : A + B, P (functor_sum f g z)
forallb : B,
(funs : 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: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x))
forallg0 : foralla : 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: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x))
forallhk : forallb : A' + B', P b,
ExtendableAlong n (functor_sum f g)
(funb : A' + B' => h b = k b)
n: nat A, B, A', B': Type f: A -> A' g: B -> B' IH: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x))
forallg0 : foralla : 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: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x)) h: foralla : A + B, P (functor_sum f g a)
ExtendableAlong 1 f (funx : A' => P (inl x))
n: nat A, B, A', B': Type f: A -> A' g: B -> B' IH: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x)) h: foralla : A + B, P (functor_sum f g a)
ExtendableAlong 1 g (funx : B' => P (inr x))
n: nat A, B, A', B': Type f: A -> A' g: B -> B' IH: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x)) h: foralla : A + B, P (functor_sum f g a)
ExtendableAlong 1 f (funx : A' => P (inl x))
exact (fst ef, fun__ => tt).
n: nat A, B, A', B': Type f: A -> A' g: B -> B' IH: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x)) h: foralla : A + B, P (functor_sum f g a)
ExtendableAlong 1 g (funx : B' => P (inr x))
exact (fst eg, fun__ => tt).
n: nat A, B, A', B': Type f: A -> A' g: B -> B' IH: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x))
forallhk : forallb : A' + B', P b,
ExtendableAlong n (functor_sum f g)
(funb : A' + B' => h b = k b)
n: nat A, B, A', B': Type f: A -> A' g: B -> B' IH: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x)) h, k: forallb : A' + B', P b
ExtendableAlong n (functor_sum f g)
(funb : A' + B' => h b = k b)
n: nat A, B, A', B': Type f: A -> A' g: B -> B' IH: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x)) h, k: forallb : A' + B', P b
ExtendableAlong n f
(funx : A' => h (inl x) = k (inl x))
n: nat A, B, A', B': Type f: A -> A' g: B -> B' IH: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x)) h, k: forallb : A' + B', P b
ExtendableAlong n g
(funx : B' => h (inr x) = k (inr x))
n: nat A, B, A', B': Type f: A -> A' g: B -> B' IH: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x)) h, k: forallb : A' + B', P b
ExtendableAlong n f
(funx : 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: forallP : A' + B' -> Type,
ExtendableAlong n f (funx : A' => P (inl x)) ->
ExtendableAlong n g (funx : B' => P (inr x)) ->
ExtendableAlong n (functor_sum f g) P P: A' + B' -> Type ef: ExtendableAlong n.+1 f (funx : A' => P (inl x)) eg: ExtendableAlong n.+1 g (funx : B' => P (inr x)) h, k: forallb : A' + B', P b
ExtendableAlong n g
(funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : 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)
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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A, ((funx : A' => C (coeq x)) o pr_cyl' k) (cyl a)) ->
forally : Cyl k, ((funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A, ((funx : A' => C (coeq x)) o pr_cyl' k) (cyl a)) ->
forally : Cyl k, ((funx : A' => C (coeq x)) o pr_cyl' k) y
forall
(u : forallx : Cyl h, C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h, C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A, ((funx : A' => C (coeq x)) o pr_cyl' k) (cyl a)) ->
forally : Cyl k, ((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y
forall
(u : forallx : Cyl h, C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h, C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h, C' (coeq (functor_cyl p x)) v: forallx : Cyl h, C' (coeq (functor_cyl q x))
ExtendableAlong 1 cyl
(funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h, C' (coeq (functor_cyl p x)) v: forallx : Cyl h, C' (coeq (functor_cyl q x))
forallb : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h, C' (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h, C' (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h, C' (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h, C' (coeq (functor_cyl p x)) v: forallx : Cyl h, C' (coeq (functor_cyl q x))
ExtendableAlong 1 (funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h, C' (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h, C' (coeq (functor_cyl p x)) v: forallx : Cyl h, C' (coeq (functor_cyl q x))
ExtendableAlong 1 (funx : B => pr_cyl (cyl x)) ?Goal1
exact (eh (funx => 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h, C' (coeq (functor_cyl p x)) v: forallx : Cyl h, C' (coeq (functor_cyl q x))
forallb : Cyl h,
(funb0 : Cyl h =>
(funx : B' =>
(funx0 : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
(funb : Cyl h =>
(funx : B' =>
(funx0 : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
(funr : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
(funr : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
(ap
(funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
(funr : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
(ap
(funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
(ap
(funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
(ap (funy : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
(ap
(funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
(ap (funy : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
(ap (funy : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
ap (funy : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y u: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl p x)) v: forallx : Cyl h,
(C o pr_cylcoeq p q) (coeq (functor_cyl q x)) x: Cyl h
ap (funy : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y
foralla : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y
forallb : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y
foralla : A,
(funw : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y
forallb : B,
transport
(funw : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y
foralla : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y
forallb : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y b: B
DPath C' (cglue (cyl b))
(ea1 (funx : A => s' (coeq x))
(functor_cyl p (cyl b)))
(ea1 (funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y b: B
DPath (funx : Coeq f g => C' (cyl_cylcoeq p q x))
(cglue b)
(ea1 (funx : A => s' (coeq x))
(functor_cyl p (cyl b)))
(ea1 (funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y
foralla : A,
(funw : Coeq f g =>
Coeq_ind C' (ea1 (s' o coeq))
(eb1
(funy : Cyl h =>
ea1 (funx : A => s' (coeq x))
(functor_cyl p y))
(funy : Cyl h =>
ea1 (funx : A => s' (coeq x))
(functor_cyl q y))
(funb : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y
forallb : B,
transport
(funw : Coeq f g =>
Coeq_ind C' (ea1 (s' o coeq))
(eb1
(funy : Cyl h =>
ea1 (funx : A => s' (coeq x))
(functor_cyl p y))
(funy : Cyl h =>
ea1 (funx : A => s' (coeq x))
(functor_cyl q y))
(funb0 : 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) ((funa : A => 1) (f b)) =
(funa : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y b: B
transport
(funw : Coeq f g =>
Coeq_ind C' (ea1 (s' o coeq))
(eb1
(funy : Cyl h =>
ea1 (funx : A => s' (coeq x))
(functor_cyl p y))
(funy : Cyl h =>
ea1 (funx : A => s' (coeq x))
(functor_cyl q y))
(funb : 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) ((funa : A => 1) (f b)) =
(funa : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y b: B
DPathSquare
(funx : Coeq f g => C' (cyl_cylcoeq p q x))
(PathSquare.sq_refl_h (cglue b))
(apD
(funx : Coeq f g =>
Coeq_ind C' (ea1 (funx0 : A => s' (coeq x0)))
(eb1
(funy : Cyl h =>
ea1 (funx0 : A => s' (coeq x0))
(functor_cyl p y))
(funy : Cyl h =>
ea1 (funx0 : A => s' (coeq x0))
(functor_cyl q y))
(funb : 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)) 11
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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y b: B
DPath
(funx : coeq (f b) = coeq (g b) =>
DPath
(funx0 : Coeq f g => C' (cyl_cylcoeq p q x0)) x
(Coeq_ind C' (ea1 (funx0 : A => s' (coeq x0)))
(eb1
(funy : Cyl h =>
ea1 (funx0 : A => s' (coeq x0))
(functor_cyl p y))
(funy : Cyl h =>
ea1 (funx0 : A => s' (coeq x0))
(functor_cyl q y))
(funb : 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 (funx0 : A => s' (coeq x0)))
(eb1
(funy : Cyl h =>
ea1 (funx0 : A => s' (coeq x0))
(functor_cyl p y))
(funy : Cyl h =>
ea1 (funx0 : A => s' (coeq x0))
(functor_cyl q y))
(funb : 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
(funx : Coeq f g =>
Coeq_ind C' (ea1 (funx0 : A => s' (coeq x0)))
(eb1
(funy : Cyl h =>
ea1 (funx0 : A => s' (coeq x0))
(functor_cyl p y))
(funy : Cyl h =>
ea1 (funx0 : A => s' (coeq x0))
(functor_cyl q y))
(funb : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : 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 (funx : A => s' (coeq x)))
(eb1
(funy : Cyl h =>
ea1 (funx : A => s' (coeq x))
(functor_cyl p y))
(funy : Cyl h =>
ea1 (funx : A => s' (coeq x))
(functor_cyl q y))
(funb : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x) s: forallx : Coeq f g, C (functor_coeq h k p q x) C':= C o pr_cylcoeq p q: CylCoeq p q -> Type s':= funx : Coeq f g =>
transport C (pr_cyl_cylcoeq p q x) (s x): forallx : Coeq f g,
C (pr_cylcoeq p q (cyl_cylcoeq p q x)) ea1:= funu : foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a) =>
(fst
(cyl_extendable' 1 k
(funx : A' => C (coeq x)) ek) u).1: (foralla : A,
((funx : A' => C (coeq x)) o pr_cyl' k)
(cyl a)) ->
forally : Cyl k,
((funx : A' => C (coeq x)) o pr_cyl' k) y eb'': forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
ExtendableAlong 1 cyl
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x)) eb1:= fun
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x)))
(w : foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) =>
(fst
(cyl_extendable 1 h
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(eb'' u v)) w).1: forall
(u : forallx : Cyl h,
C' (coeq (functor_cyl p x)))
(v : forallx : Cyl h,
C' (coeq (functor_cyl q x))),
(foralla : B,
(funx : Cyl h =>
DPath C' (cglue x) (u x) (v x))
(cyl a)) ->
forally : Cyl h,
(funx : Cyl h => DPath C' (cglue x) (u x) (v x))
y b: B
apD
(Coeq_ind C' (ea1 (funx : A => s' (coeq x)))
(eb1
(funy : Cyl h =>
ea1 (funx : A => s' (coeq x))
(functor_cyl p y))
(funy : Cyl h =>
ea1 (funx : A => s' (coeq x))
(functor_cyl q y))
(funb : 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))
napply Coeq_ind_beta_cglue.Defined.(** Now we can easily iterate into higher extendability. *)
n: nat B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h C: Coeq f' g' -> Type ek: ExtendableAlong n k (C o coeq) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : 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: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : 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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x)
forallg0 : foralla : 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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x)
forallh0k0 : forallb : Coeq f' g', C b,
ExtendableAlong n (functor_coeq h k p q)
(funb : 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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x)
forallg0 : foralla : 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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x)
ExtendableAlong 1 k (funx : 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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x)
foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : 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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x)
ExtendableAlong 1 k (funx : 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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x)
foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong 1 h (funx : B' => u x = v x)
exact (funuv => (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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x)
forallh0k0 : forallb : Coeq f' g', C b,
ExtendableAlong n (functor_coeq h k p q)
(funb : 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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x) u, v: forallb : Coeq f' g', C b
ExtendableAlong n k
(funx : 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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x) u, v: forallb : Coeq f' g', C b
forallu0v0 : forallx : B', u (coeq (g' x)) = v (coeq (g' x)),
ExtendableAlong n h (funx : 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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x) u, v: forallb : Coeq f' g', C b
ExtendableAlong n k
(funx : 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: forallC : Coeq f' g' -> Type,
ExtendableAlong n k (funx : A' => C (coeq x)) ->
(foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)) ->
ExtendableAlong n (functor_coeq h k p q) C C: Coeq f' g' -> Type ek: ExtendableAlong n.+1 k (funx : A' => C (coeq x)) eh: foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n.+1 h (funx : B' => u x = v x) u, v: forallb : Coeq f' g', C b
forallu0v0 : forallx : B', u (coeq (g' x)) = v (coeq (g' x)),
ExtendableAlong n h (funx : B' => u0 x = v0 x)
exact (snd (eh (u o coeq o g') (v o coeq o g'))).Defined.Definitionooextendable_functor_coeq
{BAfgB'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 (uv : forallx : B', C (coeq (g' x))),
ooExtendableAlong h (funx => u x = v x))
: ooExtendableAlong (functor_coeq h k p q) C
:= funn => extendable_functor_coeq n (ek n) (funuv => 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 (funx : 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')
foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : 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')
foralluv : forallx : B', C (coeq (g' x)),
ExtendableAlong n h (funx : B' => u x = v x)
exact (snd eh).Defined.Definitionooextendable_functor_coeq'
{BAfgB'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
:= funn => extendable_functor_coeq' n (ek n) (eh n.+1).