Egbert Rijke: Localizations in Homotopy Type Theory (Part 3)

Given a map f : A -> B, a type X is said to be f-local is every map A -> X extends uniquely along f to a map B -> X. The subuniverse of f-local types form a reflective subuniverse, which means that the forgetful functor from f-local types to ordinary types has a left adjoint. For example, if we take f to be the map S^{n+1} -> 1, then a type is f-local if and only if it is n-truncated (which implies that its homotopy groups vanish above degree n), and the left adjoint to the inclusion is the n-truncation.

Localization at a map f can be constructed in homotopy type theory using higher inductive types. Using the idea of finitely presentable types, we also show that localization at a map between finitely presentable types can be constructed more directly as a sequential colimit. This gives plenty of examples, including the truncations and localizations at maps between spheres such as the degree p maps on the circle, for a prime p.

Reflective subuniverses already have many nice properties. The localization preserves finite products, and any reflective subuniverse is closed under pullbacks and dependent products. However, they need not be closed under dependent sums. In fact being closed under dependent sums is one of several equivalent conditions for the reflective subuniverse to be a modality. Another equivalent condition is that the localizations X -> LX are L-connected maps.

A type is L-connected if its localization is contractible, and a map is L-connected if its fibers are L-connected. The L-connected maps are precisely the maps that are left orthogonal to the class of L-local maps, which are the maps that have local fibers. However, the classes of L-connected maps and L-local maps need not form an orthogonal factorization system. They do if and only if L is a modality! In the case of a modality this factorization system is called the stable orthogonal factorization system of a modality and its left class enjoys the property of being stable under base change.

There are two other classes of maps of interest, that can be associated to any reflective subuniverse. The class of L-equivalences (maps f such that Lf is an equivalence), and the L-etale maps (maps g that are a base change of their own localization Lg). Again, the L-equivalences and L-etale maps need not form an orthogonal factorization system, but they do if L is a modality. In this case the orthogonal factorization system is called the reflective factorization system of L, and this time the left class enjoys the 3-for-2 property. This factorization system satisfies another very nice property: the L-etale maps descend along the L-equivalences, in the sense that if f : A -> B is an L-equivalence, then the slice category of L-etale maps into A is equivalent to the slice category of L-etale maps into B.

The difference between the stable factorization system and the reflective factorization system is most easily appreciated when L is n-truncation, by comparing the left classes (i.e. the n-connected maps and the n-equivalences). In this case the n-connected maps are precisely those maps that induce isomorphisms on the homotopy groups up to n, and a surjective group homomorphism on the (n+1)-st homotopy groups. The n-equivalences on the other hand only induce isomorphisms on homotopy groups up to n, and no further condition.

 

Coming back to the example of localizing at a prime p, we will use the reflective subuniverse of L-separated types (types with L-local identity types) to show that for simply connected types, the homotopy groups of the deg(p)-localization of a type are the deg(p) localizations of the original homotopy groups of that type.