Localization is the process of inverting a specified class of maps.
Consider a family F:∏ (a:A)B(a)→C(a)F:\prod_{(a:A)} B(a) \to C(a) of maps. We say that a type XX is FF-local if the function
is an equivalence for all (a : A).
TODO: Localisation as a HIT?