Localization

Suppose given a family of maps f : ∀ (i:I), S i → T i. A type X is said to be f-local if for all i:I, the map (T i → X) → (S i → X) given by precomposition with f i is an equivalence. Our goal is to show that the f-local types form a reflective subuniverse, with a reflector constructed by localization. That is, morally we want to say

Inductive Localize f (X : Type) : Type :=
| loc : X -> Localize X
| islocal_localize : forall i, IsEquiv (fun (g : T i -> X) => g o f i).

This is not a valid HIT by the usual rules, but if we expand out the definition of IsEquiv and apply path_sigma and path_forall, then it becomes one. We get a simpler definition (no 2-path constructors) if we do this with BiInv rather than IsEquiv:

Inductive Localize f (X : Type) : Type :=
| loc : X -> Localize X
| lsect : forall i (g : S i -> X), T i -> X
| lissect : forall i (g : S i -> X) (s : S i), lsect i g (f i s) = g s
| lretr : forall i (g : S i -> X), T i -> X
| lisretr : forall i (h : T i -> X) (t : T i), lretr i (h o f i) t = h t.

This definition works, and from it one can prove that the f-local types form a reflective subuniverse. However, the proof inextricably involves Funext. We can avoid Funext in the same way that we did in the definition of a ReflectiveSubuniverse, by using pointwise path-split precomposition equivalences. Observe that the assertion ExtendableAlong n f C consists entirely of points, paths, and higher paths in C. Therefore, for any n we might choose, we can define Localize f X as a HIT to universally force ExtendableAlong n (f i) (fun _ ⇒ Localize f X) to hold for all i. For instance, when n is 2 (the smallest value which will ensure that Localize f X is actually f-local), we get

Inductive Localize f (X : Type) : Type :=
| loc : X -> Localize X
| lrec : forall i (g : S i -> X), T i -> X
| lrec_beta : forall i (g : S i -> X) (s : T i), lrec i g (f i s) = g s
| lindpaths : forall i (h k : T i -> X) (p : h o f i == k o f i) (t : T i), h t = k t
| lindpaths_beta : forall i (h k : T i -> X) (p : h o f i == k o f i) (s : S i),
                     lindpaths i h k p (f i s) = p s.

However, just as for ReflectiveSubuniverse, in order to completely avoid Funext we need the oo-version of path-splitness. Written out as above, this would involve infinitely many constructors (but it would not otherwise be problematic, so for instance it can be constructed semantically in model categories). We can't actually write out infinitely many constructors in Coq, of course, but since we have a finite definition of ooExtendableAlong, we can just assert directly that ooExtendableAlong (f i) (fun _ ⇒ Localize f X) holds for all i. Then, however, we have to express the hypotheses of the induction principle. We know what these should be for each path-constructor and higher path-constructor, so all we need is a way to package up those infinitely many hypotheses into a single one, analogously to ooExtendableAlong. Thus, we begin this file by defining a "dependent" version of ooExtendableAlong, and of course we start this with a version for finite n.

Dependent extendability

Control universe parameters

Like ExtendableAlong, these can be postcomposed with known equivalences.

And if the dependency is trivial, we obtain them from an ordinary ExtendableAlong.

This lemma will be used in stating the computation rule for localization.

Here's the oo-version.

The oo-version for trivial dependency.

A crucial fact: the oo-version is inherited by types of homotopies.

Local types

We have to fiddle with the max universes to get this to work, since ooextendable_postcompose requires the max universe in both cases to be the same, whereas we don't want to assume that the hypothesis and conclusion are related in any way.

Localization as a HIT

Note that the following axiom actually contains a point-constructor. We could separate out that point-constructor and make it an actual argument of the private inductive type, thereby getting a judgmental computation rule for it. However, since locality is an hprop, there seems little point to this.

We now state the computation rule for islocal_localize. Since locality is an hprop, we never actually have any use for it, but the fact that we can state it is a reassuring check that we have defined a meaningful HIT.

Now we prove that localization is a reflective subuniverse.

The induction principle is an equivalence.

Typeclass inference can find this, but we give it explicitly to prevent extra universes from cropping up.

Here is the "real" definition of the notation IsLocal. Defining it this way allows it to inherit typeclass inference from In, unlike (for instance) the slightly annoying case of IsTrunc n versus In (Tr n).

A remark on universes: recall that ooExtendableAlong takes four universe parameters, three for the sizes of the types involved and one for the max of all of them. In the definition of IsLocal f X we set that max universe to be the same as the size of X, so that In (Loc f) X would lie in the same universes as X, which is necessary for our definition of a reflective subuniverse. However, in practice we may need this extendability property with the max universe being larger, to avoid coalescing universes undesiredly. Thus, in making it available by the following name, we also insert a lift to generalize the max universe.

The non-dependent eliminator

Localization and accessibility

Localization subuniverses are accessible, essentially by definition. Without the universe annotations, a and i get collapsed.

Conversely, if a subuniverse is accessible, then the corresponding localization subuniverse is equivalent to it, and moreover exists at every universe level and satisfies its computation rules judgmentally. This is called lift_accrsu but in fact it works equally well to *lower* the universe level, as long as both levels are no smaller than the size a of the generators.

The lifted universe agrees with the original one, on any universe contained in both i and j

Anyone stepping through this proof should do Set Printing Universes.

Similarly, because localization is a HIT that has an elimination rule into types in *all* universes, for accessible reflective subuniverses we can show that containment implies connectedness properties with the universe containments in the other order.

Compared to O_leq@{i1 i2 i1} and A : Type@{i1} in isconnected_O_leq, these two lines are what make i2 ≤ i1 instead of vice versa.

Anyone stepping through this proof should do Set Printing Universes.

At this point you should also do Unset Printing Notations to see the universe annotation on IsTrunc change.

And similarly for connected maps.

Anyone stepping through this proof should do Set Printing Universes.

The same is true for inverted maps, too.

It looks like we can say exact e, but that would collapse the universes i1 and i2. You can check with Set Printing Universes. Unset Printing Notations. that e and the goal have different universes. So instead we do this: