How do I read $\star$ the only inhabitant of the type $ \mathbf{1} $ in HoTT and Martin Lof

Question

When I read the $ \star $ symbol out loud to myself how should I pronounce it? Also when dealing with type theories like HoTT and Martin Lof what should I be regarding $ \star : \mathbf{1} $ as?

Answer 1

Type theory people usually use the term "unit", though they often explicitly represent that type as an empty tuple. For example, in the programming language Haskell the type (and value) are written (). You'll also see $\langle\rangle : \mathbf{1}$. $\mathbf{1}$ is called the "unit type". Any closed term is a (global) point, so using the term "point" is ambiguous (though global points are closely related to the unit type.) Even ignoring that ambiguity, "point" will mean little to many people coming from a more logic/computer science background.

From a topological perspective, it would make more sense to read $\mathbf{1}$ as "point" rather than its value, though I recommend the "unit type" terminology over this. The idea here is that we may have a type like $\mathbb{S}^1$ that represents a circle, and we think of functions $\mathbb{S}^1 \to X$ as the "circles in $X$". Functions $\mathbf{1}\to X$ would then be the "points in $X$". ($\mathbf{1}$ is sometimes written "pt" in this context.) We don't call the values of $\mathbb{S}^1$ circles, though. Traditionally, in set theory and point-set topology, we do call the elements of $\mathbb{S}^1$ the "points" of $\mathbb{S}^1$. In set theory there's no issue because there's a (natural) bijection between the functions $\mathbf{1}\to X$ and the elements of $X$.

Via the Curry-Howard correspondence, the unit type corresponds to the trivially true proposition. Categorically, the unit type corresponds to a terminal object. In the category of sets, any singleton set works as "the" terminal object. Often for concreteness, something like $\{*\}$ or $\{\star\}$ is used. The $*$ or $\star$ is just meant as a meaningless name for the meaningless element. Something like $\{\{\}\}$ or $\{0\}$ could be used, but this may suggest some significance that doesn't exist.

The empty tuple/product interpretation is probably the best way to think about it in general. It is virtually always an accurate interpretation. For example, in (classical) homotopy, we might represent a path as a function from an interval $[0,1]\to X$. This is a 1-dimensional object. Homotopies correspond to surfaces and are represented by functions $[0,1]\times[0,1]\to X$. Higher homotopies have higher-dimensional inputs. The 0-dimensional case, i.e. a point, would then be a function $\mathbf{1}\to X$.