Homotopy Type Theory
realizability (Rev #1, changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

Idea

One possible way to find a computational interpretation for univalence is to interpret it in using realizability. Stekelburg provides a univalent universe of modest Kan complexes.

References

Wouter Stekelenburg, Realizability of Univalence: Modest Kan complexes, arXiv

Revision on March 14, 2015 at 16:59:43 by Bas Spitters. See the history of this page for a list of all contributions to it.