Nominal Presentation of Cubical Sets Models of Type Theory
Andrew M. Pitts
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.