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
logic | category theory | type theory |
---|---|---|
true | terminal object/(-2)-truncated object | h-level 0-type/unit type |
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language
</table>
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 construct 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 a negative type. In both cases 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$.
In homotopy type theory the unit type is a contractible type, and every contractible type is equivalent to the unit type.
Under categorical semantics, a unit type satisfying both beta and eta conversions corresponds to a terminal object in a category. More precisely:
A terminal object may be used to interpret a unit type that validates both beta and eta rules, while
the syntactic category of a type theory with a unit type has a terminal object, as long as the unit type satisfies both beta and eta rules.
Of course, the categorical notion of terminal object matches the negative definition of a unit type most directly. In linear logic, therefore, the categorical terminal object interprets “top” $\top$, while the unit object of an additional monoidal structure interprets “one” $\mathbf{1}$.
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 September 10, 2012 at 20:22:12. See the history of this page for a list of all contributions to it.