Homotopy Type Theory localization > history (Rev #7, changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

Idea

Localization is the process of inverting a specified class of maps.

Definition

Consider a family $F:{\prod }_{(a:A)}B(a)\to C(a)$ \prod_{(a:A)} F:\prod_{(a:A)} B(a) \to C(a) of maps. We say that a type $X$ is $F$-local if the function

is an equivalence . for all (a : A).

Properties

References

• Modalities in homotopy type theory
• Localization in Homotopy Type Theory
• HoTT book