nLab
unit type

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty 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
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

homotopy levels

semantics

Contents

Idea

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.

Definition

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”:

1:Type \frac{ }{1\colon Type}

As a positive type

Regarded as a positive type, we give primacy to the constructors, of which there is exactly one, denoted ()() or tttt.

():1 \frac{ }{() \colon 1 }

The eliminator now says that to use something of type 11, it suffices to say what to do in the case when that thing is ()().

c:Cu:1let()=uinc:C \frac{\vdash c\colon C}{u\colon 1 \vdash let () = u in c \;\colon C}

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 CC to depend on the unit type 11.

We then have the β-reduction rule:

let()=()inc βc let () = () in c \;\to_\beta\; c

and (if we wish) the η-reduction rule:

let()=uinc[()/z] ηc[u/z]. let () = u in c[()/z] \;\to_\eta\; c[u/z].

The β\beta-reduction rule is simple. The η\eta-reduction rule says that if cc is an expression involving a variable zz of type 11, and we substitute ()() for zz in cc and use that (with the eliminator) to define a term involving another term uu of type 11, then the result is the same as what we would get by substituting uu for zz in cc 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.)

As a negative type

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 π 1\pi_1 and π 2\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 11, 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 11, by doing nothing:

():1\frac{ }{()\colon 1}

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 ():1()\colon 1 is an “η\eta-redex”, and it “reduces” to any term of type 11 at all:

() ηu () \;\to_\eta\; u

This is obviously not a well-defined “operation”, so in this case it is better to view η\eta-conversion in terms of expansion:

u η(). u \;\to_\eta\; ().

Positive versus negative

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

let()=uincc let () = u in c \quad \coloneqq\quad c

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()=uinc[()/z]let () = u in c[()/z] is precisely c[()/z]c[()/z], which is convertible to c[u/z]c[u/z] by the negative η\eta-conversion rule () ηu() \;\leftrightarrow_\eta\; u.

Conversely, if we start from the positive presentation, then we have

() ηlet()=uin() ηu () \;\leftrightarrow_\eta\; let () = u in () \;\leftrightarrow_\eta\; u

where in the first conversion we use c()c \coloneqq () and in the second we use czc\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” 1\mathbf{1}, while the negative product becomes “top” \top.

Properties

Proposition

In homotopy type theory the unit type is a contractible type, and every contractible type is equivalent to the unit type.

Categorical semantics

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” 1\mathbf{1}.

homotopy leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/unit type/contractible type
h-level 1(-1)-truncated(-1)-groupoid/truth valuemere proposition, h-proposition
h-level 20-truncateddiscrete space0-groupoid/setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/groupoid(2,1)-sheaf/stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoidh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoidh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoidh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/∞-stackh-\infty-groupoid

Revised on September 10, 2012 20:22:12 by Urs Schreiber (131.174.188.17)