Skip to Main content Skip to Navigation
Master thesis

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.
Complete list of metadata

https://hal.inria.fr/hal-01626651
Contributor : Théo Winterhalter <>
Submitted on : Tuesday, October 31, 2017 - 1:19:38 PM
Last modification on : Monday, February 15, 2021 - 10:38:18 AM
Long-term archiving on: : Thursday, February 1, 2018 - 12:36:11 PM

Files

Identifiers

  • 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⟩

Share

Metrics

Record views

349

Files downloads

119