Combinatorial realizability models of type theory
Logic
2012-05-25 v1 Category Theory
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.
Keywords
Cite
@article{arxiv.1205.5527,
title = {Combinatorial realizability models of type theory},
author = {Pieter Hofstra and Michael A. Warren},
journal= {arXiv preprint arXiv:1205.5527},
year = {2012}
}
Comments
38 pages