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
2 votes
1 answer

Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?

Suppose we work inside MLTT with equality reflection (extensional MLTT). Assume I postulate existence of Streams as final co-algebra for the suitable functor. Is that enough to prove the bisimulation ...
Russoul's user avatar
  • 345
5 votes
0 answers

Proof-theoretic strength of HOL compared to predicative dependent types

By HOL I mean something like inference rules of HOL Light with the 3 axioms of infinity, extensionality and choice ($\varepsilon$ operator). By predicative dependent types, I am thinking of MLTT + W-...
Timo's user avatar
  • 517
18 votes
1 answer

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 ...
user21820's user avatar
  • 455
24 votes
4 answers

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 ...
Meven Lennon-Bertrand's user avatar