License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2014.202
URN: urn:nbn:de:0030-drops-54980
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5498/
Go to the corresponding LIPIcs Volume Portal

Pitts, Andrew M.

Nominal Presentation of Cubical Sets Models of Type Theory

pdf-format:
12.pdf (0.5 MB)

Abstract

The cubical sets model of Homotopy Type Theory introduced by Bezem, Coquand and Huber uses a particular category of presheaves. We show that this presheaf category is equivalent to a category of sets equipped with an action of a monoid of name substitutions for which a finite support property holds. That category is in turn isomorphic to a category of nominal sets equipped with operations for substituting constants 0 and 1 for names. This formulation of cubical sets brings out the potentially useful connection that exists between the homotopical notion of path and the nominal sets notion of name abstraction. The formulation in terms of actions of monoids of name substitutions also encompasses a variant category of cubical sets with diagonals, equivalent to presheaves on Grothendieck's "smallest test category." We show that this category has the pleasant property that path objects given by name abstraction are exponentials with respect to an interval object.

BibTeX - Entry

@InProceedings{pitts:LIPIcs:2015:5498,
  author =	{Andrew M. Pitts},
  title =	{{Nominal Presentation of Cubical Sets Models of Type Theory}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{202--220},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5498},
  URN =		{urn:nbn:de:0030-drops-54980},
  doi =		{10.4230/LIPIcs.TYPES.2014.202},
  annote =	{Keywords: models of dependent type theory, homotopy type theory, cubical sets, nominal sets, monoids}
}

Keywords: models of dependent type theory, homotopy type theory, cubical sets, nominal sets, monoids
Collection: 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Issue Date: 2015
Date of publication: 12.10.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI