Higher-dimensional realizability for intensional type theory
<p>We develop realizability models of intensional type theory, based on groupoids, wherein realizers themselves carry higher-dimensional structure. In the spirit of realizability this is intended to formalise a higher-dimensional (topological, homotopical) BHK interpretation whereby evidence f...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
2023
|
| Subjects: |