Jakie części teorii typów homotopii nie są możliwe w Agdzie lub Coq?

Kiedy patrzymy na książkę, teoria typów homotopii - widzimy następujące tematy:

Homotopy type theory 
2.1 Types are higher groupoids
2.2 Functions are functors
2.3 Type families are fibrations
2.4 Homotopies and equivalences
2.5 The higher groupoid structure of type formers
2.6 Cartesian product types
2.7 S-types
2.8 The unit type
2.9 P-types and the function extensionality axiom
2.10 Universes and the univalence axiom
2.11 Identity type
2.12 Coproducts
2.13 Natural numbers
2.14 Example: equality of structures
2.15 Universal properties

Teraz wiemy, że nie wszystkie teorie typu homotopii są możliwe: Agda i Coq .

Moje pytanie brzmi: jakie części teorii typów homotopii nie są możliwe w Agdzie lub Coq?

Jeśli spojrzeć na Notatki o rozdziale 8 widać, co jest już sformalizowane i myślę, że to dużo. Istnieją biblioteki Coq HoTT i biblioteka Agda HoTT-Agda, które formalizują duże fragmenty teorii typów homotopii.

Aby załatwić sprawę w Coq, potrzebowaliśmy specjalnej wersji Coq, która została załatana tylko na potrzeby HoTT. Jednak Coq zmierza w kierunku wspierania teorii typu homotopii, więc wkrótce będziemy w stanie to zrobić ze standardowym Coq.

W Agdzie trzeba włączyć tę --without-Kopcję, w przeciwnym razie Agda uważa, że ​​wszystkie typy są 0-typami. Istnieją pewne wątpliwości, czy --without-Ktak naprawdę pozbyć się założenia, że ​​wszystko jest zerowe, a może ktoś mógłby przywrócić go do Agdy przy użyciu trudnych dopasowań wzorców.

Następujące aspekty formalizacji Coq i Agda nie są zadowalające:

1. Aksjomat Univalence jest podany jako hipoteza. Byłoby lepiej, gdyby był wbudowany w system. W szczególności chcielibyśmy, aby Coq i Agda zrozumieli zasady obliczeń dotyczące aksjomatu Univalence.

2. Podobnie, musimy użyć hacków, aby uzyskać wykonalne typy o wyższej indukcji. Znowu lepiej byłoby mieć bezpośrednie wsparcie.

Problem z powyższymi brakami polega na tym, że nikt nie wie, jak je naprawić, nawet teoretycznie. To jest aktywny obszar badań.

Poza tym uważam, że uczciwie można powiedzieć, że HoTT można wykonać głównie w Coq i Agda, ale nie w optymalny sposób.

O ile rozumiem, w Agdzie można to wszystko przedstawić (tj. Cały rozdział 2 - na github znajduje się biblioteka; AFAIK, to samo dotyczy Coq). Dopiero po przejściu do kolejnych rozdziałów sprawy stają się groźne. Istnieją dwa oczywiste elementy:

1. Okrąg. Jest to reprezentowane (w Agdzie) za pomocą postulatu , a więc nie jest tak miłe jak inne rzeczy.
2. $\infty$

Są też inne rzeczy, ale jeszcze nie czytałem tej części formalizacji Agdy ... Ale ogólnie rzecz biorąc, większość HoTT można ładnie sformalizować zarówno w Agdzie, jak i Coq.

Co ważniejsze, oba zespoły programistów aktywnie pracują nad dostosowaniem swoich systemów, tak aby można było obsłużyć więcej HoTT, przynajmniej wtedy, gdy istnieje jasna teoria, w jaki sposób zaimplementować potrzebne funkcje. Okazało się to częściowo trudne.