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

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

Definition

Intensional Martin-Loef type theoryA 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?