Czy MLTT skutecznie pCiC bez Prop?

Czy teoria typu Martina-Löfa jest w gruncie rzeczy predykatywnym rachunkiem konstrukcji indukcyjnych bez impredykatywnego ?$\mathtt{Prop}$

Jeśli są blisko spokrewnione, ale mają więcej różnic niż tylko , jakie to są różnice?$\mathtt{Prop}$

Krótka odpowiedź brzmi: tak, MLTT można rozsądnie utożsamić z CIC bez impredicative Prop.

Głównym problemem technicznym jest to, że istnieją dziesiątki wariantów, gdy mówi się o teorii typu Martina-Löfa i, co może być bardziej zaskakujące, gdy mówi się o CIC. Na przykład, biorąc pod uwagę wersję CIC zdefiniowaną w pracy Benjamina Wernera, nie ma nawet sensu jej usuwać Prop, ponieważ nie ma ani jednego, Setani jednego wszechświata Type.

Główne warianty, które można rozważyć w jednej z tych teorii, to:

1. Wszechświaty : ile i jak są one zdefiniowane (Palmgren, On Universes in Theory Theory , omawia wiele nierównych odmian) i czy dopuszcza się polimorfizm wszechświata .

2. Które typy / rodziny indukcyjne : Agda przyjmuje typy indukcyjno-rekurencyjne, ale istnieje wiele bardziej przyziemnych odmian w zależności od tego, jak „duże” typy w konstruktorach i eliminatorach są dozwolone, parametry obsługi w porównaniu z indeksami itp.

3. Zastrzyki konstruktorów typów . Prowadzi to do systemu niezgodnego z EM w Agdzie. Oczywiście Epigram ma bardziej ekstremalną „Teorię Typów Obserwacyjnych”, ale można to uznać za coś zupełnie innego.

4. Axiom K : jest dostępny za darmo z niektórymi wersjami zależnego dopasowania wzorca.

5. Celowe a ekstrawaganckie : to ogromna różnica, w której zasadniczo dodawana jest nowa reguła konwersji w systemach ekstensywnych Co sprawia, że ​​sprawdzanie typu jest nierozstrzygalne (ale znacznie potężniejsze!). Wydaje się, że sam Martin-Löf rozważał oba rodzaje systemów.

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

6. Obecność typów koindukcyjnych i związanych z nimi zasad eliminacji.

Wszystkie powyższe odmiany (oprócz OTT) zostały wzięte pod uwagę w literaturze i związane z nazwą „Teoria typów Martina-Löfa” lub „Rachunek konstrukcji indukcyjnych”, głównie ze względu na ich związek z systemami Agda i Coq.

Długa odpowiedź brzmi więc, że nie ma zgody co do dokładnej definicji jednego z tych systemów.