O MLTT é efetivamente pCiC sem Prop?

A teoria dos tipos de Martin-Löf é basicamente o cálculo predicativo de construções indutivas sem impredicative ?$\mathtt{Prop}$

Se eles estão intimamente relacionados, mas com mais diferenças do que apenas , quais são essas diferenças?$\mathtt{Prop}$

A resposta curta é sim, o MLTT pode ser razoavelmente igualado ao CIC sem impredicativo Prop.

A principal questão técnica é que existem dezenas de variantes quando se fala da teoria dos tipos de Martin-Löf e, talvez mais surpreendente, quando se fala da CIC. Por exemplo, considerando a versão do CIC definida na tese de Benjamin Werner, nem faz sentido remover Prop, pois não se tem um Setou universos de Type.

As principais variações que podemos considerar em uma dessas teorias são:

1. Universos : quantos, e como eles são definidos (Palmgren, On Universes in Type Theory , discute muitas variações desigual), e se o polimorfismo do universo é ou não admitido.

2. Quais tipos / famílias indutivos : A Agda admite tipos indutivos-recursivos, mas há muitas outras variações mundanas, dependendo de quão "grandes" os tipos nos construtores e eliminadores são permitidos, lidando com parâmetros versus índices, etc.

3. Injetividade dos construtores de tipos . Isso leva a um sistema inconsistente com o EM na Agda. É claro que o Epigram tem uma "Teoria do tipo observacional" mais extrema, mas isso pode ser considerado algo completamente diferente.

4. Axioma K : é fornecido gratuitamente com certas versões da correspondência de padrões dependentes.

5. Intencional vs Extensional : essa é uma enorme diferença, onde essencialmente uma nova regra de conversão é adicionada nos sistemas que torna a verificação de tipo indecidível (mas muito mais poderosa!). O próprio Martin-Löf parece ter considerado os dois tipos de sistemas.

   $$\frac{\Gamma\vdash t:\mathrm{Id}_{\mathrm{Type}}\ A\ B }{\Gamma\vdash A\ =\ B}$$

6. A presença de tipos coindutores e princípios de eliminação associados.

Todas as variações acima (exceto OTT) foram consideradas na literatura e associadas ao nome "Teoria dos tipos Martin-Löf" ou "Cálculo de construções indutivas", principalmente devido à associação com os sistemas Agda e Coq, respectivamente.

Portanto, a resposta longa é que não há consenso sobre qual é a definição exata de qualquer um desses sistemas.