natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In type theory the unit type is the type with a unique term. It is the special case of a product type with no factors.
In a model by categorical semantics, this is a terminal object. In set theory, it is a singleton.
Like any type in type theory, the unit type is specified by rules saying when we can introduce it as a type, how to introduce terms of that type, how to use or eliminate terms of that type, and how to compute when we combine the constructors with the eliminators.
The unit type, like the binary product type, can be presented both as a positive type and as a negative type. There are typically two foundations in which the unit type is specified in, natural deduction and lambda-calculus.
We assume that our unit types have typal conversion rules, as those are the most general of the conversion rules. Both the propositional and judgmental conversion rules imply the typal conversion rules by the structural rules for propositional and judgmental equality respectively.
For both the positive unit type and the negative unit type, the formation and introduction rules are the same.
The formation rule for the unit type is given by
and the introduction rule for the unit type is given by
The positive unit type says that $\mathbb{1}$ satisfies singleton induction. The negative unit type says that the element $*:\mathbb{1}$ is the center of contraction of $\mathbb{1}$.
Singleton induction for a type $\mathbb{1}$ and term $*:\mathbb{1}$ states that the type has the following elimination rule, computation rule, and uniqueness rule:
Thus, the unit type satisfies singleton induction.
As a negative type, there are no elimination rules or computation rules for $\mathbb{1}$. The uniqueness rule states that $*$ is the center of contraction of $\mathbb{1}$ and is given by:
Thus, the unit type is a contractible type.
Let $\mathbb{1}$ denote the positive unit type, and let $p:\mathbb{1}$ and $q:\mathbb{1}$ be elements of $\mathbb{1}$. Then the identity type $q =_\mathbb{1} p$ is a contractible type.
Given an element $p:\mathbb{1}$, we can define the family of types $C(q) \coloneqq q =_\mathbb{1} p$ for all $q:\mathbb{1}$. The elimination and computation rules for the positive unit type imply that $* =_\mathbb{1} p$ is a contractible type with center of contraction $c_*(p):* =_\mathbb{1} p$ which is equal to $\mathrm{ind}_\mathbb{1}^{(-) =_\mathbb{1} p}(p, c_*(p))$.
The uniqueness rule for the positive unit type states that given a family of terms $u(p):q =_\mathbb{1} p$ indexed by $p:\mathbb{1}$ and $q:\mathbb{1}$, for all elements $c_*(p):* =_\mathbb{1} p$, elements $q:\mathbb{1}$, and witnesses $i_*(u(p))$ that $u(p)(*)$ is equal to $c_*(p)$ in $* =_\mathbb{1} p$, there is a witness $\eta_\mathbb{1}^{(-) =_\mathbb{1} p}(c_*(p), q, u(p), i_*(u(q)))$ that $u(p)$ is equal to $\mathrm{ind}_\mathbb{1}^{(-) =_\mathbb{1} p}(p, c_*(p))$ in $C(p)$.
Thus, the identity type $q =_\mathbb{1} p$ is a contractible type for all elements $p:\mathbb{1}$ and $q:\mathbb{1}$, with element $\eta_\mathbb{1}^{(-) =_\mathbb{1} p}(c_*(p), q, u(p), i_*(u(q))):q =_\mathbb{1} p$.
The positive unit type is a contractible type.
Since the identity type $q =_\mathbb{1} p$ is a contractible type for all elements $p:\mathbb{1}$ and $q:\mathbb{1}$, with element $\eta_\mathbb{1}^{(-) =_\mathbb{1} p}(c_*(p), q, u(p), i_*(u(q))):q =_\mathbb{1} p$, it follows that $\mathbb{1}$ is an h-proposition. Since $\mathbb{1}$ is also pointed with element $*:\mathbb{1}$, it is thus a contractible type.
There is an equivalence of types between two contractible types $S$ and $T$.
By the definition of contractible type, there are elements $p_S:\sum_{a:S} \prod_{b:S} a =_S b$ and $p_T:\sum_{a:T} \prod_{b:T} a =_T b$, and thus, an element $\pi_1(p_S)$ and a witness $\pi_2(p_S)$ that $\pi_1(p_S)$ is a center of contraction of $S$, and an element $\pi_1(p_T)$ and a witness $\pi_2(p_T)$ that $\pi_1(p_T)$ is a center of contraction of $T$. By the uniqueness principle of contractible types, it suffices to define a function $f:S \to T$ at $\pi_1(p_S)$. We define it as $f(\pi_1(p_S)) \coloneqq \pi_1(p_T)$. Now, all that’s left is to prove that the fiber of $f$ at all elements $a:T$ is contractible. But by the uniqueness principle of contractible types, it suffices to prove it for the center of contraction $\pi_1(p_T)$. The canonical element $*$ is in the fiber of $f$ at $\pi_1(p_T)$, and since $\pi_1(p_S)$ is the center of contraction of $S$, the fiber of $f$ at $\pi_1(p_T)$ is contractible, and thus the fiber of $f$ at every element $a:T$ is contractible. Thus, $f$ is an equivalence of types between the contractible types $S$ and $T$.
The positive and negative unit types are equivalent to each other.
Since the negative unit type is contractible by definition, and the positive unit type is contractible, they are equivalent to each other.
Then we could derive the extensionality principle for the unit type:
Given elements $x:\mathbb{1}$ and $y:\mathbb{1}$, there is an equivalence of types $(x =_\mathbb{1} y) \simeq \mathbb{1}$ between the identity type $x =_\mathbb{1} y$ and $\mathbb{1}$ itself.
Since every identity type $x =_\mathbb{1} y$ is contractible for elements $x:\mathbb{1}$ and $y:\mathbb{1}$, and $\mathbb{1}$ itself is contractible, this implies that every identity type $x =_\mathbb{1} y$ is equivalent to $\mathbb{1}$.
In set theory, regular and inaccessible cardinals are useful in determining size issues in strongly predicative and weakly predicative/impredicative mathematics respectively. Some definitions of regular and inaccessible cardinals do not have a requirement that the cardinals be infinite; thus finite cardinals such as $0$ and $1$ could be considered to be regular and inaccessible cardinals. Univalent universes in type theory which are closed under dependent sum types are the type theoretic equivalent of regular cardinals, and univalent universe which are additionally closed under power sets are the type theoretic equivalent of inaccessible cardinals.
We inductively define the type family $x:\mathbb{1} \vdash \mathrm{El}_\mathbb{1}(x) \; \mathrm{type}$ by defining
The extensionality principle for the unit type then is simply the univalence axiom:
The unit type $\mathbb{1}$ represents the trivial universe, the universe with only one element up to identification, where every type in the universe is a contractible type and thus every contractible type is essentially $\mathbb{1}$-small. The equivalence type between the two contractible types $\mathrm{El}_\mathbb{1}(x)$ and $\mathrm{El}_\mathbb{1}(y)$ is itself contractible and thus equivalent to $\mathbb{1}$ itself. As proven in the previous section, $\mathbb{1}$ is equivalent to $x =_\mathbb{1} y$ for any $x:\mathbb{1}$ and $y:\mathbb{1}$. Thus the univalence axiom for $\mathbb{1}$ is true.
In addition, given any type $A$, functions into the unit type $A \to \mathbb{1}$ are families of contractible types. The universe $(\mathbb{1}, \mathrm{El}_\mathbb{1})$ is also closed under dependent sum types, as for any family of contractible types $p:B \to \mathbb{1}$,
This makes the unit type into a Tarski universe representing a finite regular cardinal.
If the dependent type theory also has weak function extensionality, then the universe above is also closed under dependent product types, as weak function extensionality states that for any family of contractible types $p:B \to \mathbb{1}$,
making the unit type into a Tarski universe representing a finite product-regular cardinal.
As a universe, the unit type also satisfies propositional resizing: the type of all $\mathbb{1}$-small propositions is simply the unit type itself as a weakly Tarski universe, which is essentially $\mathbb{1}$-small. Thus, in the context of weak function extensionality, power sets exist in the unit type, making the unit type impredicative: power sets are just function types into the unit type. This makes the unit type into a Tarski universe representing a finite inaccessible cardinal.
The unit type is also the only universe which contains itself, as any univalent universe which contains the empty type and itself makes the entire dependent type theory inconsistent.
In lambda-calculus, for both the positive unit type and the negative unit type, the rule for building the unit type is the same, namely “it exists”:
Regarded as a positive type, we give primacy to the constructors, of which there is exactly one, denoted $()$ or $tt$.
The eliminator now says that to use something of type $1$, it suffices to say what to do in the case when that thing is $()$.
Obviously this is not very interesting, but this is what we get from the general rules of type theory in this degenerate case. In dependent type theory, we should also allow $C$ to depend on the unit type $1$.
We then have the ∞-reduction rule:
and (if we wish) the ∞-reduction rule:
The $\beta$-reduction rule is simple. The $\eta$-reduction rule says that if $c$ is an expression involving a variable $z$ of type $1$, and we substitute $()$ for $z$ in $c$ and use that (with the eliminator) to define a term involving another term $u$ of type $1$, then the result is the same as what we would get by substituting $u$ for $z$ in $c$ directly.
The positive presentation of the unit type is naturally expressed as an inductive type. In Coq syntax:
Inductive unit : Type :=
| tt : unit.
(Coq then implements beta-reduction, but not eta-reduction. However, eta-equivalence is provable with the internally defined identity type, using the dependent eliminator mentioned above.)
A negative type is characterized by its eliminators, which is a little subtle for the unit type. But by analogy with binary product types, which have two eliminators $\pi_1$ and $\pi_2$ when presented negatively, the negative unit type (a nullary product) should have no eliminators at all.
To derive the constructors from this, we follow the general rule for negative types that to construct an element of $1$, it should suffice to specify how that element behaves under all the eliminators. Since there are no eliminators, this means we have nothing to do; thus we have exactly one way to construct an element of $1$, by doing nothing:
There is no $\beta$-reduction rule, since there are no eliminators to compose with the constructor. However, there is an $\eta$-conversion rule. In general, an $\eta$-redex? consists of a constructor whose inputs are all obtained from eliminators. Here we have a constructor which has no inputs, so it is not a problem that we have no eliminators to fill them in with. Thus, the term $()\colon 1$ is an “$\eta$-redex”, and it “reduces” to any term of type $1$ at all:
This is obviously not a well-defined “operation”, so in this case it is better to view $\eta$-conversion in terms of expansion:
In ordinary “nonlinear” type theory, the positive and negative unit types are equivalent. They manifestly have the same constructor, while we can define the positive eliminator in a trivial way as
Note that just as for binary product types, in order for this to be a well-typed definition of the dependent eliminator in dependent type theory, we need to assume the $\eta$-conversion rule for the assumed negative unit type (at least, propositionally).
Of course, the positive $\beta$-reduction rule holds by definition for the above defined eliminator.
For the $\eta$-conversion rules, if we start from the negative presentation and define the positive eliminator as above, then $let () = u in c[()/z]$ is precisely $c[()/z]$, which is convertible to $c[u/z]$ by the negative $\eta$-conversion rule $() \;\leftrightarrow_\eta\; u$.
Conversely, if we start from the positive presentation, then we have
where in the first conversion we use $c \coloneqq ()$ and in the second we use $c\coloneqq z$.
As in the case of binary product types, these translations require the contraction rule and the weakening rule; that is, they duplicate and discard terms. In linear logic these rules are disallowed, and therefore the positive and negative unit types become different. The positive product becomes “one” $\mathbf{1}$, while the negative product becomes “top” $\top$.
There are two interpretations of the unit type, corresponding to the positive and negative unit types. Namely:
The negative unit type corresponds to a terminal object in a category
The positive unit type with both $\beta$-conversion and $\eta$-conversion corresponds to an initial object with a point, a morphism from some unit object $I$ to the object corresponding to the unit type, in a category.
These two conditions are the same if the syntactic category is a cartesian monoidal category, where the points are the global elements and the unit is the terminal object. In general, however, the points may not be defined out of the terminal object. In linear logic, therefore, the categorical terminal object interprets “top” $\top$, while the unit object of an additional monoidal structure interprets “one” $\mathbf{1}$.
On the unit type as an inductive type satisfying singleton induction:
Univalent Foundations Project, p. 30 Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]
Egbert Rijke, Def. 3.1.1 in: Introduction to Homotopy Type Theory, lecture notes, CMU (2018) [pdf, pdf, webpage]
homotopy level | n-truncation | homotopy theory | higher category theory | higher topos theory | homotopy type theory |
---|---|---|---|---|---|
h-level 0 | (-2)-truncated | contractible space | (-2)-groupoid | true/unit type/contractible type | |
h-level 1 | (-1)-truncated | contractible-if-inhabited | (-1)-groupoid/truth value | (0,1)-sheaf/ideal | mere proposition/h-proposition |
h-level 2 | 0-truncated | homotopy 0-type | 0-groupoid/set | sheaf | h-set |
h-level 3 | 1-truncated | homotopy 1-type | 1-groupoid/groupoid | (2,1)-sheaf/stack | h-groupoid |
h-level 4 | 2-truncated | homotopy 2-type | 2-groupoid | (3,1)-sheaf/2-stack | h-2-groupoid |
h-level 5 | 3-truncated | homotopy 3-type | 3-groupoid | (4,1)-sheaf/3-stack | h-3-groupoid |
h-level $n+2$ | $n$-truncated | homotopy n-type | n-groupoid | (n+1,1)-sheaf/n-stack | h-$n$-groupoid |
h-level $\infty$ | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h-$\infty$-groupoid |
Last revised on March 27, 2023 at 11:15:23. See the history of this page for a list of all contributions to it.