Formalizando a teoria do tipo de homotopia em Idris

Olhando para o blog da teoria dos tipos de homotopia, é fácil encontrar muitas bibliotecas formalizando a maior parte da teoria dos tipos de homotopia em Agda e Coq.

Alguém sabe se existe alguma tentativa semelhante de formalizar o HoTT em Idris ?

proof-assistants homotopy-type-theory Giorgio Mossa
fonte

Não conheço ninguém, e espero que provavelmente teríamos ouvido falar sobre isso se alguém tivesse tentado (ou pelo menos se tivesse conseguido).

Mike Shulman

@ MikeShulman Os sistemas de tipo Idris e Agda não devem ser essencialmente equivalentes? Nesse caso, deveria ser possível formalizar o HoTT em Idris também, não deveria?

Giorgio Mossa

Idris é mais fortemente orientado para a programação. Uma coisa que me preocuparia é se ela tem o equivalente da Agda postulateou da Coq Axiom. Se sim, como ele consegue computar com ele (é uma linguagem compilada)? O ponto é que o axioma da univalência precisa ser postulatededitado.

Andrej Bauer

Eu certamente não quis dizer que não achava que seria possível! Só não conheço ninguém que tenha tentado ainda. Não sei quase nada sobre Idris.

Mike Shulman

Espero que Idris permita que você prove o axioma K de Streicher (exclusividade de provas de identidade) por meio de correspondência de padrões (como a Agda fez até recentemente), o que seria um problema para o HoTT.

Neel Krishnaswami

Respostas:

Aqui está uma formalização pequena, incompleta e inconsistente do HoTT em Idris. Isso mostra que você pode derivar uma contradição em Idris apenas postulando univalência. No momento, existem duas barreiras para formalizar o HoTT em Idris.

\prod_{P : X \to T y p e} \prod_{x : X} \prod_{p : x = x} \prod_{uma, b : P x} (t r uma n s p o r t P p uma = b) \to (uma = 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

Barreira 2: O padrão de correspondência em Idris é muito forte para o HoTT, como Neel Krishnaswami suspeitava em um comentário acima. Podemos derivar o K. de Streicher. Isso leva à singularidade das provas de identidade e, portanto, é incompatível com a univalência. Podemos mostrar mais uma vez True = False.

Francisco Mota
fonte