Skip to main content
27 votes

Proof-theoretic comparison table?

Here are a few comparisons of dependent type theories with fragments of Peano arithmetic and set theories that I know of: Predicative systems (the MLTT family) Predicative systems are comparable with ...
Loïc Pujet's user avatar
  • 1,479
22 votes

What are the differences between MLTT and CIC?

I do not think I would align typed conversion with CiC versus MLTT. From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time. While it ...
Neel Krishnaswami's user avatar
18 votes

What are the differences between MLTT and CIC?

The short answer is: $\mathbf{MLTT}$ relies on $\Pi$, $\Sigma$, $\mathbf{Id}$, $\mathbf{0}$, $\mathbf{1}$, $\mathbf{2}$, $\mathbf{W}$, and $\mathbf{CiC}$ relies on $\Pi$, $\Sigma$, $\mathbf{Id}$, ...
Namdak Tönpa's user avatar
12 votes

What are the differences between MLTT and CIC?

The technical answers are correct, but they completely overlook the philosophical differences between the two formalisms. Martin-Löf type theory closely reflects Arendt Heyting's explanations of the ...
Lawrence Paulson's user avatar
11 votes

What are the differences between MLTT and CIC?

Apart from judgmental equality, MLTT and CIC also differ in the following: The existence of an impredicative universe. CIC has Prop, and that's what makes it a part of the lambda cube. This universe ...
ice1000's user avatar
  • 6,256
6 votes

In a dependently typed language, are all types statements?

To make the basics clear: languages don't mean anything before you assign them meanings manually, and you can interpret the same language different ways. So if you want to interpret a dependent type ...
Trebor's user avatar
  • 4,015
4 votes

In a dependently typed language, are all types statements?

You can look at the ways to define types as ways to define propositions. One simple definition of Nat is its Boehm-Berarducci encoding: ...
Li-yao Xia's user avatar
  • 1,792
3 votes

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?

The universal property of final coalgebras can be formalized as unique-ana : ∀ (f : A → B × A) (g : A → Stream B) → unfold ∘ g ≡ map₂ g ∘ f → g ≡ ana f where <...
Li-yao Xia's user avatar
  • 1,792

Only top scored, non community-wiki answers of a minimum length are eligible