Questions tagged [martin-lof-type-theory]

Per Martin-Löf‘s dependent type theory, also known as intuitionistic or constructive type theory, is a foundation for constructive mathematics notably using П-types, Σ-types, and W-types.

Filter by
Sorted by
Tagged with
18 votes
1 answer
817 views

Proof-theoretic comparison table?

I read this CSTheory SE post, which suggests that it is often not clear what variant of MLTT or CIC is being referred to. But I would like to know the proof-theoretic strengths of the various ...
user avatar
  • 421
24 votes
4 answers
531 views

What are the differences between MLTT and CIC?

In the theory and design of proof assistants based upon dependent types, I feel like there’s a somewhat cultural divide between the "MLTT" world (with Agda as the main representative proof ...
user avatar