A Restricted Version of Reflection Compatible with Univalent Homotopy Type Theory
Résumé
We present our work conducted on the relation between the different notions of equality in type theory, particularly in the setting of homotopy type theory. We offer a novel notion of restricted reflection that is still consistent in a univalent setting while allowing us to derive useful applications in the field of interactive proving.
Fichier principal
main.pdf (416.16 Ko)
Télécharger le fichier
main (1).pdf (334.9 Ko)
Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)