Localization as an Inductive Definition | Homotopy Type Theory

Localization as an Inductive Definition

I’ve been talking a lot about reflective subcategories (or more precisely, reflective subfibrations) in type theory lately (here and here and here), so I started to wonder about general ways to construct them inside type theory. There are some simple examples like the following.

• As Steve Awodey mentioned, the (effective epi, mono) factorization system is an example. It can be constructed inside type theory using the higher inductive type is_inhab (see here), which is a version of the Awodey-Bauer “bracket” operation on types.
• More generally, we should be able to construct the n-truncated factorization system for any n, once we write down the n-truncation as a HIT. In particular, for n=0 we get as the reflector.
• There’s one that we can construct without any HITs: any h-proposition U gives rise to an open subtopos whose reflector is fun A => U -> A (see here). The objects of the subcategory are those for which const : A -> (U -> A) is an equivalence.
• I think we should be able to construct closed subtoposes using the HIT that defines homotopy pushouts (the reflector there should take A to the pushout of the two projections ), but I haven’t checked this yet.

However, in category theory (and -category theory) there is an important, uniform way of constructing reflective subcategories and factorization systems — by localization. Given a family of maps F, we define an object X to be F–local if is an equivalence for all in F. When F is small in a well-behaved category (such as a Grothendieck topos), the F-local objects are a reflective subcategory, and moreover every (accessible) reflective subcategory arises in this way.

Can we mimic this in type theory? Given a family of maps

Hypothesis I : Type.
Hypothesis S T : I -> Type.
Hypothesis f : forall i, S i -> T i.

it’s easy to define locality:

Definition is_local Z := forall i,
  is_equiv (fun g : T i -> Z => g o f i).

but how can we prove the local objects are reflective? In both classical homotopy theory and -category theory, the reflector is obtained with a transfinite cell-complex construction (sometimes disguised by other machinery, such as accessibility). But this is exactly the sort of thing that higher inductive types do even better! Consider the following HIT (I’ve switched to using the notation == for identity/path types, following a discussion on the HoTT mailing list):

Inductive localize X :=
| to_local : X -> localize X
| local_extend : forall (i:I) (h : S i -> localize X),
    T i -> localize X
| local_extension : forall (i:I) (h : S i -> localize X) (s : S i),
    local_extend i h (f i s) == h s
| local_unextension : forall (i:I) (g : T i -> localize X) (t : T i),
    local_extend i (g o f i) t == g t
| local_triangle : forall (i:I) (g : T i -> localize X) (s : S i),
    local_unextension i g (f i s) == local_extension i (g o f i) s.

The first constructor to_local says that localize X comes with a map from X. And the other four say exactly that localize X is F-local! Specifically, the second constructor local_extend says that any map S i -> localize X can be extended along f i to T i. The third says that this extension is an extension (that is, the extension operation is right inverse to restriction), while the fourth says that it is left inverse, and the fifth supplies one triangle identity for these homotopies. Thus, together they form an element of the space of “adjoint equivalence data” for fun g : T i -> localize X => g o f i, which is an h-proposition that’s equivalent to Voevodsky’s definition of is_equiv.

Axiomatizing localize in Coq as usual for HITs, I’ve been able to prove that it does, in fact, make the local objects into a reflective subfibration, in the sense discussed here. The code (still rather ugly, alas) can be found here. The reason we can get a reflective subfibration rather than merely a reflective subcategory is that we are automatically performing an internal localization: the local objects see the maps f i as equivalences not only on external hom-spaces (which we don’t have access to internally anyway) but on the internal-homs. (More precisely, they see all pullbacks of F along maps into I as equivalences, which means that if I is interesting, it influences the localization as well — see below.) As discussed here, being this sort of internal localization is exactly what we need to make a reflective subcategory into a reflective subfibration — and conveniently, the latter is also exactly what we can describe internally.

In other words, higher inductive types allow us to construct localizations by just saying “the localization of X is the universal object equipped with a map from X and which is local,” which is exactly what we want. I find this very intuitively attractive and quite pleasing. It also makes very precise the vague idea mentioned here that is “inductively generated” by X together with “sharpness” — here “sharpness” means “F-locality”, and the inductive type says exactly that.

Moreover, lots of useful things are special cases of localization:

• The (-1)-truncation is_inhab is equivalently localization at .
• Similarly, the n-truncation is localization at .
• The reflector of an open subtopos is equivalently localization at .
• Modulo size questions, every reflective subcategory is a localization (at the large class of maps inverted by the reflector).
• Unlike Set, which (classically) has no interesting reflective subcategories, has many interesting reflective subcategories even classically, many of which are naturally constructed as localizations. Moreover, since in the internal and external-homs are identical, all these localizations are internal. For instance, in classical homotopy theory, it is important to be able to localize a space by “inverting a prime number”. One way to do this is to localize at the degree-p map . Another way (probably distinct in general, but agreeing for a large class of spaces) is to localize at the class of -homology isomorphisms (which is not small, but you can find a small generating set for it). We might be able to do this in type theory if we knew how to define homology.
• Any -topos is a (left exact) localization of an -category of presheaves. Thus, combining this with my previous post, we should be able to reduce the question of modeling univalence in -toposes to the case of presheaf -toposes. Moreover, if the HIT localize satisfies the computation rule for the constructor to_local definitionally (this is a 0-level constructor, which are the ones that it’s most sensible to expect to have definitional computation), then the corresponding should also have definitional computation, so that we can model (higher) inductive types in the subcategory strictly as well.

It’s natural to ask what properties of the family F being localized at will make the reflective subfibration into a stable factorization system or a lex-reflective subcategory. The main result in that direction I have is that we get a stable factorization system if the family of targets T is constant at the terminal object. In this case, what we are essentially doing is localizing at the class of all pullbacks of the projection . And as discussed here, localization at a pullback-stable class always gives a stable factorization system. I don’t know any general conditions on F to ensure that we get a lex-reflective subcategory, though.