Return to Answer

The short answer is yes, MLTT can reasonably be equated with CIC without impredicative prop.

The main technical issue is that there are dozens of variants when one talks about Martin-Löf Type Theory and, perhaps more surprisingly, when one talks about CIC. For example, taking the version of CIC defined in Benjamin Werner's thesis, it doesn't even make sense to remove Prop, as one doesn't have either Set or universes of Type.

The main variations one can consider in either of these theories are:

1. Universes: how many, and how are they defined (Palmgren, On Universes in Type Theory, discusses many inequivalent variations), and wether or not universe polymorphism is admitted.

2. Which inductive types/families: Agda admits Inductive-Recursive types, but there are many more mundane variations depending on how "large" the types in the constructors and eliminators are allowed, handling parameters vs indices, etc.

3. Injectivity of type constructors. This leads to a system inconsistent with EM in Agda. Of course Epigram has a more extreme "Observational Type Theory", but this can be considered something different altogether.

4. Axiom K: this comes for free with certain versions dependent pattern matching.

5. Intentional vs Extensional: this is a huge difference, where essentially a new conversion rule is added in the extensional systems $$ \frac{\Gamma\vdash t:\mathrm{Id}_{\mathrm{Type}}\ A\ B }{\Gamma\vdash A\ =\ B} $$ Which makes type-checking undecidable (but much more powerful!). Martin-Löf himself seems to have considered both types of systems.

6. The presence of coinductive types and associated elimination principles.

All of the above variations (except OTT) have been considered in the litterature and associated with the name "Martin-Löf Type Theory" or "Calculus of Inductive Constructions", mostly because of their association with the Agda and Coq systems, respectively.

So the long answer is that there is no consensus about what the exact definition of either of these systems is.

The short answer is yes, MLTT can reasonably be equated with CIC without impredicative Prop.

The main technical issue is that there are dozens of variants when one talks about Martin-Löf Type Theory and, perhaps more surprisingly, when one talks about CIC. For example, taking the version of CIC defined in Benjamin Werner's thesis, it doesn't even make sense to remove Prop, as one doesn't have either Set or universes of Type.

The main variations one can consider in either of these theories are:

1. Universes: how many, and how are they defined (Palmgren, On Universes in Type Theory, discusses many inequivalent variations), and whether or not universe polymorphism is admitted.

2. Which inductive types/families: Agda admits Inductive-Recursive types, but there are many more mundane variations depending on how "large" the types in the constructors and eliminators are allowed, handling parameters vs indices, etc.

3. Injectivity of type constructors. This leads to a system inconsistent with EM in Agda. Of course Epigram has a more extreme "Observational Type Theory", but this can be considered something different altogether.

4. Axiom K: this comes for free with certain versions of dependent pattern matching.

5. Intentional vs Extensional: this is a huge difference, where essentially a new conversion rule is added in the extensional systems $$ \frac{\Gamma\vdash t:\mathrm{Id}_{\mathrm{Type}}\ A\ B }{\Gamma\vdash A\ =\ B} $$ Which makes type-checking undecidable (but much more powerful!). Martin-Löf himself seems to have considered both types of systems.

6. The presence of coinductive types and associated elimination principles.

All of the above variations (except OTT) have been considered in the literature and associated with the name "Martin-Löf Type Theory" or "Calculus of Inductive Constructions", mostly because of their association with the Agda and Coq systems, respectively.

So the long answer is that there is no consensus about what the exact definition of either of these systems is.

The short answer is yes, MLTT can reasonably be equated with CIC without impredicative prop.

The main technical issue is that there are dozens of variants when one talks about Martin-Löf Type Theory and, perhaps more surprisingly, when one talks about CIC. For example, taking the version of CIC defined in Benjamin Werner's thesis, it doesn't even make sense to remove Prop, as one doesn't have either Set or universes of Type.

The main variations one can consider in either of these theories are:

1. Universes: how many, and how are they defined (Palmgren, On Universes in Type Theory, discusses many inequivalent variations), and wether or not universe polymorphism is admitted.

2. Which inductive types/families: Agda admits Inductive-Recursive types, but there are many more mundane variations depending on how "large" the types in the constructors and eliminators are allowed, handling parameters vs indices, etc.

3. Injectivity of type constructors. This leads to a system inconsistent with EM in Agda. Of course Epigram has a more extreme "Observational Type Theory", but this can be considered something different altogether.

4. Axiom K: this comes for free with certain versions dependent pattern matching.

5. Intensional vs Extensional: this is a huge difference, where essentially a new conversion rule is added in the extensional systems $$ \frac{\Gamma\vdash t:\mathrm{Id}_{\mathrm{Type}}\ A\ B }{\Gamma\vdash A\ =\ B} $$ Which makes type-checking undecidable (but much more powerful!). Martin-Löf himself seems to have considered both types of systems.

6. The presence of coinductive types and associated elimination principles.

All of the above variations (except OTT) have been considered in the litterature and associated with the name "Martin-Löf Type Theory" or "Calculus of Inductive Constructions", mostly because of their association with the Agda and Coq systems, respectively.

So the long answer is that there is no consensus about what the exact definition of either of these systems is.

The short answer is yes, MLTT can reasonably be equated with CIC without impredicative prop.

The main technical issue is that there are dozens of variants when one talks about Martin-Löf Type Theory and, perhaps more surprisingly, when one talks about CIC. For example, taking the version of CIC defined in Benjamin Werner's thesis, it doesn't even make sense to remove Prop, as one doesn't have either Set or universes of Type.

The main variations one can consider in either of these theories are:

1. Universes: how many, and how are they defined (Palmgren, On Universes in Type Theory, discusses many inequivalent variations), and wether or not universe polymorphism is admitted.

2. Which inductive types/families: Agda admits Inductive-Recursive types, but there are many more mundane variations depending on how "large" the types in the constructors and eliminators are allowed, handling parameters vs indices, etc.

3. Injectivity of type constructors. This leads to a system inconsistent with EM in Agda. Of course Epigram has a more extreme "Observational Type Theory", but this can be considered something different altogether.

4. Axiom K: this comes for free with certain versions dependent pattern matching.

5. Intentional vs Extensional: this is a huge difference, where essentially a new conversion rule is added in the extensional systems $$ \frac{\Gamma\vdash t:\mathrm{Id}_{\mathrm{Type}}\ A\ B }{\Gamma\vdash A\ =\ B} $$ Which makes type-checking undecidable (but much more powerful!). Martin-Löf himself seems to have considered both types of systems.

6. The presence of coinductive types and associated elimination principles.

All of the above variations (except OTT) have been considered in the litterature and associated with the name "Martin-Löf Type Theory" or "Calculus of Inductive Constructions", mostly because of their association with the Agda and Coq systems, respectively.

So the long answer is that there is no consensus about what the exact definition of either of these systems is.

The short answer is yes, MLTT can reasonably be equated with CIC without impredicative prop.

The main technical issue is that there are dozens of variants when one talks about Martin-Löf type and when one talks about CIC. For example, taking the version of CIC defined in Benjamin Werner's thesis, it doesn't even make sense to remove Prop, as one doesn't have either Set or universes of Type.

The main variations one can consider in either of these theories are:

1. Universes: how many, and how are they defined (Palmgren, On Universes in Type Theory, discusses many inequivalent variations), and wether or not universe polymorphism is admitted.

2. Which inductive types/families: Agda admits Inductive-Recursive types, but there are many more mundane variations depending on how "large" the types in the constructors and eliminators are allowed, handling parameters vs indices, etc.

3. Injectivity of type constructors. This leads to a system inconsistent with EM in Agda. Of course Epigram has a more extreme "Observational Type Theory", but this can be considered something different altogether.

4. Axiom K: this comes for free with certain versions dependent pattern matching.

5. Intensional vs Extensional: this is a huge difference, where essentially a new conversion rule is added in the extensional systems $$ \frac{\Gamma\vdash t:\mathrm{Id}_{\mathrm{Type}}\ A\ B }{\Gamma\vdash A\ =\ B} $$ Which makes type-checking undecidable (but much more powerful!). Martin-Löf himself seems to have considered both types of systems.

6. The presence of coinductive types and associated elimination principles.

All of the above variations (except OTT) have been considered in the litterature and associated with the name "Martin-Löf Type Theory" or "Calculus of Inductive Constructions", mostly because of their association with the Agda and Coq systems, respectively.

So the long answer is that there is no consensus about what the exact definition of either of these systems is.

The short answer is yes, MLTT can reasonably be equated with CIC without impredicative prop.

The main technical issue is that there are dozens of variants when one talks about Martin-Löf Type Theory and, perhaps more surprisingly, when one talks about CIC. For example, taking the version of CIC defined in Benjamin Werner's thesis, it doesn't even make sense to remove Prop, as one doesn't have either Set or universes of Type.

The main variations one can consider in either of these theories are:

1. Universes: how many, and how are they defined (Palmgren, On Universes in Type Theory, discusses many inequivalent variations), and wether or not universe polymorphism is admitted.

2. Which inductive types/families: Agda admits Inductive-Recursive types, but there are many more mundane variations depending on how "large" the types in the constructors and eliminators are allowed, handling parameters vs indices, etc.

3. Injectivity of type constructors. This leads to a system inconsistent with EM in Agda. Of course Epigram has a more extreme "Observational Type Theory", but this can be considered something different altogether.

4. Axiom K: this comes for free with certain versions dependent pattern matching.

5. Intensional vs Extensional: this is a huge difference, where essentially a new conversion rule is added in the extensional systems $$ \frac{\Gamma\vdash t:\mathrm{Id}_{\mathrm{Type}}\ A\ B }{\Gamma\vdash A\ =\ B} $$ Which makes type-checking undecidable (but much more powerful!). Martin-Löf himself seems to have considered both types of systems.

6. The presence of coinductive types and associated elimination principles.

All of the above variations (except OTT) have been considered in the litterature and associated with the name "Martin-Löf Type Theory" or "Calculus of Inductive Constructions", mostly because of their association with the Agda and Coq systems, respectively.

So the long answer is that there is no consensus about what the exact definition of either of these systems is.