Homotopy Type Theory
localization (Rev #6, changes)

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

Idea

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

Definition

Consider a family (a:A)B(a)C(a)\prod_{(a:A)} B(a) \to C(a) of maps. We say that a type XX is FF-local if the function

λg.gF(a):(C(a)X)(B(a)X)\lambda g . g \circ F(a) : (C(a) \to X) \to (B(a) \to X)

is an equivalence.

Properties

References

category: homotopy theory

Revision on October 10, 2018 at 19:21:02 by Ali Caglayan. See the history of this page for a list of all contributions to it.