Homotopy Type Theory Martin-Loef type theory > history (Rev #2)

Definition

A Martin-Loef type theory is a homotopy type theory with all W-types?.

See also

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

References

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