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

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)