Homotopy Type Theory univalent type theory > history (Rev #2, changes)

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

Definition

A univalent type theory is a homotopy type theory with universes such that all universes are univalent universes.

Examples

• univalent Martin-Loef type theory
  • book homotopy type theory
• cubical type theory?
• higher observational type theory

See also

• dependent type theory
• homotopy type theory

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)