¿Qué partes de la teoría del tipo de homotopía no son posibles en Agda o Coq?

16

Cuando miramos el libro, Teoría del tipo de homotopía , vemos los siguientes temas:

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

Ahora sabemos que no toda la teoría del tipo de homotopía es posible es Agda y Coq .

Mi pregunta es: ¿Qué partes de la teoría del tipo de homotopía no son posibles en Agda o Coq?

type-systems ojo de halcón
fuente
44
No es una pregunta especialmente bien formulada. ¿Cuál es la relación entre la lista de temas y la pregunta?
Dave Clarke
@Dave Clarke, La lista de temas se parece al contexto de la mente del interrogador para que el respondedor sepa cuál es el punto de partida del interlocutor y pueda adaptar la respuesta en consecuencia. Otros estudiantes también pueden apreciar la respuesta en el mismo contexto y comprender que la respuesta probablemente sea útil para ellos si el que responde es reflexivo y astuto con respecto a la naturaleza humana. Espero que eso también ayude en otras conversaciones futuras.
código de

Respuestas:

21

Si nos fijamos en Notas sobre el capítulo 8 verá lo que ha sido ya formalizada, y creo que eso es mucho. Existen la biblioteca Coq HoTT y la biblioteca Agda HoTT-Agda que formalizan grandes fragmentos de la teoría de tipos de homotopía.

Para hacer las cosas en Coq, necesitábamos una versión especial de Coq que fue parcheada solo para los propósitos de HoTT. Sin embargo, Coq se está moviendo en la dirección de apoyar la teoría del tipo de homotopía, por lo que en poco tiempo podríamos hacerlo con Coq estándar.

En Agda, uno tiene que activar la --without-Kopción; de lo contrario, Agda piensa que todos los tipos son de tipo 0. Hay algunas dudas persistentes sobre si --without-Krealmente se elimina la suposición de que todo es un conjunto de 0, o tal vez uno podría reintroducirlo en Agda con usos complicados de coincidencias de patrones.

Los siguientes aspectos de las formalizaciones de Coq y Agda no son satisfactorios:

  1. El axioma de la univalencia se establece como una hipótesis. Sería mejor si se integrara en el sistema. En particular, nos gustaría que Coq y Agda entiendan las reglas de cálculo sobre el axioma de Univalencia.

  2. Del mismo modo, tenemos que usar hacks para obtener tipos viables de mayor inductividad. Una vez más, sería mejor tener un apoyo directo.

El problema con las deficiencias anteriores es que nadie sabe cómo solucionarlas, incluso en teoría. Esta es un área activa de investigación.

Aparte de eso, creo que es justo decir que HoTT se puede hacer principalmente en Coq y Agda, pero no de la manera óptima.

Andrej Bauer
fuente
1
Gracias, ¿hay una buena descripción de por qué la univalencia y los tipos inductivos superiores no se ajustan bien a las teorías de tipos como Agda y Coq?
Martin Berger
1
@MartinBerger esta podría ser una pregunta separada (con algunas definiciones para lectores más casuales, etc.).
Artem Kaznatcheev
44
El problema con la univalencia y los HIT no es que "no se sientan bien con las teorías de tipos como Agda y Coq", sino que "no sabemos cómo hacerlas correctamente en ninguna teoría de tipos".
Andrej Bauer
1
@AndrejBauer La univalencia y los tipos inductivos superiores están formateados en la escritura HoTT, que es una teoría de tipos (semi-formal). ¿Cuál es el ingrediente que falta que impide una formalización adecuada en Agda / Coq? Relacionado, si está dispuesto a renunciar a Curry-Howard, ¿hay alguna dificultad para formular univalencia y tipos inductivos más altos en un probador de estilo LCF, como Isabelle, que usa, por ejemplo, LF como metalenguaje para formalizar reglas de prueba?
Martin Berger
44
¿Para qué son las reglas de cálculo ua, la constante que presencia el axioma de Univalencia? ¿Cuáles son las reglas de cálculo para los HIT? Tenemos algunas ideas, pero nada hermético.
Andrej Bauer
12

Por lo que entiendo, en Agda es posible representar todo eso (es decir, todo el Capítulo 2: hay una biblioteca en github que sí; AFAIK, lo mismo es cierto para Coq). Es solo cuando llegas a capítulos posteriores que las cosas se ponen difíciles. Hay dos elementos obvios:

  1. El círculo. Esto se representa (en Agda) usando un postulado , por lo que no es tan bueno como otras cosas.
  2. ∞

También hay otros elementos, pero todavía no he leído esa parte de la formalización de Agda ... Pero, en general, la mayoría de HoTT se puede formalizar bien tanto en Agda como en Coq.

Más importante aún, ambos equipos de desarrolladores están trabajando activamente en la adaptación de sus sistemas para que se pueda manejar más HoTT, al menos siempre que haya una teoría clara de cómo implementar las características necesarias. Eso ha resultado ser un desafío en partes.

Jacques Carette
fuente