A Restricted Version of Reflection Compatible with Univalent Homotopy Type Theory

Abstract : 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.
Type de document :
Mémoires d'étudiants -- Hal-inria+
Logic in Computer Science [cs.LO]. 2017
Liste complète des métadonnées

https://hal.inria.fr/hal-01626651
Contributeur : Théo Winterhalter <>
Soumis le : mardi 31 octobre 2017 - 13:19:38
Dernière modification le : jeudi 19 avril 2018 - 11:46:05
Document(s) archivé(s) le : jeudi 1 février 2018 - 12:36:11

Identifiants

  • HAL Id : hal-01626651, version 1

Citation

Théo Winterhalter. A Restricted Version of Reflection Compatible with Univalent Homotopy Type Theory. Logic in Computer Science [cs.LO]. 2017. 〈hal-01626651〉

Partager

Métriques

Consultations de la notice

105

Téléchargements de fichiers

46