Skip to content

Commit

Permalink
Merge pull request #1789 from jdchristensen/colimit-flattening
Browse files Browse the repository at this point in the history 
Speed up Colimit_Flattening
  • Loading branch information
@jdchristensen
jdchristensen authored Oct 20, 2023
2 parents ca9ef4b + 571a37b commit e26ac2c
Showing 1 changed file with 134 additions and 123 deletions.
257 changes: 134 additions & 123 deletions theories/Colimits/Colimit_Flattening.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ Local Open Scope path_scope.

(** * Flattening lemma *)

(** This file provide 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 recusrion on a colimit. *)
(** 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 W-types is presented in section 6.12 of the HoTT book. *)
(** A good intuition is given by the pushout's case (see above). *)

Expand All @@ -23,7 +23,7 @@ Section Flattening.
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 recusrion on the colimit. *)
(** 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.
Proof.
Expand Down Expand Up @@ -79,134 +79,144 @@ Section Flattening.
+ apply transport_E'.
Defined.

(** And we directly prove than it is universal. *)
(** And we directly prove that it is universal. We break the proof into parts to slightly speed it up. *)

Local Opaque path_sigma ap11.

(** TODO: Make this faster! *)
Local Definition cocone_extends Z: Cocone (diagram_sigma E) Z -> ((sig E') -> Z).
Proof.
intros [q qq]; cbn in *.
intros [x y]; revert x y.
srapply Colimit_ind; cbn.
+ intros i x y; exact (q i (x; y)).
+ intros i j g x; cbn.
funext y.
refine (transport_arrow_toconst _ _ _ @ _).
refine (_ @ qq i j g (x; y)).
cbn; f_ap.
refine (path_sigma' _ 1 _); cbn.
apply transport_E'_V.
Defined.

Local Definition cocone_isretr Z
: cocone_postcompose cocone_E' o cocone_extends Z == idmap.
Proof.
intros [q qq].
srapply path_cocone.
+ intros i x; reflexivity.
+ intros i j g [x y].
rewrite concat_1p, concat_p1.
cbn; rewrite ap_path_sigma.
simpl.
rewrite Colimit_ind_beta_colimp.
rewrite ap10_path_forall.
rewrite concat_pp_p, concat_V_pp.
refine (_ @ concat_1p _).
refine (concat_p_pp _ _ _ @ _).
refine (_ @@ 1).
match goal with |- ap _ ?X @ _ = _ => set (p := X) end.
assert (r : transport_E'_V g x y = p^).
{ subst p.
exact (moveL_transport_V_V E' _ _ _ _)^. }
rewrite r; clear r.
destruct p.
reflexivity.
Defined. (* 0.1s *)

Local Definition cocone_issect Z
: cocone_extends Z o cocone_postcompose cocone_E' == idmap.
Proof.
intro f.
funext [x y].
revert x y.
srapply Colimit_ind.
+ cbn; reflexivity.
+ intros i j g x; cbn.
funext y.
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.
lhs rapply concat_pp_p.
apply moveR_Vp.
apply equiv_1p_q1.
rewrite ap_path_sigma.
rewrite Colimit_ind_beta_colimp.
rewrite ap10_path_forall.
simpl.
rewrite concat_pp_p, concat_V_pp.
rewrite ap11_is_ap10_ap01.
cbn.
rewrite concat_1p.
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).
rewrite <- ! (ap_pp f).
apply (ap (ap 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)^).
{ subst p1; clear.
etransitivity.
1: srapply moveL_transport_V_1.
etransitivity.
1: nrapply inverse2; snrapply transport_VpV.
symmetry; apply ap_V. }
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.
apply moveL_Vp.
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 _ _ _)).
{ subst p1.
rewrite <- ap_exist.
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).
clear; symmetry.
apply transport_VpV. }
rewrite p1eq; clear p1eq p1.
rewrite <- !path_sigma_pp_pp'; f_ap.
rewrite concat_p1, concat_pp_p.
refine (1 @@ _).
apply moveL_Mp.
rewrite <- ap_V, <- ap_pp.
srefine (_ @ _).
- refine (ap (transport E' (colimp i j g x)) _).
refine ((transport_E'_V _ _ _)^ @ _).
refine (ap _ (transport_pV _ _ _)).
- f_ap.
refine (1 @@ _).
apply transport_VpV.
- 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 (1 @@ _).
subst e.
refine (_ @ (transport_pVp _ _ _)^).
rewrite ap_compose.
f_ap; symmetry.
apply transport_VpV.
Defined. (* TODO: a little slow, 0.40s *)

Global Instance unicocone_cocone_E' : UniversalCocone cocone_E'.
Proof.
srapply Build_UniversalCocone.
intro Z; srapply isequiv_adjointify.
- intros [q qq]; cbn in *.
intros [x y]; revert x y.
srapply Colimit_ind; cbn.
+ intros i x y; exact (q i (x; y)).
+ intros i j g x; cbn.
funext y.
refine (transport_arrow_toconst _ _ _ @ _).
refine (_ @ qq i j g (x; y)).
cbn; f_ap.
refine (path_sigma' _ 1 _); cbn.
apply transport_E'_V.
- intros [q qq].
srapply path_cocone.
+ intros i x; reflexivity.
+ intros i j g [x y].
rewrite concat_1p, concat_p1.
cbn; rewrite ap_path_sigma.
cbn; rewrite Colimit_ind_beta_colimp.
rewrite ap10_path_forall.
hott_simpl.
refine (_ @ concat_1p _).
refine (_ @@ 1).
match goal with |- ap _ ?X @ _ = _ => set X end.
assert (transport_E'_V g x y = p^).
{ subst p.
exact (moveL_transport_V_V E' _ _ _ _)^. }
rewrite X.
clearbody p; clear.
set (E_f g x y) in *.
destruct p.
reflexivity.
- intro f.
funext [x y].
revert x y; cbn.
srapply Colimit_ind; cbn.
+ reflexivity.
+ intros i j g x; cbn.
funext y.
rewrite transport_forall; cbn.
rewrite transport_paths_FlFr.
match goal with |- (_ @ ?pp) @ _ = _ => set pp end.
cbn in p.
assert (p = 1).
{ subst p.
match goal with |- transportD E' ?C _ _ _ = _ => set (C2:=C) end.
rewrite (transportD_is_transport _ (fun w => C2 w.1 w.2)).
subst C2; cbn.
rewrite transport_paths_FlFr.
rewrite concat_p1.
apply moveR_Vp.
rewrite concat_p1.
rewrite ap_path_sigma.
cbn.
rewrite Colimit_ind_beta_colimp.
rewrite ap10_path_forall.
hott_simpl.
rewrite ap11_is_ap10_ap01.
cbn.
rewrite concat_1p.
rewrite (ap_compose (fun y => (colim j ((D _f g) x); y)) f).
cbn.
rewrite (ap_compose (fun x0 : exists x0 : D j, E (j; x0)
=> (colim j (pr1 x0); pr2 x0)) f).
rewrite <- ! (ap_pp f).
apply (ap (ap f)).
match goal with |- _ = (ap ?ff ?pp1 @ ?pp2) @ ?pp3
=> set (p1 := pp1) end.
assert (p1 = ap (transport E' (colimp i j g x)^)
(transport_pV E' (colimp i j g x) y)^).
{ subst p1; clear.
etransitivity.
1: srapply moveL_transport_V_1.
etransitivity.
{ srapply inverse2.
2: srapply transport_VpV. }
symmetry; apply ap_V. }
rewrite X; clear X 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.
apply moveL_Vp.
match goal with |- ?pp1 @ _ = ?pp2 @ _
=> set (p1 := pp1); set (p2 := pp2) end; cbn in *.
assert (p1 = path_sigma' E' 1 (transport_Vp _ _ _)).
{ subst p1.
rewrite <- ap_exist.
rewrite (ap_compose (transport E' (colimp i j g x)^)
(fun v => (colim j ((D _f g) x); v))).
f_ap; set (colimp i j g x).
clear; symmetry.
apply transport_VpV. }
rewrite X; clear p1 X.
assert (p2 = path_sigma' E' 1 (transport_E'_V _ _ _))
by reflexivity.
rewrite X; clear p2 X.
rewrite <- !path_sigma_pp_pp'; f_ap.
rewrite concat_p1, concat_pp_p.
refine (1 @@ _).
apply moveL_Mp.
rewrite <- ap_V, <- ap_pp.
srefine (_ @ _).
- refine (ap (transport E' (colimp i j g x)) _).
refine ((transport_E'_V _ _ _)^ @ _).
refine (ap _ (transport_pV _ _ _)).
- f_ap.
refine (1 @@ _).
apply transport_VpV.
- set (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 (1 @@ _).
subst e.
refine (_ @ (transport_pVp _ _ _)^).
rewrite ap_compose.
f_ap; symmetry.
apply transport_VpV. }
rewrite X; simpl; hott_simpl.
- exact (cocone_extends Z).
- exact (cocone_isretr Z).
- exact (cocone_issect Z).
Defined.

(** The flattening lemma follows by colimit unicity. *)
Expand All @@ -220,3 +230,4 @@ Section Flattening.
Defined.

End Flattening.
(* 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. *)

0 comments on commit e26ac2c

Please sign in to comment.