Martin-Löf type theory

Framework

A Dependent type theory with Identity type. Or rather it's an umbrella term for several closely related such theories.

Reference

Wikipedia: Intuitionistic type theory

Requirements

Identity type

Link to graph
Log In
Improvements of the human condition
limeGraphxioms