What are the differences between MLTT and CIC?

Question

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 assistant) and the "CIC" world (with Coq). For instance, there are two presentations in annex A of the HoTT book, the first one presenting conversion as the equivalence relation generated by computation rules (this is I believe the traditional "CIC" presentation), while the second uses a typed conversion judgment (I would relate this to the "MLTT" culture).

What would you list as the features most representatives of each side, be it in the theoretical presentation or in the implementations? Or do you think this view of two different cultures is not accurate, and if so why?

Answer 1

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 wouldn't be trivial, producing a version of CiC with typed conversion seems like a fairly routine effort.

IMO, the serious difference in design lies in the treatment of Prop. Coq (and Lean) have an impredicative sort of propositions, and this really fundamentally changes the logical strength of the theory.

You can formalise the normalisation of System F in Coq/Lean, and you just can't in predicative systems like Agda. Conversely, the metatheory of predicative systems like Agda is much simpler to establish than that of CiC-style systems.

One thing which does seem like a cultural difference to me is that Agda/Idris favour top-level clausal definitions, whereas Coq has a more traditional expression-oriented design. (E.g., Agda doesn't even have a case expression AFAIK.)

There might be a slight technical basis to this choice (polarised presentations of type theory tend to lead one towards clausal definitions), but it mostly seems to be based on whether the proof assistant was implemented in Haskell (lots of clausal definitions) or ML (lots of expressions).

Answer 2

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}$, General Inductive Schemes. They are slightly different systems, e.g. $\mathbf{0}$, $\mathbf{1}$, $\mathbf{2}$, $\mathbf{W}$ basis lacks of mutual recursivity which can be added separately. There are also a list of flavours of MLTT: MLTT-72 with $\Pi$, $\Sigma$ only, MLTT-73 with Id-types and predicative hierarchy of universes $\mathcal{U}_n$ and more recent developments up to HoTT which is also MLTT-80 based. The other option is $\mathcal{Prop}$ universe such that $\mathcal{Prop} \prec \mathcal{U}_n$. It is aded to CiC, but also could be added to MLTT. The pure formulas are following:

• MLTT-72¹ = $\Pi$, $\Sigma$, $\mathcal{U}$
  

• MLTT-73² = $\Pi$, $\Sigma$, +, $\mathbb{N}$, $\mathbb{N}_n$, $\mathbf{Id}$, $\mathcal{U}_n$
  

• MLTT-80³ = $\Pi$, $\Sigma$, $\mathbf{0}$, $\mathbf{1}$, $\mathbf{2}$, $\mathbf{W}$, $\mathbf{Id}$, $\mathcal{U}_n$, derivable: +, $\mathbb{N}$, List
  

• CiC⁴ = $\Pi$, $\Sigma$, $\mathbf{Id}$, $\mathbf{Ind}$, $\mathcal{U}_n$, $\mathcal{Prop}$

Among these systems CiC is most powerful as implements general inductive schemes with mutual recursivity, termination checking, and strict positivity checking.

---

[1]. Martin-Löf. An Intuitionistic Theory of Types. 1972
[2]. Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. 1975
[3]. Martin-Löf. Intuitionistic Type Theory. 1980
[4]. Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. 2015

Answer 3

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 logical signs and is intuitionistic by construction. CIC is a formal calculus based on string substitution with no underlying philosophy that I can detect.

I have personally heard Martin-Löf criticise CIC, in particular because it is impredicative. The habit of using CIC to do constructive mathematics has never made sense to me.

Answer 4

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 can be useful in stating some theorems. MLTT is fully predicative.
• Due to typed conversion, MLTT supports more eta laws.
• The "preferred" underlying models are different. In my impression, CIC people prefer a domain theoretic model, while MLTT is based on Martin-Löf's so-called "substitution calculus" which has a very nice categorical model (with many different but similar presentations, like CwF, CwA, etc.).

For the last point, I would say it's more like a cultural diversity instead of a theoretical difference (but it's still worth mentioning).