Timings for Accessible.v
(* -*- mode: coq; mode: visual-line -*- *)
(** * Accessible subuniverses and modalities *)
Require Import HoTT.Basics HoTT.Types.
Require Import Extensions NullHomotopy.
Local Open Scope nat_scope.
Local Open Scope path_scope.
(** ** Accessible reflective subuniverses *)
(** An accessible reflective subuniverse is one that is the localization at a small family of maps. Accessibility is necessary for some constructions, and in practice it's a reasonable hypothesis that includes most examples (though a few examples, such as double negation, may only be accessible if we assume propositional resizing).
We now give the basic definitions related to accessibility, using [ooExtendableAlong] as our notion of equivalence as we did with reflective subuniverses. The actual construction of a reflective subuniverse by localization will be in [Localization]. *)
Record LocalGenerators@{a} :=
{ lgen_indices : Type@{a} ;
lgen_domain : lgen_indices -> Type@{a} ;
lgen_codomain : lgen_indices -> Type@{a} ;
lgenerator : forall i, lgen_domain i -> lgen_codomain i
}.
Coercion lgenerator : LocalGenerators >-> Funclass.
(** We put this definition in a module so that no one outside of this file will use it accidentally. It will be redefined in [Localization] to refer to the localization reflective subuniverse, which is judgmentally the same but will also pick up typeclass inference for [In]. *)
Module Import IsLocal_Internal.
Definition IsLocal f X :=
(forall (i : lgen_indices f), ooExtendableAlong (f i) (fun _ => X)).
Class IsAccRSU@{a i} (O : Subuniverse@{i}) :=
{
acc_lgen : LocalGenerators@{a} ;
inO_iff_islocal : forall (X : Type@{i}),
(** We call [iff] explicitly to control the number of universe parameters. *)
iff@{i i i} (In O X) (IsLocal acc_lgen X) ;
}.
Arguments acc_lgen O {_}.
Arguments inO_iff_islocal O {_} X.
Global Instance O_inverts_generators {O : ReflectiveSubuniverse} `{IsAccRSU O}
(i : lgen_indices (acc_lgen O))
: O_inverts O (acc_lgen O i).
pose (ext_dom := fst (inO_iff_islocal O (O (lgen_domain (acc_lgen O) i))) _).
pose (ext_cod := fst (inO_iff_islocal O (O (lgen_codomain (acc_lgen O) i))) _).
simple refine (isequiv_adjointify _ _ _ _).
exact ((fst (ext_dom i 1%nat) (to O _)).1).
apply O_indpaths; intros x; simpl.
refine ((fst (snd (ext_cod i 2)
(fun x => O_functor O (acc_lgen O i)
((fst (ext_dom i 1%nat) (to O _)).1 x))
_) _).1 x); intros a.
rewrite ((fst (ext_dom i 1%nat) (to O _)).2 a).
apply O_indpaths; intros x; simpl.
rewrite (to_O_natural O (acc_lgen O i) x).
apply ((fst (ext_dom i 1%nat) (to O _)).2 x).
(** The construction of the localization reflective subuniverse for any family of maps will be in [Localization]. *)
(** ** Accessible modalities *)
(** A modality is accessible just when its underlying reflective subuniverse is accessible. However, for modalities we have a simpler characterization in terms of families of generating connected objects rather than families of generating inverted maps. We call an object [S]-null if it is local with respect to the maps [S i -> Unit]. *)
Record NullGenerators :=
{ ngen_indices : Type@{a} ;
ngen_type : ngen_indices -> Type@{a}
}.
Coercion ngen_type : NullGenerators >-> Funclass.
Definition null_to_local_generators : NullGenerators@{a1} -> LocalGenerators@{a2}
:= fun S => Build_LocalGenerators (ngen_indices S) (ngen_type S) (fun _ => Unit) (fun _ _ => tt).
(** As with [IsLocal], the real version of this notation will be defined in [Nullification]. *)
Module Import IsNull_Internal.
Definition IsNull (S : NullGenerators@{a}) (X : Type@{i})
:= IsLocal@{i i a} (null_to_local_generators@{a a} S) X.
(** A central fact: if a type [X] is null for all the fibers of a map [f], then it is [f]-local. (NB: the converse is *not* generally true.) TODO: Should this go in [Extensions]? *)
Definition extendable_isnull_fibers (n : nat)
{A B} (f : A -> B) (C : B -> Type)
: (forall b, ooExtendableAlong (const_tt (hfiber f b))
(fun _ => C b))
-> ExtendableAlong n f C.
simple_induction n n IHn; intros C null; [exact tt | split].
exists (fun b => (fst (null b 1%nat) (fun x => x.2 # g x.1)).1 tt).
rewrite (path_unit tt (const_tt _ a)).
exact ((fst (null (f a) 1%nat) _).2 (a ; 1)).
apply ooextendable_homotopy, null.
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
:= fun null n => extendable_isnull_fibers n f C null.
(** We define a modality to be accessible if it consists of the null types for some family of generators as above. *)
Class IsAccModality@{a i} (O : Subuniverse@{i}) :=
{
acc_ngen : NullGenerators@{a} ;
inO_iff_isnull : forall (X : Type@{i}),
iff@{i i i} (In O X) (IsNull acc_ngen X) ;
}.
Arguments acc_ngen O {_}.
Arguments inO_iff_isnull O {_} X.
Section AccessibleModalities.
Context (O : Modality) {acco : IsAccModality O}.
(** Unsurprisingly, the generators are connected. *)
Global Instance isconnected_acc_ngen i : IsConnected O (acc_ngen O i).
apply isconnected_from_elim_to_O.
pose (H := fst (fst (inO_iff_isnull O (O (acc_ngen O i))) _ i 1%nat)
(to O ((acc_ngen O) i))).
exact (fun x => (H.2 x)^).
(** If all the generators are inhabited, some things become a bit simpler. *)
Section InhabitedGenerators.
Context (inhab : forall i, acc_ngen O i).
(** For testing modal-ness of types, it suffices for all maps out of a generator to be constant. Probably one could do without [Funext]. *)
Definition inO_const_fromgen `{Funext} A
(c : forall i (f : acc_ngen O i -> A), NullHomotopy f)
: In O A.
apply (snd (inO_iff_isnull O A)); intros i.
apply ((equiv_ooextendable_isequiv _ _)^-1%equiv).
snrapply isequiv_adjointify.
intros f []; exact (c i f).1.
intros f; apply path_arrow; intros x.
symmetry; exact ((c i f).2 x).
intros g; apply path_arrow; intros [].
pose ((c i (g oD (null_to_local_generators (acc_ngen O)) i)).2).
simpl in p; unfold composeD in p.
symmetry; apply p, inhab.
(** In particular, all hprops are modal. *)
Definition inO_hprop_inhab_gen `{Funext} (A : Type) `{IsHProp A}
: In O A.
apply inO_const_fromgen; intros i f.
intros; apply path_ishprop.
End AccessibleModalities.
(** We will now show that a modality is accessible in this sense if and only if its underlying reflective subuniverse is accessible in the sense previously defined. We (almost?) never need to actually use this, though; in practice accessible modalities usually seem to be given to us with the appropriate sort of generators. *)
(** One direction of this implication is trivial. *)
Global Instance acc_rsu_modality (O : Modality) `{IsAccModality O}
: IsAccRSU O
:= Build_IsAccRSU O (null_to_local_generators (acc_ngen O)) (fun X => inO_iff_isnull O X).
(** For the less trivial converse, the idea is as follows. By [ooextendable_isnull_fibers], we can detect locality with respect to a map by nullity with respect to its fibers. Therefore, our first thought might be to just consider all the fibers of all the maps that we are localizing at. However, this doesn't quite work because [ooextendable_isnull_fibers] is not an if-and-only-if, so not every modal type would necessarily be null for that type family.
We do know, however, that if [f] is an [O]-connected map, then any [O]-modal type is null for its fibers (since they are [O]-connected types). There is no *a priori* why all the maps we localize at should end up being connected for the modality; they will always be inverted, but not every inverted map is connected (unless the modality is lex). But if [f : A -> B] is [O]-inverted, then the [O]-connected map [to O A] is (up to equivalence) the composite of [f] with the [O]-connected map [to O B]. Thus, if [X] is null for the fibers of [to O A] and [to O B], it will be [f]-local and hence [O]-modal, while all [O]-modal types will be null for these fibers since they are connected. *)
(** We don't make this an [Instance] since it is rarely used, and would cause loops when combined with the previous one. *)
Definition acc_modality_rsu (O : Modality) `{IsAccRSU O}
: IsAccModality O.
refine (Build_NullGenerators
( { i : lgen_indices@{a} (acc_lgen O)
& O (lgen_domain@{a} (acc_lgen O) i) }
+ { i : lgen_indices@{a} (acc_lgen O)
& O (lgen_codomain@{a} (acc_lgen O) i) })
_).
intros [ [i x] | [i x] ]; exact (hfiber (to O _) x).
assert (cm := @conn_map_to_O O).
intros X_inO [ [i x] | [i x] ];
exact (ooextendable_const_isconnected_inO O _ _).
apply (snd (inO_iff_islocal O X)); intros i.
refine (cancelL_ooextendable (fun _ => X) (acc_lgen O i)
(to O (lgen_codomain (acc_lgen O) i)) _ _).
apply ooextendable_isnull_fibers; intros x.
exact (Xnull (inr (i;x))).
refine (ooextendable_homotopic _
(O_functor O (acc_lgen O i)
o to O (lgen_domain (acc_lgen O) i)) _ _).
apply ooextendable_compose.
apply ooextendable_equiv, O_inverts_generators.
apply ooextendable_isnull_fibers; intros x.
exact (Xnull (inl (i;x))).
(** The construction of the nullification modality for any family of types will be in [Nullification]. *)