Combinatorial realizability models of type theory
classification
🧮 math.LO
math.CT
keywords
modeltheorytypegroupoidgeneratedrealizabilitysyntacticanalyse
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.