Timings for Extensions.v
(* -*- mode: coq; mode: visual-line -*- *)
(** * Extensions and extendible maps *)
Require Import HoTT.Basics HoTT.Types.
Require Import Equiv.PathSplit PathAny.
Require Import Cubical.DPath Cubical.DPathSquare.
Require Import Colimits.Coeq Colimits.MappingCylinder.
Local Open Scope nat_scope.
Local Open Scope path_scope.
(** Given [C : B -> Type] and [f : A -> B], an extension of [g : forall a, C (f a)] along [f] is a section [h : forall b, C b] such that [h (f a) = g a] for all [a:A]. This is equivalently the existence of fillers for commutative squares, restricted to the case where the bottom of the square is the identity; type-theoretically, this approach is sometimes more convenient. In this file we study the type of such extensions. One of its crucial properties is that a path between extensions is equivalently an extension in a fibration of paths.
This turns out to be useful for several reasons. For instance, by iterating it, we can to formulate universal properties without needing [Funext]. It also gives us a way to "quantify" a universal property by the connectedness of the type of extensions. *)
(* TODO: consider naming for [ExtensionAlong] and subsequent lemmas. As a name for the type itself, [Extension] or [ExtensionAlong] seems great; but resultant lemma names such as [path_extension] (following existing naming conventions) are rather misleading. *)
(** This elimination rule (and others) can be seen as saying that, given a fibration over the codomain and a section of it over the domain, there is some *extension* of this to a section over the whole codomain. It can also be considered as an equivalent form of an [hfiber] of precomposition-with-[f] that replaces paths by pointwise paths, thereby avoiding [Funext]. *)
Definition ExtensionAlong@{a b p m} {A : Type@{a}} {B : Type@{b}} (f : A -> B)
(P : B -> Type@{p}) (d : forall x:A, P (f x))
:= (* { s : forall y:B, P y & forall x:A, s (f x) = d x }. *)
sig@{m m} (fun (s : forall y:B, P y) => forall x:A, s (f x) = d x).
(** [ExtensionAlong] takes 4 universe parameters:
- the size of A
- the size of B
- the size of P
- >= max(A,B,P)
*)
(** It's occasionally useful to be able to modify those universes. For each of the universes [a], [b], [p], we give an initial one, a final one, and a "minimum" one smaller than both and where the type actually lives. *)
Definition lift_extensionalong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} {A : Type@{amin}} {B : Type@{bmin}} (f : A -> B)
(P : B -> Type@{pmin}) (d : forall x:A, P (f x))
: ExtensionAlong@{a1 b1 p1 m1} f P d -> ExtensionAlong@{a2 b2 p2 m2} 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. *)
assert (e2 := ext.2); set (e1 := ext.1) in e2.
(** Curiously, without this line we get a spurious universe inequality [p1 <= m2]. *)
(** 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. *)
Definition equiv_path_extension `{Funext} {A B : Type} {f : A -> B}
{P : B -> Type} {d : forall x:A, P (f x)}
(ext ext' : ExtensionAlong f P d)
: (ExtensionAlong f
(fun y => pr1 ext y = pr1 ext' y)
(fun x => pr2 ext x @ (pr2 ext' x)^))
<~> ext = ext'.
srapply equiv_path_from_contr.
unfold ExtensionAlong; cbn.
exists (fun y => 1%path).
intros x; symmetry; apply concat_pV.
destruct ext as [g gd]; unfold ExtensionAlong; cbn.
refine (contr_sigma_sigma
(forall y:B, P y) (fun s => forall x:A, s (f x) = d x)
(fun a => g == a)
(fun a b c => forall x:A, c (f x) = gd x @ (b x)^)
g (fun y:B => idpath (g y))).
refine (contr_equiv' {p:g o f == d & gd == p} _).
refine (equiv_functor_sigma_id _); intros p.
refine (equiv_functor_forall_id _); intros x; cbn.
refine (_ oE equiv_path_inverse _ _).
symmetry; apply equiv_moveR_1M.
Definition path_extension `{Funext} {A B : Type} {f : A -> B}
{P : B -> Type} {d : forall x:A, P (f x)}
(ext ext' : ExtensionAlong f P d)
: (ExtensionAlong f
(fun y => pr1 ext y = pr1 ext' y)
(fun x => pr2 ext x @ (pr2 ext' x)^))
-> ext = ext'
:= equiv_path_extension ext ext'.
Global Instance isequiv_path_extension `{Funext} {A B : Type} {f : A -> B}
{P : B -> Type} {d : forall x:A, P (f x)}
(ext ext' : ExtensionAlong f P d)
: IsEquiv (path_extension ext ext') | 0
:= equiv_isequiv _.
(** Here is the iterated version. *)
Fixpoint ExtendableAlong@{i j k l}
(n : nat) {A : Type@{i}} {B : Type@{j}}
(f : A -> B) (C : B -> Type@{k}) : Type@{l}
:= match n with
| 0 => Unit
| S n => (forall (g : forall a, C (f a)),
ExtensionAlong@{i j k l} f C g) *
forall (h k : forall b, C b),
ExtendableAlong n f (fun b => h b = k b)
end.
(** [ExtendableAlong] takes 4 universe parameters:
- size of A
- size of B
- size of C
- size of result (>= A,B,C) *)
Global Arguments ExtendableAlong n%nat_scope {A B}%type_scope (f C)%function_scope.
(** We can modify the universes, as with [ExtensionAlong]. *)
Definition lift_extendablealong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2}
(n : nat) {A : Type@{amin}} {B : Type@{bmin}}
(f : A -> B) (P : B -> Type@{pmin})
: ExtendableAlong@{a1 b1 p1 m1} n f P -> ExtendableAlong@{a2 b2 p2 m2} n f P.
revert P; simple_induction n n IH; intros P.
intros g; exact (lift_extensionalong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} _ _ _ (fst ext g)).
(** Unles we give the universe explicitly here, [kmin] gets collapsed to [k1]. *)
pose (P' := (fun b => h b = k b) : B -> Type@{pmin}).
exact (IH P' (snd ext h k)).
Definition equiv_extendable_pathsplit `{Funext} (n : nat)
{A B : Type} (C : B -> Type) (f : A -> B)
: ExtendableAlong n f C
<~> PathSplit n (fun (g : forall b, C b) => g oD f).
generalize dependent C; simple_induction n n IHn; intros C.
refine (equiv_functor_forall' 1 _); intros g; simpl.
refine (equiv_functor_sigma' 1 _); intros rec.
refine (equiv_functor_forall' 1 _); intros h.
refine (equiv_functor_forall' 1 _); intros k; simpl.
refine (_ oE IHn (fun b => h b = k b)).
refine (equiv_functor_pathsplit n _ _
(equiv_apD10 _ _ _) (equiv_apD10 _ _ _) _).
Definition isequiv_extendable `{Funext} (n : nat)
{A B : Type} {C : B -> Type} {f : A -> B}
: ExtendableAlong n.+2 f C
-> IsEquiv (fun g => g oD f)
:= isequiv_pathsplit n o (equiv_extendable_pathsplit n.+2 C f).
Global Instance ishprop_extendable `{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).
Definition equiv_extendable_isequiv `{Funext} (n : nat)
{A B : Type} (C : B -> Type) (f : A -> B)
: ExtendableAlong n.+2 f C
<~> IsEquiv (fun (g : forall b, C b) => g oD f).
apply equiv_extendable_pathsplit.
apply equiv_pathsplit_isequiv.
(* Without [Funext], we can prove a small part of the above equivalence.
We suspect that the rest requires [Funext]. *)
Definition extension_isequiv_precompose
{A : Type} {B : Type}
(f : A -> B) (C : B -> Type)
: IsEquiv (fun (g : forall b, C b) => g oD f) -> forall g, ExtensionAlong f C g.
pose (e := Build_Equiv _ _ _ E).
(** Postcomposition with a known equivalence. Note that this does not require funext to define, although showing that it is an equivalence would require funext. *)
Definition extendable_postcompose' (n : nat)
{A B : Type} (C D : B -> Type) (f : A -> B)
(g : forall b, C b <~> D b)
: ExtendableAlong n f C -> ExtendableAlong n f D.
generalize dependent C; revert D.
simple_induction n n IH; intros C D g; simpl.
refine (functor_prod _ _).
refine (functor_forall (functor_forall idmap
(fun a => (g (f a))^-1)) _);
intros h; simpl.
refine (functor_sigma (functor_forall idmap g) _); intros k.
refine (functor_forall idmap _);
intros a; unfold functor_arrow, functor_forall, composeD; simpl.
refine (functor_forall (functor_forall idmap (fun b => (g b)^-1)) _);
intros h.
refine (functor_forall (functor_forall idmap (fun b => (g b)^-1)) _);
intros k; simpl; unfold functor_forall.
refine (IH _ _ _); intros b.
apply equiv_inverse, equiv_ap; exact _.
Definition extendable_postcompose (n : nat)
{A B : Type} (C D : B -> Type) (f : A -> B)
(g : forall b, C b -> D b) `{forall b, IsEquiv (g b)}
: ExtendableAlong n f C -> ExtendableAlong n f D
:= extendable_postcompose' n C D f (fun b => Build_Equiv _ _ (g b) _).
(** Composition of the maps we extend along. This also does not require funext. *)
Definition extendable_compose (n : nat)
{A B C : Type} (P : C -> Type) (f : A -> B) (g : B -> C)
: ExtendableAlong n g P -> ExtendableAlong n f (fun b => P (g b)) -> ExtendableAlong n (g o f) P.
revert P; simple_induction n n IHn; intros P extg extf; [ exact tt | split ].
exists ((fst extg (fst extf h).1).1); intros a.
refine ((fst extg (fst extf h).1).2 (f a) @ _).
exact ((fst extf h).2 a).
exact (snd extf (h oD g) (k oD g)).
Definition cancelL_extendable (n : nat)
{A B C : Type} (P : C -> Type) (f : A -> B) (g : B -> C)
: ExtendableAlong n g P -> ExtendableAlong n (g o f) P -> ExtendableAlong n f (fun b => P (g b)).
revert P; simple_induction n n IHn; intros P extg extgf; [ exact tt | split ].
exists ((fst extgf h).1 oD g); intros a.
exact ((fst extgf h).2 a).
pose (h' := (fst extg h).1).
pose (k' := (fst extg k).1).
refine (extendable_postcompose' n (fun b => h' (g b) = k' (g b)) (fun b => h b = k b) f _ _).
exact (equiv_concat_lr ((fst extg h).2 b)^ ((fst extg k).2 b)).
apply (IHn (fun c => h' c = k' c) (snd extg h' k') (snd extgf h' k')).
Definition cancelR_extendable (n : nat)
{A B C : Type} (P : C -> Type) (f : A -> B) (g : B -> C)
: ExtendableAlong n.+1 f (fun b => P (g b)) -> ExtendableAlong n (g o f) P -> ExtendableAlong n g P.
revert P; simple_induction n n IHn; intros P extf extgf; [ exact tt | split ].
exists ((fst extgf (h oD f)).1); intros b.
refine ((fst (snd extf ((fst extgf (h oD f)).1 oD g) h) _).1 b); intros a.
apply ((fst extgf (h oD f)).2).
apply (snd extf (h oD g) (k oD g)).
(** And transfer across homotopies *)
Definition extendable_homotopic (n : nat)
{A B : Type} (C : B -> Type) (f : A -> B) {g : A -> B} (p : f == g)
: ExtendableAlong n f C -> ExtendableAlong n g C.
revert C; simple_induction n n IHn; intros C extf; [ exact tt | split ].
exists ((fst extf (fun a => (p a)^ # h a)).1); intros a.
refine ((apD ((fst extf (fun a => (p a)^ # h a)).1) (p a))^ @ _).
exact ((fst extf (fun a => (p a)^ # h a)).2 a).
apply IHn, (snd extf h k).
(** We can extend along equivalences *)
Definition extendable_equiv (n : nat)
{A B : Type} (C : B -> Type) (f : A -> B) `{IsEquiv _ _ f}
: ExtendableAlong n f C.
revert C; simple_induction n n IHn; intros C; [ exact tt | split ].
exists (fun b => eisretr f b # h (f^-1 b)); intros a.
refine (transport2 C (eisadj f a) _ @ _).
refine ((transport_compose C f _ _)^ @ _).
exact (apD h (eissect f a)).
(** And into contractible types *)
Definition extendable_contr (n : nat)
{A B : Type} (C : B -> Type) (f : A -> B)
`{forall b, Contr (C b)}
: ExtendableAlong n f C.
generalize dependent C; simple_induction n n IHn;
intros C ?; [ exact tt | split ].
exists (fun _ => center _); intros a.
(** This is inherited by types of homotopies. *)
Definition extendable_homotopy (n : nat)
{A B : Type} (C : B -> Type) (f : A -> B)
(h k : forall b, C b)
: ExtendableAlong n.+1 f C -> ExtendableAlong n f (fun b => h b = k b).
revert C h k; simple_induction n n IHn;
intros C h k ext; [exact tt | split].
exact (fst (snd ext h k) p).
(** And the oo-version. *)
Definition ooExtendableAlong@{i j k l}
{A : Type@{i}} {B : Type@{j}}
(f : A -> B) (C : B -> Type@{k}) : Type@{l}
:= forall n : nat, ExtendableAlong@{i j k l} n f C.
(** Universe parameters are the same as for [ExtendableAlong]. *)
Global Arguments ooExtendableAlong {A B}%type_scope (f C)%function_scope.
(** Universe modification. *)
Definition lift_ooextendablealong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2}
{A : Type@{amin}} {B : Type@{bmin}}
(f : A -> B) (P : B -> Type@{pmin})
: ooExtendableAlong@{a1 b1 p1 m1} f P -> ooExtendableAlong@{a2 b2 p2 m2} f P
:= fun ext n => lift_extendablealong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} n f P (ext n).
(** We take part of the data from [ps 1] and part from [ps 2] so that the inverse chosen is the expected one. *)
Definition isequiv_ooextendable `{Funext}
{A B : Type} (C : B -> Type) (f : A -> B)
: ooExtendableAlong f C -> IsEquiv (fun g => g oD f)
:= fun ps => isequiv_extendable 0 (fst (ps 1%nat), snd (ps 2)).
Definition equiv_ooextendable_pathsplit `{Funext}
{A B : Type} (C : B -> Type) (f : A -> B)
: ooExtendableAlong f C <~>
ooPathSplit (fun (g : forall b, C b) => g oD f).
refine (equiv_functor_forall' 1 _); intros n.
apply equiv_extendable_pathsplit.
Global Instance ishprop_ooextendable `{Funext}
{A B : Type} (C : B -> Type) (f : A -> B)
: IsHProp (ooExtendableAlong f C).
refine (istrunc_equiv_istrunc _ (equiv_ooextendable_pathsplit C f)^-1).
Definition equiv_ooextendable_isequiv `{Funext}
{A B : Type} (C : B -> Type) (f : A -> B)
: ooExtendableAlong f C
<~> IsEquiv (fun (g : forall b, C b) => g oD f)
:= equiv_oopathsplit_isequiv _ oE equiv_ooextendable_pathsplit _ _.
Definition ooextendable_postcompose
{A B : Type} (C D : B -> Type) (f : A -> B)
(g : forall b, C b -> D b) `{forall b, IsEquiv (g b)}
: ooExtendableAlong f C -> ooExtendableAlong f D
:= fun ppp n => extendable_postcompose n C D f g (ppp n).
Definition ooextendable_postcompose'
{A B : Type} (C D : B -> Type) (f : A -> B)
(g : forall b, C b <~> D b)
: ooExtendableAlong f C -> ooExtendableAlong f D
:= fun ppp n => extendable_postcompose' n C D f g (ppp n).
Definition ooextendable_compose
{A B C : Type} (P : C -> Type) (f : A -> B) (g : B -> C)
: ooExtendableAlong g P -> ooExtendableAlong f (fun b => P (g b)) -> ooExtendableAlong (g o f) P
:= fun extg extf n => extendable_compose n P f g (extg n) (extf n).
Definition cancelL_ooextendable
{A B C : Type} (P : C -> Type) (f : A -> B) (g : B -> C)
: ooExtendableAlong g P -> ooExtendableAlong (g o f) P -> ooExtendableAlong f (fun b => P (g b))
:= fun extg extgf n => cancelL_extendable n P f g (extg n) (extgf n).
Definition cancelR_ooextendable
{A B C : Type} (P : C -> Type) (f : A -> B) (g : B -> C)
: ooExtendableAlong f (fun b => P (g b)) -> ooExtendableAlong (g o f) P -> ooExtendableAlong g P
:= fun extf extgf n => cancelR_extendable n P f g (extf n.+1) (extgf n).
Definition ooextendable_homotopic
{A B : Type} (C : B -> Type) (f : A -> B) {g : A -> B} (p : f == g)
: ooExtendableAlong f C -> ooExtendableAlong g C
:= fun extf n => extendable_homotopic n C f p (extf n).
Definition ooextendable_equiv
{A B : Type} (C : B -> Type) (f : A -> B) `{IsEquiv _ _ f}
: ooExtendableAlong f C
:= fun n => extendable_equiv n C f.
Definition ooextendable_contr
{A B : Type} (C : B -> Type) (f : A -> B)
`{forall b, Contr (C b)}
: ooExtendableAlong f C
:= fun n => extendable_contr n C f.
Definition ooextendable_homotopy
{A B : Type} (C : B -> Type) (f : A -> B)
(h k : forall b, C b)
: ooExtendableAlong f C -> ooExtendableAlong f (fun b => h b = k b).
intros ext n; apply extendable_homotopy, ext.
(** 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. *)
Definition ooextendable_isnull_fibers {A B} (f : A -> B) (C : B -> Type)
: (forall b, ooExtendableAlong (const_tt (hfiber f b))
(fun _ => C b))
-> ooExtendableAlong f C.
intros orth n; revert C orth.
induction n as [|n IHn]; intros C orth; [exact tt | split].
exists (fun b => (fst (orth b 1%nat) (fun x => x.2 # g x.1)).1 tt).
rewrite (path_unit tt (const_tt _ a)).
exact ((fst (orth (f a) 1%nat) _).2 (a ; 1)).
apply ooextendable_homotopy, orth.
(** ** Extendability along cofibrations *)
(** If a family is extendable along a cofibration (i.e. a mapping cylinder), it is extendable definitionally. *)
Definition cyl_extension {A B} (f : A -> B) (C : Cyl f -> Type)
(g : forall a, C (cyl a))
(ext : ExtensionAlong cyl C g)
: ExtensionAlong cyl C g.
srefine (Cyl_ind C g (ext.1 o cyr) _ ; _); intros a.
refine ((ext.2 a)^ @Dl _)%dpath.
(** The point is that this equality is now definitional. *)
Definition cyl_extendable (n : nat)
{A B} (f : A -> B) (C : Cyl f -> Type)
(ext : ExtendableAlong n cyl C)
: ExtendableAlong n cyl C.
revert C ext; simple_induction n n IH; intros C ext; [ exact tt | split ].
Definition cyl_ooextendable
{A B} (f : A -> B) (C : Cyl f -> Type)
(ext : ooExtendableAlong cyl C)
: ooExtendableAlong cyl C
:= fun n => cyl_extendable n f C (ext n).
Definition cyl_extension'
{A B} (f : A -> B) (C : B -> Type)
(g : forall a, C (pr_cyl (cyl a)))
(ext : ExtensionAlong f C g)
: ExtensionAlong cyl (C o pr_cyl) g.
Definition cyl_extendable' (n : nat)
{A B} (f : A -> B) (C : B -> Type)
(ext : ExtendableAlong n f C)
: ExtendableAlong n cyl (C o (pr_cyl' f)).
refine (cancelL_extendable n C cyl pr_cyl _ ext).
Definition cyl_ooextendable'
{A B} (f : A -> B) (C : B -> Type)
(ext : ooExtendableAlong f C)
: ooExtendableAlong cyl (C o (pr_cyl' f))
:= fun n => cyl_extendable' n f C (ext n).
(** ** Extendability along [functor_prod] *)
Definition extension_functor_prod
{A B A' B'} (f : A -> A') (g : B -> B')
(P : A' * B' -> Type)
(ef : forall b', ExtendableAlong 1 f (fun a' => P (a',b')))
(eg : forall a', ExtendableAlong 1 g (fun b' => P (a',b')))
(s : forall z, P (functor_prod f g z))
: ExtensionAlong (functor_prod f g) P s.
intros [a' b']; revert b'.
refine ((fst (eg a') _).1).
refine ((fst (ef (g b)) _).1).
refine ((fst (eg (f a)) _).2 b @ _).
exact ((fst (ef (g b)) _).2 a).
Definition extendable_functor_prod (n : nat)
{A B A' B'} (f : A -> A') (g : B -> B')
(P : A' * B' -> Type)
(ef : forall b', ExtendableAlong n f (fun a' => P (a',b')))
(eg : forall a', ExtendableAlong n g (fun b' => P (a',b')))
: ExtendableAlong n (functor_prod f g) P.
revert P ef eg; simple_induction n n IH; intros P ef eg; [ exact tt | split ].
apply extension_functor_prod.
intros b'; exact (fst (ef b'), fun _ _ => tt).
intros a'; exact (fst (eg a'), fun _ _ => tt).
intros b'; apply (snd (ef b')).
intros a'; apply (snd (eg a')).
Definition ooextendable_functor_prod
{A B A' B'} (f : A -> A') (g : B -> B')
(P : A' * B' -> Type)
(ef : forall b', ooExtendableAlong f (fun a' => P (a',b')))
(eg : forall a', ooExtendableAlong g (fun b' => P (a',b')))
: ooExtendableAlong (functor_prod f g) P
:= fun n => extendable_functor_prod n f g P (fun b' => ef b' n) (fun a' => eg a' n).
(** ** Extendability along [functor_sigma] *)
Definition extension_functor_sigma_id
{A} {P Q : A -> Type} (f : forall a, P a -> Q a)
(C : sig Q -> Type)
(ef : forall a, ExtendableAlong 1 (f a) (fun v => C (a;v)))
(s : forall z, C (functor_sigma idmap f z))
: ExtensionAlong (functor_sigma idmap f) C s.
refine ((fst (ef a) _).1).
exact ((fst (ef a) _).2 u).
Definition extendable_functor_sigma_id n
{A} {P Q : A -> Type} (f : forall a, P a -> Q a)
(C : sig Q -> Type)
(ef : forall a, ExtendableAlong n (f a) (fun v => C (a;v)))
: ExtendableAlong n (functor_sigma idmap f) C.
revert C ef; simple_induction n n IH; intros C ef; [ exact tt | split ].
apply extension_functor_sigma_id.
intros a; exact (fst (ef a) , fun _ _ => tt).
intros a; apply (snd (ef a)).
Definition ooextendable_functor_sigma_id
{A} {P Q : A -> Type} (f : forall a, P a -> Q a)
(C : sig Q -> Type)
(ef : forall a, ooExtendableAlong (f a) (fun v => C (a;v)))
: ooExtendableAlong (functor_sigma idmap f) C
:= fun n => extendable_functor_sigma_id n f C (fun a => ef a n).
(** Unfortunately, the technology of [ExtensionAlong] seems to be insufficient to state a general, funext-free version of [extension_functor_sigma] with a nonidentity map on the bases; the hypothesis on the fiberwise map would have to be the existence of an extension in a function-type "up to pointwise equality". With wild oo-groupoids we could probably manage it. For now, we say something a bit hacky. *)
Definition HomotopyExtensionAlong {A B} {Q : B -> Type}
(f : A -> B) (C : sig Q -> Type)
(p : forall (a:A) (v:Q (f a)), C (f a;v))
:= { q : forall (b:B) (v:Q b), C (b;v) & forall a v, q (f a) v = p a v }.
Fixpoint HomotopyExtendableAlong (n : nat)
{A B} {Q : B -> Type} (f : A -> B) (C : sig Q -> Type) : Type
:= match n with
| 0 => Unit
| S n => ((forall (p : forall (a:A) (v:Q (f a)), C (f a;v)),
HomotopyExtensionAlong f C p) *
(forall (h k : forall z, C z),
HomotopyExtendableAlong n f (fun z => h z = k z)))
end.
Definition ooHomotopyExtendableAlong
{A B} {Q : B -> Type} (f : A -> B) (C : sig Q -> Type)
:= forall n, HomotopyExtendableAlong n f C.
Definition extension_functor_sigma
{A B} {P : A -> Type} {Q : B -> Type}
(f : A -> B) (g : forall a, P a -> Q (f a))
(C : sig Q -> Type)
(ef : HomotopyExtendableAlong 1 f C)
(eg : forall a, ExtendableAlong 1 (g a) (fun v => C (f a ; v)))
(s : forall z, C (functor_sigma f g z))
: ExtensionAlong (functor_sigma f g) C s.
intros [b v]; revert b v.
refine ((fst (eg a) _).1).
refine ((fst ef _).2 _ _ @ _).
exact ((fst (eg a) _).2 u).
Definition extendable_functor_sigma (n : nat)
{A B} {P : A -> Type} {Q : B -> Type}
(f : A -> B) (g : forall a, P a -> Q (f a))
(C : sig Q -> Type)
(ef : HomotopyExtendableAlong n f C)
(eg : forall a, ExtendableAlong n (g a) (fun v => C (f a ; v)))
: ExtendableAlong n (functor_sigma f g) C.
revert C ef eg; simple_induction n n IH; intros C ef eg; [ exact tt | split ].
apply extension_functor_sigma.
exact (fst ef, fun _ _ => tt).
intros a; exact (fst (eg a) , fun _ _ => tt).
intros a; apply (snd (eg a)).
Definition ooextendable_functor_sigma
{A B} {P : A -> Type} {Q : B -> Type}
(f : A -> B) (g : forall a, P a -> Q (f a))
(C : sig Q -> Type)
(ef : ooHomotopyExtendableAlong f C)
(eg : forall a, ooExtendableAlong (g a) (fun v => C (f a ; v)))
: ooExtendableAlong (functor_sigma f g) C
:= fun n => extendable_functor_sigma n f g C (ef n) (fun a => eg a n).
(** ** Extendability along [functor_sum] *)
Definition extension_functor_sum
{A B A' B'} (f : A -> A') (g : B -> B')
(P : A' + B' -> Type)
(ef : ExtendableAlong 1 f (P o inl))
(eg : ExtendableAlong 1 g (P o inr))
(h : forall z, P (functor_sum f g z))
: ExtensionAlong (functor_sum f g) P h.
srefine (sum_ind _ _ _ ; sum_ind _ _ _).
exact (fst ef (h o inl)).1.
exact (fst eg (h o inr)).1.
exact (fst ef (h o inl)).2.
exact (fst eg (h o inr)).2.
Definition extendable_functor_sum (n : nat)
{A B A' B'} (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.
revert P ef eg; induction n as [|n IH]; intros P ef eg; [ exact tt | split ].
intros h; apply extension_functor_sum.
exact (fst ef, fun _ _ => tt).
exact (fst eg, fun _ _ => tt).
exact (snd ef (h o inl) (k o inl)).
exact (snd eg (h o inr) (k o inr)).
Definition ooextendable_functor_sum
{A B A' B'} (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 ].
(** ** 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. *)
Definition extension_functor_coeq {B A f g B' A' f' g'}
{h : B -> B'} {k : A -> A'}
{p : k o f == f' o h} {q : k o g == g' o h}
{C : Coeq f' g' -> Type}
(ek : ExtendableAlong 1 k (C o coeq))
(eh : forall (u v : forall x : B', C (coeq (g' x))),
ExtendableAlong 1 h (fun x => u x = v x))
(s : forall x, C (functor_coeq h k p q x))
: ExtensionAlong (functor_coeq h k p q) C s.
(** We start by change the problem to involve [CylCoeq] with cofibrations. *)
set (C' := C o pr_cylcoeq p q).
set (s' x := pr_cyl_cylcoeq p q x # s x).
assert (e : ExtensionAlong (cyl_cylcoeq p q) C' s').
pose (ex := fst (extendable_equiv 1 C (pr_cylcoeq p q)) e.1).
apply (equiv_inj (transport C (pr_cyl_cylcoeq p q x))).
exact (apD _ (pr_cyl_cylcoeq p q x) @ ex.2 _ @ e.2 x).
(** 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. *)
pose (ea1 := fun u => (fst (cyl_extendable' 1 _ _ ek) u).1).
assert (eb'' : forall u v,
ExtendableAlong 1 cyl (fun x:Cyl h => DPath C' (cglue x) (u x) (v x))).
rapply extendable_postcompose'.
rapply (cancelL_extendable 1 _ cyl pr_cyl).
exact (eh (fun x => cglue x # u (cyr x)) (v o cyr)).
refine ((dp_compose (pr_cylcoeq p q) C _)^-1 oE _).
symmetry; srapply equiv_ds_fill_lr.
3:rapply ap_pr_cylcoeq_cglue.
all:srapply (transport (fun r => DPath C r _ _)).
3:exact (dp_inverse (dp_compose _ C _ (apD u (eissect pr_cyl x) : DPath _ _ _ _))).
4:exact (dp_inverse (dp_compose _ C _ (apD v (eissect pr_cyl x) : DPath _ _ _ _))).
1:change (fun y => pr_cylcoeq p q (coeq (functor_cyl p y)))
with (fun y => coeq (f := f') (g := g') (pr_cyl (functor_cyl p y))).
2:change (fun y => pr_cylcoeq p q (coeq (functor_cyl q y)))
with (fun y => coeq (f := f') (g := g') (pr_cyl (functor_cyl q y))).
all:refine ((ap_V _ (eissect pr_cyl x))^ @ _).
all: exact (ap_compose (fun x => pr_cyl (functor_cyl _ x)) coeq _).
pose (eb1 := fun u v w => (fst (cyl_extendable _ _ _ (eb'' u v)) w).1).
(** Now we construct an extension using Coeq-induction, and prove that it *is* an extension also using Coeq-induction. *)
srefine (_;_); srapply Coeq_ind.
rapply (dp_compose' _ _ (ap_cyl_cylcoeq_cglue p q b)).
exact (apD s' (cglue b)).
(** Since we're using cofibrations, this holds definitionally. *)
(** And this one is much simpler than it would be otherwise. *)
refine (dp_apD_compose' _ _ (ap_cyl_cylcoeq_cglue p q b) _ @ _).
nrapply Coeq_ind_beta_cglue.
(** Now we can easily iterate into higher extendability. *)
Definition extendable_functor_coeq (n : nat)
{B A f g B' A' f' g'}
{h : B -> B'} {k : A -> A'}
{p : k o f == f' o h} {q : k o g == g' o h}
{C : Coeq f' g' -> Type}
(ek : ExtendableAlong n k (C o coeq))
(eh : forall (u v : forall x : B', C (coeq (g' x))),
ExtendableAlong n h (fun x => u x = v x))
: ExtendableAlong n (functor_coeq h k p q) C.
revert C ek eh; simple_induction n n IH; intros C ek eh; [ exact tt | split ].
apply extension_functor_coeq.
exact (fst ek , fun _ _ => tt).
exact (fun u v => (fst (eh u v) , fun _ _ => tt)).
exact (snd ek (u o coeq) (v o coeq)).
exact (snd (eh (u o coeq o g') (v o coeq o g'))).
Definition ooextendable_functor_coeq
{B A f g B' A' f' g'}
{h : B -> B'} {k : A -> A'}
{p : k o f == f' o h} {q : k o g == g' o h}
{C : Coeq f' g' -> Type}
(ek : ooExtendableAlong k (C o coeq))
(eh : forall (u v : forall x : B', C (coeq (g' x))),
ooExtendableAlong h (fun x => u x = v x))
: ooExtendableAlong (functor_coeq h k p q) C
:= fun n => extendable_functor_coeq n (ek n) (fun u v => eh u v n).
(** Since extending at level [n.+1] into [C] implies extending at level [n] into path-types of [C], we get the following corollary. *)
Definition extendable_functor_coeq' (n : nat)
{B A f g B' A' f' g'}
{h : B -> B'} {k : A -> A'}
{p : k o f == f' o h} {q : k o g == g' o h}
{C : Coeq f' g' -> Type}
(ek : ExtendableAlong n k (C o coeq))
(eh : ExtendableAlong n.+1 h (C o coeq o g'))
: ExtendableAlong n (functor_coeq h k p q) C.
apply extendable_functor_coeq.
Definition ooextendable_functor_coeq'
{B A f g B' A' f' g'}
{h : B -> B'} {k : A -> A'}
{p : k o f == f' o h} {q : k o g == g' o h}
{C : Coeq f' g' -> Type}
(ek : ooExtendableAlong k (C o coeq))
(eh : ooExtendableAlong h (C o coeq o g'))
: ooExtendableAlong (functor_coeq h k p q) C
:= fun n => extendable_functor_coeq' n (ek n) (eh n.+1).