Combinatorial realizability models of type theory

DOI10.1016/J.APAL.2013.05.002zbMath1323.03013arXiv1205.5527OpenAlexW2096221521MaRDI QIDQ385804

Michael A. Warren, Pieter J. W. Hofstra

Publication date: 11 December 2013

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1205.5527

zbMATH Keywords

realizabilityMartin-Löf type theoryhomotopy type theorygluinglogical relationsgroupoid semantics

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Fibered categories (18D30) Foundations, relations to logic and deductive systems (18A15)

Related Items (6)

Homotopy type theory and Voevodsky’s univalent foundations ⋮ Martin-Löf complexes ⋮ Models of HoTT and the Constructive View of Theories ⋮ Univalence for inverse diagrams and homotopy canonicity ⋮ Monoidal computer III: a coalgebraic view of computability and complexity (extended abstract) ⋮ The least subtopos containing the discrete skeleton of \(\Omega\)

Cites Work

• Martin-Löf complexes
• The identity type weak factorisation system
• Internal type theory
• Type Theory and Homotopy
• Intensional interpretations of functionals of finite type I
• Unnamed Item
• Unnamed Item

This page was built for publication: Combinatorial realizability models of type theory