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}$

type-theory calculus-of-constructions

— użytkownik
źródło

W mojej książce MLTT jest (starą i ugruntowaną) intuicyjną teorią typów zależnych, podczas gdy rachunek rachunku konstrukcji kojarzę z asystentem dowodu Coq. Ale mogę się mylić.

— Thomas Klimpel

MLTT wykorzystuje typy tożsamości do radzenia sobie z równością. Czym byłaby równość w predykcyjnym fragmencie CiC?

— Martin Berger,

@MartinBerger: CiC ma również typy tożsamości!

— cody

To trochę jak pytanie, czy Wielka Brytania jest UE bez pozostałych 27 państw członkowskich :-)

— Andrej Bauer

@AndrejBauer Gdybym był wystarczająco dowcipny, wymyśliłbym żart brexit, ale niestety nie jestem. :-P

— użytkownik

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:

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 .
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.
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.
Axiom K : jest dostępny za darmo z niektórymi wersjami zależnego dopasowania wzorca.
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{Γ ⊢ t : {I d}_{T y p e} A B}{Γ ⊢ A = B}$ $\frac{\Gamma\vdash t:\mathrm{Id}_{\mathrm{Type}}\ A\ B }{\Gamma\vdash A\ =\ B}$
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.

— cody
źródło