| ||||
| ||||
![]() Title:Groupoidal Realizability: Formalizing the Topological BHK Interpretation Authors:Sam Speight Conference:HoTT/UF 2022 Tags:Assemblies, Groupoids, Impredicative universe and Realizability Abstract: We develop groupoidal realizability models of intensional type theory, wherein realizers themselves carry higher-dimensional structure. This can be understood as a formalization of an extension/modification of the BHK interpretation such that evidence for an identification of two objects is a path between them. Groupoidal Realizability: Formalizing the Topological BHK Interpretation ![]() Groupoidal Realizability: Formalizing the Topological BHK Interpretation | ||||
Copyright © 2002 – 2025 EasyChair |