Formalizowanie teorii typów homotopii w Idris

Patrząc na blog dotyczący teorii homotopii, łatwo można znaleźć wiele bibliotek formalizujących większość teorii typów homotopii w Agdzie i Coq.

Czy ktoś wie, czy istnieje podobna próba sformalizowania HoTT w Idris ?

proof-assistants homotopy-type-theory Giorgio Mossa
źródło

Nic mi nie wiadomo i spodziewam się, że prawdopodobnie usłyszelibyśmy o tym, gdyby ktoś spróbował (a przynajmniej odniósłby sukces).

Mike Shulman

@MikeShulman Czy systemy typu Idris i Agda nie powinny być zasadniczo równoważne? W takim przypadku powinna istnieć możliwość sformalizowania HoTT również w Idris, prawda?

Giorgio Mossa

Idris jest bardziej zorientowany na programowanie. Martwi mnie to, czy ma odpowiednik Agdy postulateczy Coq Axiom. Jeśli tak, to jak sobie z tym poradzić (to skompilowany język)? Chodzi o to, że aksjomat uniwalencyjności wymaga postulatededycji.

Andrej Bauer,

Z pewnością nie chciałem powiedzieć, że nie sądzę, że to możliwe! Po prostu nie znam nikogo, kto jeszcze tego próbował. Nic nie wiem o Idrisie.

Mike Shulman

Oczekuję, że Idris pozwoli ci udowodnić aksjomat K Streichera (unikalność dowodów tożsamości) poprzez dopasowanie wzorca (tak jak Agda do niedawna), co byłoby problemem dla HoTT.

Neel Krishnaswami

Odpowiedzi:

Oto mała, niekompletna i niespójna formalizacja HoTT w Idris. Pokazuje, że w Idris można wywrzeć sprzeczność, postulując jedność. W tej chwili istnieją dwie bariery w sformalizowaniu HoTT w Idris.

\prod_{P : X \to T y p e} \prod_{x : X} \prod_{p : x = x} \prod_{a, b : P x} (t r a n s p o r t P p a = b) \to (a = b)

$\prod_{P \,:\, X \to \mathsf{Type}}\ \prod_{x\,:\,X}\ \prod_{p \,:\, x = x}\ \prod_{a,\,b \,:\, P\, x} (\mathsf{transport}\ P\ p\ a = b) \to (a = b)$ True = False

Bariera 2: Dopasowywanie wzorów w Idris jest zbyt silne dla HoTT, jak podejrzewał Neel Krishnaswami w powyższym komentarzu. Możemy wyprowadzić Streichera K. Prowadzi to do wyjątkowości dowodów tożsamości, a zatem jest niezgodny z powszechnością. Możemy po raz kolejny pokazać True = False.

Francisco Mota
źródło