Timings for Colimit_Flattening.v
Require Import Diagrams.Diagram.
Require Import Diagrams.Graph.
Require Import Diagrams.Cocone.
Require Import Diagrams.DDiagram.
Require Import Colimits.Colimit.
Local Open Scope path_scope.
(** * Flattening lemma *)
(** This file provides a proof of the flattening lemma for colimits. This lemma describes the type [sig E'] when [E' : colimit D -> Type] is a type family defined by recursion on a colimit. The flattening lemma in the case of coequalizers is presented in section 6.12 of the HoTT book and is in Colimits/Coeq.v. *)
(** TODO: See whether there's a straightforward way to deduce the flattening lemma for general colimits from the version for coequalizers. *)
(** ** Equifibered diagrams *)
Context `{Univalence} {G : Graph} (D : Diagram G)
(E : DDiagram D) `(Equifibered _ _ E).
Let E_f {i j : G} (g : G i j) (x : D i) : E (i; x) -> E (j; (D _f g) x)
:= @arr _ E (i; x) (j; D _f g x) (g; 1).
(** Now, given an equifibered diagram and using univalence, one can define a type family [E' : colimit D -> Type] by recursion on the colimit. *)
Definition E' : Colimit D -> Type.
simple refine (Build_Cocone _ _).
exact (fun i x => E (i; x)).
srapply (path_universe (E_f _ _)).
Definition transport_E' {i j : G} (g : G i j) (x : D i) (y : E (i; x))
: transport E' (colimp i j g x) (E_f g x y) = y.
refine (transport_idmap_ap _ _ _ @ _).
srefine (transport2 idmap _ _ @ _).
2: apply Colimit_rec_beta_colimp; cbn.
apply (moveR_transport_V idmap).
symmetry; apply transport_path_universe.
Definition transport_E'_V {i j : G} (g : G i j) (x : D i) (y : E (i; x))
: transport E' (colimp i j g x)^ y = E_f g x y.
Definition transport_E'_V_E' {i j : G} (g : G i j) (x : D i) (y : E (i; x))
: transport_E' g x y
= ap (transport E' (colimp i j g x)) (transport_E'_V g x y)^
@ transport_pV E' (colimp i j g x) y.
rewrite moveR_transport_V_V, inv_V.
symmetry; apply ap_transport_transport_pV.
(** ** Main result *)
(** We define the cocone over the sigma diagram to [sig E']. *)
Definition cocone_E' : Cocone (diagram_sigma E) (sig E').
srapply Build_Cocone; cbn.
exists (colim i w.1); cbn.
(** And we directly prove that it is universal. We break the proof into parts to slightly speed it up. *)
Local Opaque path_sigma ap11.
Local Definition cocone_extends Z: Cocone (diagram_sigma E) Z -> ((sig E') -> Z).
intros [x y]; revert x y.
srapply Colimit_ind; cbn.
intros i x y; exact (q i (x; y)).
refine (transport_arrow_toconst _ _ _ @ _).
refine (_ @ qq i j g (x; y)).
refine (path_sigma' _ 1 _); cbn.
Local Definition cocone_isretr Z
: cocone_postcompose cocone_E' o cocone_extends Z == idmap.
rewrite concat_1p, concat_p1.
cbn; rewrite ap_path_sigma.
rewrite Colimit_ind_beta_colimp.
rewrite ap10_path_forall.
rewrite concat_pp_p, concat_V_pp.
refine (_ @ concat_1p _).
refine (concat_p_pp _ _ _ @ _).
match goal with |- ap _ ?X @ _ = _ => set (p := X) end.
assert (r : transport_E'_V g x y = p^).
exact (moveL_transport_V_V E' _ _ _ _)^.
Local Definition cocone_issect Z
: cocone_extends Z o cocone_postcompose cocone_E' == idmap.
refine (transport_forall _ _ _ @ _).
rewrite transport_paths_FlFr.
refine ((1 @@ _ @@ 1) @ (concat_p1 _ @@ 1) @ concat_Vp _).
match goal with |- transportD E' ?C _ _ _ = _ =>
rewrite (transportD_is_transport _ (fun w => C w.1 w.2)) end.
rewrite transport_paths_FlFr.
rewrite Colimit_ind_beta_colimp.
rewrite ap10_path_forall.
rewrite concat_pp_p, concat_V_pp.
rewrite ap11_is_ap10_ap01.
rewrite (ap_compose (fun y => (colim j ((D _f g) x); y)) f).
rewrite (ap_compose (fun x0 : exists x0 : D j, E (j; x0)
=> (colim j (pr1 x0); pr2 x0)) f).
refine (_ @ concat_pp_p _ _ _).
match goal with |- _ = (ap ?ff ?pp1 @ ?pp2) @ ?pp3
=> set (p1 := pp1) end.
assert (p1eq : p1 = ap (transport E' (colimp i j g x)^)
(transport_pV E' (colimp i j g x) y)^).
1: srapply moveL_transport_V_1.
1: nrapply inverse2; snrapply transport_VpV.
rewrite p1eq; clear p1eq p1.
rewrite <- ap_compose; cbn.
rewrite (ap_path_sigma (fun x => E (j; x))
(fun x y => (colim j x; y))).
cbn; rewrite !concat_p1, concat_pp_p, ap_V.
match goal with |- ?pp1 @ _ = ?pp2 @ _
=> set (p1 := pp1);
change pp2 with (path_sigma' E' 1
(transport_E'_V g x
(transport E' (colimp i j g x) (transport E' (colimp i j g x)^ y)))) end.
assert (p1eq : p1 = path_sigma' E' 1 (transport_Vp _ _ _)).
rewrite (ap_compose (transport E' (colimp i j g x)^)
(fun v => (colim j ((D _f g) x); v))).
f_ap; set (p := colimp i j g x).
rewrite p1eq; clear p1eq p1.
rewrite <- !path_sigma_pp_pp'; f_ap.
rewrite concat_p1, concat_pp_p.
rewrite <- ap_V, <- ap_pp.
refine (ap (transport E' (colimp i j g x)) _).
refine ((transport_E'_V _ _ _)^ @ _).
refine (ap _ (transport_pV _ _ _)).
set (e := transport E' (colimp i j g x)
(transport E' (colimp i j g x)^ y)).
rewrite ap_pp, <- ap_compose.
refine (_ @ (transport_E'_V_E' _ _ _)^).
refine (_ @ (transport_pVp _ _ _)^).
(* TODO: a little slow, 0.40s *)
Global Instance unicocone_cocone_E' : UniversalCocone cocone_E'.
srapply Build_UniversalCocone.
intro Z; srapply isequiv_adjointify.
exact (cocone_extends Z).
(** The flattening lemma follows by colimit unicity. *)
Definition flattening_lemma : Colimit (diagram_sigma E) <~> sig E'.
3: apply iscolimit_colimit.
apply unicocone_cocone_E'.
(* TODO: ending the section is a bit slow (0.2s). But simply removing the Section (and changing "Let" to "Local Definition") causes the whole file to be much slower. It should be possible to remove the section without making the whole file slower. *)