Timings for Topological.v
(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
Require Import Extensions HoTT.Truncations.
Require Import Accessible Lex Nullification.
Local Open Scope path_scope.
(** * Topological localizations *)
(** A topological localization -- or, as we will say, a topological nullification -- is a nullification at a family of hprops, or more generally an accessible modality whose generators of accessibility are all hprops. This is not quite the same as Lurie's definition: in Higher Topos Theory, a topological localization is an accessible *left exact* localization at a pullback-stable class generated by a set of monomorphisms. "Pullback-stable class generated by" is roughly incorporated into our internal notion of accessibility, so the main new difference here is that when the generation is internal in this way, the localization at a family of hprops is *automatically* left exact. *)
Notation Topological O := (forall i, IsHProp (acc_ngen O i)).
(** ** Topological modalities are lex *)
(** We prove left-exactness by proving that the universe of modal types is modal, using univalence. It's unclear whether univalence is necessary or not in general; in one special case (open modalities) funext suffices. But it's plausible that it would be necessary in general, because lex-ness of nullification is a statement about the path-spaces of a HIT, and characterizing those in any way usually requires some amount of univalence. *)
Global Instance lex_topological `{Univalence}
(O : Modality) `{IsAccModality O} `{Topological O}
: Lex O.
snrapply lex_from_inO_typeO; [ exact _ | intros i ].
apply ((equiv_ooextendable_isequiv _ _)^-1%equiv).
srapply isequiv_adjointify; cbn.
refine ((forall a, B a) ; _).
apply path_arrow; intros a.
apply path_TypeO, path_universe_uncurried.
simple refine (equiv_adjointify _ _ _ _).
exact (transport B (path_ishprop a a') b).
refine (transport2 B (path_contr _ 1) b).
apply path_forall; intros a'.
apply path_arrow; intros [].
apply path_TypeO, path_universe_uncurried.
pose (e := isequiv_ooextendable _ _
(fst (inO_iff_isnull O (B tt)) (inO_TypeO (B tt)) i)).
unfold composeD in e; simpl in e.
refine (_ oE (Build_Equiv _ _ _ e)^-1).
exact (equiv_contr_forall _).
Global Instance lex_nullification `{Univalence}
(S : NullGenerators) `{forall i, IsHProp (S i)}
: Lex (Nul S).
(** ** Lex modalities generated by n-types are topological *)
(** For [n >= 0], nullification at a family of [n]-types need not be lex. For instance, the (-1)-truncation is nullification at [Bool]. However, if the nullification at a family of [n]-types *is* lex, then it is topological. *)
(** This is kind of annoying to prove, not just because the proof is fiddly, but because we have to pass back and forth between different generating families for the "same" modality. It's a bit easier to prove it about nullifications than about arbitrary accessible lex modalities. *)
Definition topological_lex_trunc_acc `{Funext}
(B : NullGenerators) {Olex : Lex (Nul B)}
(n : trunc_index) (gtr : forall a, IsTrunc n (ngen_type B a))
: { D : NullGenerators &
(forall c, IsHProp (ngen_type D c)) *
(Nul D <=> Nul B) }.
exists (Build_NullGenerators Empty (fun _ => Unit)).
split; [ exact _ | split; intros X _; [ | intros [] ] ].
apply ooextendable_equiv, isequiv_contr_contr.
pose (OeqB := reflexive_O_eq O : O <=> (Nul B)).
change (Nul B) with O in Olex.
induction n; intros B OeqB gtr.
exists B; split; [ assumption | reflexivity ].
pose (A := ngen_indices B).
pose (C := A + { a:A & B(a) * B(a) }).
pose (D := Build_NullGenerators
C (fun c:C => match c with
| inl a => merely (B a)
| inr (a ; (b1, b2)) => (b1 = b2)
end : Type)).
assert (Dtrunc : forall c:C, IsTrunc n.+1 (D c)).
intros [a | [a [b1 b2]]]; [ cbn | exact _ ].
(* Because [trunc_hprop] can't be used as an idmap... *)
assert (OeqD : O <=> (Nul D)).
assert (Bc : forall a:A, IsConnected O (B a)).
rapply (@isconnected_O_leq O (Nul B)).
exact (isconnected_acc_ngen (Nul B) a).
apply (ooextendable_const_isconnected_inO O);
[ destruct c as [a | [a [b1 b2]]] | exact X_inO ].
apply isconnected_from_elim_to_O.
destruct (isconnected_elim O (O (merely (B a)))
(fun b => to O _ (tr b)))
as [x h].
exists x; intros y; cbn in y.
rapply isconnected_paths.
intros Dnull; rapply (@inO_leq (Nul B) O).
apply ((equiv_ooextendable_isequiv
(unit_name X) (fun _:B a => tt))^-1).
apply isequiv_contr_map; intros f; cbn in f.
refine (contr_equiv' { x:X & forall u:B a, x = f u } _).
refine (equiv_functor_sigma' (equiv_unit_rec X) _).
intros x; unfold composeD; cbn.
refine ((isconnected_elim (Nul D) (A := D (inl a)) _ _).1).
rapply isconnected_acc_ngen.
assert (bc : IsConnMap (Nul D) (unit_name b)).
apply (isconnected_equiv (Nul D) (b = x)
(equiv_contr_sigma _)^-1).
rapply (isconnected_acc_ngen (Nul D) (inr (a;(b,x)))).
pose (p := conn_map_elim (Nul D) (unit_name b)
(fun u => f b = f u) (fun _ => 1)).
apply (Build_Contr _ (f b ; p)); intros [x q].
refine (path_sigma' _ (q b)^ _); apply path_forall.
refine (conn_map_elim (Nul D) (unit_name b) _ _); intros [].
rewrite transport_forall_constant, transport_paths_l, inv_V.
rewrite (conn_map_comp (Nul D) (unit_name b)
(fun u:B a => f b = f u)
(fun _ => 1) tt : p b = 1).
destruct (IHn D OeqD _) as [E [HE EeqD]].
exists E; split; [ exact HE | ].
refine (transitivity EeqD _).
refine (transitivity _ OeqB).