Combinatorial realizability models of type theory

DOI10.1016/J.APAL.2013.05.002MaRDI QIDQ385804zbMATH OpenOpenAlexFDO

Authors Michael A. Warren, Pieter 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

realizabilitygluinglogical relationsgroupoid semanticshomotopy type theoryMartin-Löf type theory

Mathematics Subject Classification ID

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

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.

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

Cites work

• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• Internal type theory
• Martin-Löf complexes
• The identity type weak factorisation system
• Type theory and homotopy

Cited in

(9)

• Homotopy type theory and Voevodsky's univalent foundations
• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• Monoidal computer. III: A coalgebraic view of computability and complexity (extended abstract)
• Models of HoTT and the Constructive View of Theories
• scientific article; zbMATH DE number 1841819 (Why is no real title available?)
• Martin-Löf complexes
• Univalence for inverse diagrams and homotopy canonicity
• The least subtopos containing the discrete skeleton of \(\Omega\)
• A completeness result for a realisability semantics for an intersection type system

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)