Formalización de la teoría del tipo de homotopía en Idris

Mirando el blog de teoría de tipos de homotopía, se puede encontrar fácilmente una gran cantidad de bibliotecas que formalizan la mayoría de la teoría de tipos de homotopía en Agda y Coq.

¿Alguien sabe si hay algún intento similar de formalizar HoTT en Idris ?

proof-assistants homotopy-type-theory Giorgio Mossa
fuente

No conozco ninguno, y espero que probablemente hubiéramos oído hablar de eso si alguien lo hubiera intentado (o al menos si hubiera tenido éxito).

Mike Shulman

@MikeShulman ¿No deberían ser los sistemas de tipo Idris y Agda esencialmente equivalentes? En ese caso, también debería ser posible formalizar HoTT en Idris, ¿no?

Giorgio Mossa

Idris está más orientado a la programación. Una cosa que me preocuparía es si tiene el equivalente de Agda postulateo Coq Axiom. Si es así, ¿cómo logra calcular con él (es un lenguaje compilado)? El punto es que el axioma de univalencia necesita ser postulatededitado.

Andrej Bauer

¡Ciertamente no quise decir que no creía que fuera posible! Simplemente no conozco a nadie que lo haya probado todavía. No sé casi nada sobre Idris.

Mike Shulman

Espero que Idris le permita probar el axioma K de Streicher (singularidad de las pruebas de identidad) a través de la coincidencia de patrones (como lo hizo Agda hasta hace poco), lo que sería un problema para HoTT.

Neel Krishnaswami

Respuestas:

Aquí hay una formalización pequeña, incompleta e inconsistente de HoTT en Idris. Demuestra que puedes derivar una contradicción en Idris simplemente postulando univalencia. Hay dos barreras para formalizar HoTT en Idris en este momento.

\prod_{PAG : X \to T y pag mi} \prod_{X : X} \prod_{pag : X = X} \prod_{un, si : PAG X} (t r un norte s pag o r t PAG pag un = si) \to (un = si)

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

Barrera 2: La coincidencia de patrones en Idris es demasiado fuerte para HoTT, como Neel Krishnaswami sospechaba en un comentario anterior. Podemos derivar Streicher's K. Esto conduce a la unicidad de las pruebas de identidad, y por lo tanto es incompatible con la univalencia. Podemos mostrar una vez más True = False.

Francisco Mota
fuente