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
4 votes
2 answers
643 views

In a dependently typed language, are all types statements?

In dependently typed languages such as Agda, Lean, Coq, Idris (and Pie), a mathematical or logical statement can be expressed as a type, and then proven by writing a program that creates an instance ...
Mars's user avatar
  • 141
2 votes
1 answer
102 views

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
223 views

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-...
Ilk's user avatar
  • 547
21 votes
1 answer
1k 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 ...
user21820's user avatar
  • 484
25 votes
4 answers
1k 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 ...
Meven Lennon-Bertrand's user avatar