Quelles parties de la théorie des types d'homotopie ne sont pas possibles dans Agda ou Coq?

Quand nous regardons le livre, Homotopy Type Theory - nous voyons les sujets suivants:

Homotopy type theory 
2.1 Types are higher groupoids
2.2 Functions are functors
2.3 Type families are ﬁbrations
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

Maintenant, nous savons que toute la théorie du type d'homotopie n'est pas possible avec Agda et Coq .

Ma question est: quelles parties de la théorie du type d'homotopie ne sont pas possibles dans Agda ou Coq?

type-systems oeil de faucon
la source

Pas une question particulièrement bien formulée. Quelle est la relation entre la liste des sujets et la question?

Dave Clarke

@Dave Clarke, La liste des sujets ressemble au contexte de l'esprit de l'interrogateur afin que celui-ci sache quel est le point de départ de l'interrogateur et peut adapter la réponse en conséquence. D'autres apprenants peuvent également apprécier la réponse dans le même contexte et comprendre que la réponse est susceptible de leur être utile si le répondeur est réfléchi et rusé en ce qui concerne la nature humaine. J'espère que cela aidera également dans d'autres conversations futures.

codeshot

Réponses:

Si vous regardez les notes sur le chapitre 8, vous verrez ce qui a déjà été officialisé, et je pense que c'est beaucoup. Il existe la bibliothèque Coq HoTT et la bibliothèque Agda HoTT-Agda qui formalisent de gros morceaux de la théorie des types d'homotopie.

Pour faire avancer les choses dans Coq, nous avions besoin d'une version spéciale de Coq qui a été corrigée uniquement pour HoTT. Cependant, Coq s'oriente vers la prise en charge de la théorie du type d'homotopie, donc d'ici peu nous pourrons être en mesure de le faire avec le Coq standard.

Dans Agda, il faut activer l' --without-Koption, sinon Agda pense que tous les types sont de type 0. Il y a des doutes persistants quant à savoir si l' --without-Kon se débarrasse vraiment de l'hypothèse que tout est un 0, ou peut-être pourrait-on le réintroduire dans Agda avec des utilisations délicates des correspondances de motifs.

Les aspects suivants des formalisations Coq et Agda ne sont pas satisfaisants:

L'axiome d'univalence est énoncé comme une hypothèse. Ce serait mieux s'il était intégré au système. En particulier, nous aimerions que Coq et Agda comprennent les règles de calcul concernant l'axiome d'univalence.
De même, nous devons utiliser des hacks pour obtenir des types inductifs supérieurs utilisables. Encore une fois, il serait préférable d'avoir un soutien direct.

Le problème avec les lacunes ci-dessus est que personne ne sait comment les corriger, même en théorie. Il s'agit d'un domaine de recherche actif.

En dehors de cela, je pense qu'il est juste de dire que HoTT peut être fait principalement à Coq et Agda, mais pas de manière optimale.

Andrej Bauer
la source

Merci, existe-t-il une bonne description des raisons pour lesquelles l'univalence et les types inductifs supérieurs ne conviennent pas aux théories de type comme Agda et Coq?

Martin Berger

@MartinBerger, cela pourrait probablement être une question distincte (avec quelques définitions pour les lecteurs plus occasionnels, etc.).

Artem Kaznatcheev

Le problème avec l'univalence et les HIT n'est pas qu'ils "ne correspondent pas bien aux théories de type comme Agda et Coq" mais que "nous ne savons pas comment les faire correctement dans aucune théorie de type".

Andrej Bauer

@AndrejBauer L'univalence et les types inductifs supérieurs sont formalisés dans l'écriture HoTT qui est une théorie de type (semi-formelle). Quel est l'ingrédient manquant qui empêche une formalisation appropriée dans Agda / Coq? En relation, si vous êtes prêt à abandonner Curry-Howard, y a-t-il des difficultés à formuler l'univalence et les types inductifs supérieurs dans un prouveur de style LCF, comme Isabelle, en utilisant par exemple LF comme méta-langage pour formaliser les règles de preuve?

Martin Berger

A quoi servent les règles de calcul ua, la constante qui témoigne de l'axiome d'univalence? Quelles sont les règles de calcul pour les HIT? Nous avons quelques idées, mais rien de étanche.

Andrej Bauer

D'après ce que je comprends, dans Agda, il est possible de représenter tout cela (c'est-à-dire tout le chapitre 2 - il y a une bibliothèque sur github qui le fait; AFAIK, la même chose est vraie de Coq). Ce n'est que lorsque vous accédez aux chapitres ultérieurs que les choses deviennent difficiles. Il y a deux éléments évidents:

Le cercle. Ceci est représenté (dans Agda) à l'aide d'un postulat , et n'est donc pas aussi agréable que d'autres choses.
$\infty$

Il y a aussi d'autres éléments, mais je n'ai pas encore lu cette partie de la formalisation Agda ... Mais dans l'ensemble, la plupart des HoTT peuvent être bien formalisés à la fois dans Agda et Coq.

Plus important encore, les deux équipes de développeurs travaillent activement à l'adaptation de leurs systèmes afin qu'une plus grande quantité de HoTT puisse être gérée, au moins chaque fois qu'il existe une théorie claire sur la façon de mettre en œuvre les fonctionnalités nécessaires. Cela s'est avéré difficile en partie.

Jacques Carette
la source