Timings for Lex.v
(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
Require Import HFiber Limits.Pullback Factorization Truncations.Core.
Require Import Modality Accessible Localization Descent Separated.
Local Open Scope path_scope.
Local Open Scope subuniverse_scope.
(** * Lex modalities *)
(** A lex modality is one that preserves finite limits, or equivalently pullbacks. Many equivalent characterizations of this can be found in Theorem 3.1 of RSS.
We choose as our definition that a lex modality to be a reflective subuniverse such that [O <<< O], which is close to (but not quite the same as) RSS Theorem 3.1 (xiii).
Note that since this includes [O << O] as a precondition, such an [O] must indeed be a modality (and since modalities coerce to reflective subuniverses, in the following notation [O] could be either an element of [ReflectiveSubuniverse] or of [Modality]). *)
Notation Lex O := (O <<< O).
(** ** Properties of lex modalities *)
(** We now show that lex modalities have all the other properties from RSS Theorem 3.1 (which are equivalent to lex-ness). All of them are simple specializations of properties from [Descent.v] to the case [O' = O] (although in the general case they are not known to be equivalent). *)
Context (O : Modality) `{Lex O}.
(** RSS Theorem 3.1 (i) *)
Definition isconnected_paths
{A : Type} `{IsConnected O A} (x y : A)
: IsConnected O (x = y)
:= OO_isconnected_paths O O x y.
(** RSS Theorem 3.1 (iii) *)
Definition conn_map_lex
{Y X : Type} `{IsConnected O Y, IsConnected O X} (f : Y -> X)
: IsConnMap O f
:= OO_conn_map_isconnected O O f.
(** RSS Theorem 3.1 (iv) *)
Definition isequiv_mapino_isconnected
{Y X : Type} `{IsConnected O Y, IsConnected O X}
(f : Y -> X) `{MapIn O _ _ f}
: IsEquiv f
:= OO_isequiv_mapino_isconnected O O f.
(** RSS Theorem 3.1 (vi) *)
Definition conn_map_functor_hfiber {A B C D : Type}
{f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
`{IsConnMap O _ _ h, IsConnMap O _ _ k}
(p : k o f == g o h) (b : B)
: IsConnMap O (functor_hfiber p b)
:= OO_conn_map_functor_hfiber O O p b.
(** RSS Theorem 3.1 (vii) *)
Definition ispullback_connmap_mapino_commsq
{A B C D : Type} {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
(p : k o f == g o h)
`{O_inverts O h, O_inverts O k, MapIn O _ _ f, MapIn O _ _ g}
: IsPullback p
:= OO_ispullback_connmap_mapino O O p.
(** RSS Theorem 3.1 (viii) *)
Global Instance conn_map_functor_hfiber_to_O
{Y X : Type} (f : Y -> X) (x : X)
: IsConnMap O (functor_hfiber (fun y => (to_O_natural O f y)^) x)
:= OO_conn_map_functor_hfiber_to_O O O f x.
Global Instance isequiv_O_functor_hfiber
{A B} (f : A -> B) (b : B)
: IsEquiv (O_functor_hfiber O f b).
apply (isequiv_O_rec_O_inverts O).
apply O_inverts_conn_map.
refine (conn_map_homotopic
O (functor_hfiber (fun x => (to_O_natural O f x)^) b)
_ _ _).
unfold functor_hfiber, functor_sigma.
Definition equiv_O_functor_hfiber
{A B} (f : A -> B) (b : B)
: O (hfiber f b) <~> hfiber (O_functor O f) (to O B b)
:= Build_Equiv _ _ (O_functor_hfiber O f b) _.
(** RSS Theorem 3.1 (ix) *)
Global Instance isequiv_path_O
{X : Type@{i}} (x y : X)
: IsEquiv (path_OO O O x y)
:= isequiv_path_OO O O x y.
Definition equiv_path_O {X : Type@{i}} (x y : X)
: O (x = y) <~> (to O X x = to O X y)
:= equiv_path_OO O O x y.
Definition equiv_path_O_to_O {X : Type} (x y : X)
: (equiv_path_O x y) o (to O (x = y)) == @ap _ _ (to O X) x y.
intros p; unfold equiv_path_O, equiv_path_OO, path_OO; cbn.
(** RSS Theorem 3.1 (x). This justifies the term "left exact". *)
Global Instance O_inverts_functor_pullback_to_O
{A B C : Type} (f : B -> A) (g : C -> A)
: O_inverts O (functor_pullback f g (O_functor O f) (O_functor O g)
(to O A) (to O B) (to O C)
(to_O_natural O f) (to_O_natural O g))
:= OO_inverts_functor_pullback_to_O O O f g.
Definition equiv_O_pullback {A B C : Type} (f : B -> A) (g : C -> A)
: O (Pullback f g) <~> Pullback (O_functor O f) (O_functor O g)
:= equiv_O_rec_O_inverts
O (functor_pullback f g (O_functor O f) (O_functor O g)
(to O A) (to O B) (to O C)
(to_O_natural O f) (to_O_natural O g)).
Definition O_functor_pullback
{A B C : Type} (f : B -> A) (g : C -> A)
: IsPullback (O_functor_square O _ _ _ _ (pullback_commsq f g)).
nrapply (isequiv_homotopic
(O_rec (functor_pullback _ _ _ _ _ _ _
(to_O_natural O f) (to_O_natural O g)))).
1: apply isequiv_O_rec_O_inverts; exact _.
1: intro x; apply O_rec_beta.
snrapply pullback_homotopic; intros [b [c e]]; cbn.
all: change (to (modality_subuniv O)) with (to O).
nrapply (to_O_natural O).
nrapply (to_O_natural O).
Open Scope long_path_scope.
lhs nrapply (concat_p_pp _ _ _ @@ 1).
rewrite to_O_natural_compose.
rewrite O_functor_homotopy_beta.
rhs_V nrapply concat_pp_p.
nrapply to_O_natural_compose.
Close Scope long_path_scope.
Definition diagonal_O_functor {A B : Type} (f : A -> B)
: diagonal (O_functor O f) == equiv_O_pullback f f o O_functor O (diagonal f).
apply O_indpaths; intros x.
refine (_ @ (ap _ (to_O_natural _ _ _))^).
refine (_ @ (O_rec_beta _ _)^).
unfold diagonal, functor_pullback, functor_sigma; cbn.
apply moveL_pV; exact (concat_1p_p1 _).
(** RSS Theorem 3.1 (xi) *)
Definition cancelL_conn_map
{Y X Z : Type} (f : Y -> X) (g : X -> Z)
`{IsConnMap O _ _ (g o f)} `{IsConnMap O _ _ g}
: IsConnMap O f
:= OO_cancelL_conn_map O O f g.
(** RSS Theorem 3.1 (xii) *)
Global Instance conn_map_O_inverts
{A B : Type} (f : A -> B) `{O_inverts O f}
: IsConnMap O f
:= conn_map_OO_inverts O O f.
(** RSS Theorem 3.1 (xiii) *)
Definition modal_over_connected_isconst_lex
(A : Type) `{IsConnected O A}
(P : A -> Type) `{forall x, In O (P x)}
: {Q : Type & In O Q * forall x, Q <~> P x}.
pose proof (O_inverts_isconnected O (fun _:A => tt)).
exists (OO_descend_O_inverts O O (fun _:A => tt) P tt); split.
apply OO_descend_O_inverts_inO.
intros; nrapply OO_descend_O_inverts_beta.
(** RSS Theorem 3.11 (iii): in the accessible case, the universe is modal. *)
Global Instance inO_typeO_lex `{Univalence} `{IsAccRSU O}
: In (lift_accrsu O) (Type_ O)
:= _.
(** Part of RSS Corollary 3.9: lex modalities preserve [n]-types for all [n]. This is definitely not equivalent to lex-ness, since it is true for the truncation modalities that are not lex. But it is also not true of all modalities; e.g. the shape modality in a cohesive topos can take 0-types to [oo]-types. With a little more work, this can probably be proven without [Funext]. *)
Global Instance istrunc_O_lex `{Funext}
{n : trunc_index} {A : Type} `{IsTrunc n A}
: IsTrunc n (O A).
generalize dependent A; simple_induction n n IHn; intros A ?.
(** Already proven for all modalities. *)
refine (O_ind (fun x => forall y, IsTrunc n (x = y)) _); intros x.
refine (O_ind (fun y => IsTrunc n (to O A x = y)) _); intros y.
refine (istrunc_equiv_istrunc _ (equiv_path_O x y)).
(** ** Equivalent characterizations of lex-ness *)
(** We will not prove that *all* of the above properties from RSS Theorem 3.1 are equivalent to lex-ness, but we will do it for some of them. *)
(** RSS 3.1 (xiii) implies lexness *)
Definition lex_from_modal_over_connected_isconst
(H : forall (A : Type) (A_isC : IsConnected O A)
(P : A -> Type) (P_inO : forall x, In O (P x)),
{Q : Type & In O Q * forall x, Q <~> P x})
: Lex O.
intros A; unshelve econstructor; intros P P_inO.
all:pose (Q := fun z:O A => H (hfiber (to O A) z) _ (P o pr1) _).
exact (fun z => (Q z).1).
exact (fun z => fst (Q z).2).
exact (snd (Q (to O A x)).2 (x;1)).
(** RSS 3.11 (iii), the universe is modal, implies lex-ness *)
Definition lex_from_inO_typeO `{IsAccRSU O} `{In (lift_accrsu O) (Type_ O)}
: Lex O.
apply (O_lex_leq_inO_TypeO O O).
(** RSS Theorem 3.1 (xi) implies lex-ness *)
Definition lex_from_cancelL_conn_map
(cancel : forall {Y X Z : Type} (f : Y -> X) (g : X -> Z),
(IsConnMap O (g o f)) -> (IsConnMap O g)
-> IsConnMap O f)
: Lex O.
apply lex_from_modal_over_connected_isconst; intros.
exists (O {x:A & P x}); split; [ exact _ | intros x; symmetry ].
refine (Build_Equiv _ _ (fun p => to O _ (x ; p)) _).
nrefine (isequiv_conn_map_ino O _).
revert x; apply conn_map_fiber.
nrefine (cancel _ _ _ _ (fun z:{x:A & O {x : A & P x}} => z.2) _ _).
1: clear cancel; exact _.
refine (isconnected_equiv' O A _ _).
refine (equiv_adjointify (fun x => ((x ; z) ; 1))
(fun y => y.1.1) _ _).
intros [[x y] []]; reflexivity.
(** RSS Theorem 3.1 (iii) implies lex-ness *)
Definition lex_from_conn_map_lex
(H : forall A B (f : A -> B),
(IsConnected O A) -> (IsConnected O B) ->
IsConnMap O f)
: Lex O.
apply lex_from_cancelL_conn_map.
intros Y X Z f g gfc gc x.
pose (h := @functor_hfiber Y Z X Z (g o f) g f idmap (fun a => 1%path)).
assert (cc := H _ _ (h (g x)) (gfc (g x)) (gc (g x))).
refine (isconnected_equiv' O _ _ (cc (x;1))).
subst h; unfold functor_hfiber, functor_sigma; cbn.
refine (_ oE (equiv_sigma_assoc _ _)^-1).
apply equiv_functor_sigma_id; intros y; cbn.
refine (_ oE (equiv_functor_sigma_id _)).
2:intros; symmetry; apply equiv_path_sigma.
refine (_ oE equiv_sigma_symm _).
apply equiv_sigma_contr; intros p.
refine (contr_equiv' { p : g (f y) = g (f y) & p = 1%path } _).
apply equiv_functor_sigma_id; intros p; cbn.
exact (concat_1p _ @ ap_idmap _).
(** RSS Theorem 3.1 (i) implies lex-ness *)
Definition lex_from_isconnected_paths
(H : forall (A : Type) (Ac : IsConnected O A) (x y : A),
IsConnected O (x = y))
: Lex O.
apply lex_from_conn_map_lex.
rapply isconnected_sigma.
(** RSS Theorem 3.1 (iv) implies lex-ness *)
Definition lex_from_isequiv_ismodal_isconnected_types
(H : forall A B (f : A -> B),
(IsConnected O A) -> (IsConnected O B) ->
(MapIn O f) -> IsEquiv f)
: Lex O.
apply lex_from_conn_map_lex.
apply (conn_map_homotopic O _ _ (fact_factors (image O f))).
apply conn_map_compose; [ exact _ | ].
apply H; [ | exact _ | exact _ ].
apply isconnected_conn_map_to_unit.
apply (cancelR_conn_map O (factor1 (image O f)) (const_tt _)).
(** RSS Theorem 3.1 (vii) implies lex-ness *)
Definition lex_from_ispullback_connmap_mapino_commsq
(H : forall {A B C D}
(f : A -> B) (g : C -> D) (h : A -> C) (k : B -> D),
(IsConnMap O f) -> (IsConnMap O g) ->
(MapIn O h) -> (MapIn O k) ->
forall (p : k o f == g o h), IsPullback p)
: Lex O.
apply lex_from_isequiv_ismodal_isconnected_types.
specialize (H A Unit B Unit (const_tt _) (const_tt _) f idmap _ _ _ _
(fun _ => 1)).
unfold IsPullback, pullback_corec in H.
refine (@isequiv_compose _ _ _ H _ (fun x => x.2.1) _).
refine (@isequiv_compose _ {b:Unit & B}
(functor_sigma idmap (fun a => pr1))
_ _ pr2 _).
refine (@isequiv_compose _ _ (equiv_sigma_prod0 Unit B)
_ _ snd _).
apply (equiv_isequiv (prod_unit_l B)).
(** ** Lex reflective subuniverses *)
(** A reflective subuniverse that preserves fibers is in fact a modality (and hence lex). *)
Definition ismodality_isequiv_O_functor_hfiber (O : ReflectiveSubuniverse)
(H : forall {A B : Type} (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b))
: IsModality O.
intros A'; rapply reflectsD_from_inO_sigma.
pose (g := O_rec pr1 : O {x : A & B x} -> A).
transparent assert (p : (forall x, g (to O _ x) = x.1)).
intros x; subst g; apply O_rec_beta.
apply isequiv_contr_map; intros x.
snrefine (contr_equiv' _ (hfiber_hfiber_compose_map _ g x)).
unfold hfiber_compose_map.
transparent assert (h : (hfiber (@pr1 A B) (g x) <~> hfiber g (g x))).
refine (_ oE equiv_to_O O _).
refine (_ oE Build_Equiv _ _
(O_functor_hfiber O (@pr1 A B) (g x)) _).
apply equiv_functor_sigma_id.
refine (_ oE (equiv_moveR_equiv_V _ _)).
revert y; apply O_indpaths; intros [a q]; cbn.
refine (_ @ (O_rec_beta _ _)^).
refine (isequiv_homotopic (h oE equiv_hfiber_homotopic _ _ p (g x)) _).
unfold functor_sigma; cbn.
refine (path_sigma' _ 1 _).
rewrite O_indpaths_beta; cbn.
unfold moveL_equiv_V, moveR_equiv_V.
Open Scope long_path_scope.
(* work around bug 4533 *)
(* Even though https://github.com/coq/coq/issues/4533 is closed, this is still needed. *)
rewrite !ap_pp, !concat_p_pp, !ap_V.
rewrite concat_pp_p; apply moveR_Vp.
rewrite <- !(ap_compose (to O A) (to O A)^-1).
Local Transparent eissect.
(* work around bug 4533 *)
Close Scope long_path_scope.
(** ** Lexness via generators *)
(** Here the characterization of when an accessible presentation yields a lex modality from Anel-Biederman-Finster-Joyal ("Higher Sheaves and Left-Exact Localizations of ∞-Topoi", arXiv:2101.02791): it's enough for path spaces of the generators to be connected. *)
Definition lex_gen `{Univalence} (O : Modality) `{IsAccModality O}
(lexgen : forall (i : ngen_indices (acc_ngen O)) (x y : ngen_type (acc_ngen O) i),
IsConnected O (x = y))
: Lex O.
srapply lex_from_inO_typeO; [ exact _ | intros i ].
rapply ooextendable_TypeO_from_extension; intros P; srefine (_;_).
1:intros; exists (forall x, P x); exact _.
assert (wc : forall y z, P y <~> P z).
(** Here we use the hypothesis [lexgen] (typeclass inference finds it automatically). *)
refine (pr1 (isconnected_elim O _ (@equiv_transport _ P y z))).
intros x; apply path_TypeO, path_universe_uncurried.
refine (equiv_adjointify (fun f => f x) (fun u y => wc x y ((wc x x)^-1 u)) _ _).
intros f; apply path_forall; intros y; apply moveR_equiv_M.
destruct (isconnected_elim O _ (fun y => (wc x y)^-1 (f y))) as [z p].
(** ** n-fold separation *)
(** A type is [n]-[O]-separated, for n >= -2, if all its (n+2)-fold iterated identity types are [O]-modal. Inductively, this means that it is (-2)-O-separated if it is O-modal, and (n+1)-O-separated if its identity types are n-O-separated. *)
Fixpoint nSep (n : trunc_index) (O : Subuniverse) : Subuniverse
:= match n with
| -2 => O
| n.+1 => Sep (nSep n O)
end.
(** The reason for indexing this notion by a [trunc_index] rather than a [nat] is that when O is lex, a type is n-O-separated if and only if its O-unit is an n-truncated map. *)
Definition nsep_iff_trunc_to_O (n : trunc_index) (O : Modality) `{Lex O} (A : Type)
: In (nSep n O) A <-> IsTruncMap n (to O A).
revert A; induction n as [|n IHn]; intros A; split; intros ?.
apply contr_map_isequiv; rapply isequiv_to_O_inO.
apply (inO_equiv_inO (O A) (to O A)^-1).
apply istruncmap_from_ap; intros x y.
pose (i := fst (IHn (x = y)) _).
apply istruncmap_mapinO_tr, (mapinO_homotopic _ _ (equiv_path_O_to_O O x y)).
apply (snd (IHn (x = y))).
pose (i := istruncmap_ap n (to O A) x y).
apply mapinO_tr_istruncmap in i.
apply istruncmap_mapinO_tr, (mapinO_homotopic _ ((equiv_path_O O x y)^-1 o (@ap _ _ (to O A) x y))).
intros p; apply moveR_equiv_V; symmetry; apply equiv_path_O_to_O.
(* This speeds up the next line. *)