Combinatorial realizability models of type theory

DOI10.1016/J.APAL.2013.05.002zbMATH Open1323.03013arXiv1205.5527OpenAlexW2096221521MaRDI QIDQ385804FDOQ385804

Pieter Hofstra, Michael A. Warren

Publication date: 11 December 2013

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

Abstract: We introduce a new model construction for Martin-L"{o}f intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines the syntactic model with a notion of realizability; it also encompasses the well-known Hofmann- Streicher groupoid semantics. As our main application, we use the model to analyse the syntactic groupoid associated to the type theory generated by a graph G, showing that it has the same homotopy type as the free groupoid generated by G.

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

Recommendations

• Homotopy-theoretic models of type theory
• Martin-Löf complexes
• Homotopy theoretic models of identity types
• Models of type theory based on Moore paths
• Models of Type Theory Based on Moore Paths

zbMATH Keywords

realizabilitygluinglogical relations[https://portal.mardi4nfdi.de/w/index.php?title=+Special%3ASearch&search=Martin-L%EF%BF%BD%EF%BF%BDf+type+theory&go=Go Martin-L��f type theory]groupoid semanticshomotopy type theory

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• The identity type weak factorisation system
• Internal type theory
• Martin-Löf complexes
• Type Theory and Homotopy
• Intensional interpretations of functionals of finite type I

Cited In (9)

• Univalence for inverse diagrams and homotopy canonicity
• Title not available (Why is that?)
• Martin-Löf complexes
• The least subtopos containing the discrete skeleton of \(\Omega\)
• Models of HoTT and the Constructive View of Theories
• A completeness result for a realisability semantics for an intersection type system
• Homotopy type theory and Voevodsky’s univalent foundations
• Monoidal computer III: a coalgebraic view of computability and complexity (extended abstract)
• Title not available (Why is that?)

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q385804)