%0 Generic %1 hofstra2012combinatorial %A Hofstra, Pieter %A Warren, Michael A. %D 2012 %K HoTT model realizability %T Combinatorial realizability models of type theory %U http://arxiv.org/abs/1205.5527 %X We introduce a new model construction for Martin-Lö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.

@misc{hofstra2012combinatorial, 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.}, added-at = {2015-01-01T06:35:52.000+0100}, author = {Hofstra, Pieter and Warren, Michael A.}, biburl = {https://www.bibsonomy.org/bibtex/2cb153730ab82008a6ae1e43a68cfb78d/t.uemura}, description = {[1205.5527] Combinatorial realizability models of type theory}, interhash = {16299fa704b7a49504ba9af67245757a}, intrahash = {cb153730ab82008a6ae1e43a68cfb78d}, keywords = {HoTT model realizability}, note = {cite \href{http://arxiv.org/abs/1205.5527}{arxiv:1205.5527}Comment: 38 pages}, timestamp = {2015-01-01T06:35:52.000+0100}, title = {Combinatorial realizability models of type theory}, url = {http://arxiv.org/abs/1205.5527}, year = 2012 }