nLab unit type

Redirected from "unit types".
Contents

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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 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.

In natural deduction

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

ΓctxΓ𝟙type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{1} \; \mathrm{type}}

and the introduction rule for the unit type is given by

ΓctxΓ*:𝟙\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash *:\mathbb{1}}

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}.

As a positive type

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:

  • given a type family C(x)C(x) indexed by 𝟙\mathbb{1}, for all elements x:𝟙x:\mathbb{1} and c:C(*)c:C(*), there is an element ind 𝟙 C(x,c):C(x)\mathrm{ind}_\mathbb{1}^C(x, c):C(x).
Γ,x:𝟙C(x)typeΓ,x:𝟙,c:C(*)ind 𝟙 C(x,c):C(x)\frac{\Gamma, x:\mathbb{1} \vdash C(x) \; \mathrm{type}}{\Gamma, x:\mathbb{1}, c:C(*) \vdash \mathrm{ind}_\mathbb{1}^C(x, c):C(x)}
  • given a type family C(x)C(x) indexed by 𝟙\mathbb{1}, for all elements c:C(*)c:C(*), the element ind 𝟙 C(*,c)\mathrm{ind}_\mathbb{1}^C(*, c) derived from the elimination rule is equal to cc with witness β 𝟙 C(c)\beta_\mathbb{1}^C(c).
Γ,x:𝟙C(x)typeΓ,c *:C(*)β 𝟙 C(c):ind 𝟙 C(*,c)= C(*)c\frac{\Gamma, x:\mathbb{1} \vdash C(x) \; \mathrm{type}}{\Gamma, c_*:C(*) \vdash \beta_\mathbb{1}^C(c):\mathrm{ind}_\mathbb{1}^C(*, c) =_{C(*)} c}
  • given a type family C(x)C(x) indexed by 𝟙\mathbb{1} and a family of elements u(x):C(x)u(x):C(x) indexed by 𝟙\mathbb{1}, for all elements x:𝟙x:\mathbb{1} there is a witness η 𝟙 C(x,u(x))\eta_\mathbb{1}^C(x, u(x)) that u(x)u(x) is equal to ind 𝟙 C(x,u(*))\mathrm{ind}_\mathbb{1}^{C}(x, u(*)) in C(x)C(x).
Γ,x:𝟙C(x)typeΓ,x:𝟙u(x):C(x)Γ,x:𝟙η 𝟙 C(x,u(x)):u(x)= C(x)ind 𝟙 C(x,u(*))\frac{\Gamma, x:\mathbb{1} \vdash C(x) \; \mathrm{type} \quad \Gamma, x:\mathbb{1} \vdash u(x):C(x)}{\Gamma, x:\mathbb{1} \vdash \eta_\mathbb{1}^C(x, u(x)):u(x) =_{C(x)} \mathrm{ind}_\mathbb{1}^{C}(x, u(*))}

Thus, the unit type satisfies singleton induction.

In type theories with a separate type judgment where not all types are elements of universes, one has to additionally add the following elimination and computation rules:

Elimination rules:

ΓAtypeΓ,x:𝟙typerec 𝟙 A(x)type\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:\mathbb{1} \vdash \mathrm{typerec}_{\mathbb{1}}^{A}(x) \; \mathrm{type}}

Computation rules:

  • judgmental computation rules
ΓAtypeΓtyperec 𝟙 A(*)Atype\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{typerec}_{\mathbb{1}}^{A}(*) \equiv A \; \mathrm{type}}
  • typal computation rules
    ΓAtypeΓβ 𝟙 A:typerec 𝟙 A(*)A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \beta_{\mathbb{1}}^{A}:\mathrm{typerec}_{\mathbb{1}}^{A}(*) \simeq A}

As a negative type

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:

ΓctxΓ,p:𝟙η 𝟙(p):*= 𝟙p\frac{\Gamma \; \mathrm{ctx}}{\Gamma, p:\mathbb{1} \vdash \eta_\mathbb{1}(p):* =_\mathbb{1} p}

Thus, the unit type is a contractible type.

Positive versus negative

Theorem

Let 𝟙\mathbb{1} denote the positive unit type, and let p:𝟙p:\mathbb{1} and q:𝟙q:\mathbb{1} be elements of 𝟙\mathbb{1}. Then the identity type q= 𝟙pq =_\mathbb{1} p is a contractible type.

Proof

Given an element p:𝟙p:\mathbb{1}, we can define the family of types C(q)q= 𝟙pC(q) \coloneqq q =_\mathbb{1} p for all q:𝟙q:\mathbb{1}. The elimination and computation rules for the positive unit type imply that *= 𝟙p* =_\mathbb{1} p is a contractible type with center of contraction c *(p):*= 𝟙pc_*(p):* =_\mathbb{1} p which is equal to ind 𝟙 ()= 𝟙p(p,c *(p))\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= 𝟙pu(p):q =_\mathbb{1} p indexed by p:𝟙p:\mathbb{1} and q:𝟙q:\mathbb{1}, for all elements c *(p):*= 𝟙pc_*(p):* =_\mathbb{1} p, elements q:𝟙q:\mathbb{1}, and witnesses i *(u(p))i_*(u(p)) that u(p)(*)u(p)(*) is equal to c *(p)c_*(p) in *= 𝟙p* =_\mathbb{1} p, there is a witness η 𝟙 ()= 𝟙p(c *(p),q,u(p),i *(u(q)))\eta_\mathbb{1}^{(-) =_\mathbb{1} p}(c_*(p), q, u(p), i_*(u(q))) that u(p)u(p) is equal to ind 𝟙 ()= 𝟙p(p,c *(p))\mathrm{ind}_\mathbb{1}^{(-) =_\mathbb{1} p}(p, c_*(p)) in C(p)C(p).

Thus, the identity type q= 𝟙pq =_\mathbb{1} p is a contractible type for all elements p:𝟙p:\mathbb{1} and q:𝟙q:\mathbb{1}, with element η 𝟙 ()= 𝟙p(c *(p),q,u(p),i *(u(q))):q= 𝟙p\eta_\mathbb{1}^{(-) =_\mathbb{1} p}(c_*(p), q, u(p), i_*(u(q))):q =_\mathbb{1} p.

Lemma

The positive unit type is a contractible type.

Proof

Since the identity type q= 𝟙pq =_\mathbb{1} p is a contractible type for all elements p:𝟙p:\mathbb{1} and q:𝟙q:\mathbb{1}, with element η 𝟙 ()= 𝟙p(c *(p),q,u(p),i *(u(q))):q= 𝟙p\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.

Theorem

There is an equivalence of types between two contractible types SS and TT.

Proof

By the definition of contractible type, there are elements p S: a:S b:Sa= Sbp_S:\sum_{a:S} \prod_{b:S} a =_S b and p T: a:T b:Ta= Tbp_T:\sum_{a:T} \prod_{b:T} a =_T b, and thus, an element π 1(p S)\pi_1(p_S) and a witness π 2(p S)\pi_2(p_S) that π 1(p S)\pi_1(p_S) is a center of contraction of SS, and an element π 1(p T)\pi_1(p_T) and a witness π 2(p T)\pi_2(p_T) that π 1(p T)\pi_1(p_T) is a center of contraction of TT. By the uniqueness principle of contractible types, it suffices to define a function f:STf:S \to T at π 1(p S)\pi_1(p_S). We define it as f(π 1(p S))π 1(p T)f(\pi_1(p_S)) \coloneqq \pi_1(p_T). Now, all that’s left is to prove that the fiber of ff at all elements a:Ta:T is contractible. But by the uniqueness principle of contractible types, it suffices to prove it for the center of contraction π 1(p T)\pi_1(p_T). The canonical element ** is in the fiber of ff at π 1(p T)\pi_1(p_T), and since π 1(p S)\pi_1(p_S) is the center of contraction of SS, the fiber of ff at π 1(p T)\pi_1(p_T) is contractible, and thus the fiber of ff at every element a:Ta:T is contractible. Thus, ff is an equivalence of types between the contractible types SS and TT.

Lemma

The positive and negative unit types are equivalent to each other.

Proof

Since the negative unit type is contractible by definition, and the positive unit type is contractible, they are equivalent to each other.

Extensionality principle

Then we could derive the extensionality principle for the unit type:

Lemma

Given elements x:𝟙x:\mathbb{1} and y:𝟙y:\mathbb{1}, there is an equivalence of types (x= 𝟙y)𝟙(x =_\mathbb{1} y) \simeq \mathbb{1} between the identity type x= 𝟙yx =_\mathbb{1} y and 𝟙\mathbb{1} itself.

Proof

Since every identity type x= 𝟙yx =_\mathbb{1} y is contractible for elements x:𝟙x:\mathbb{1} and y:𝟙y:\mathbb{1}, and 𝟙\mathbb{1} itself is contractible, this implies that every identity type x= 𝟙yx =_\mathbb{1} y is equivalent to 𝟙\mathbb{1}.

The unit type as a univalent universe

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 00 and 11 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:𝟙El 𝟙(x)typex:\mathbb{1} \vdash \mathrm{El}_\mathbb{1}(x) \; \mathrm{type} by defining

El 𝟙(*)𝟙\mathrm{El}_\mathbb{1}(*) \coloneqq \mathbb{1}

The extensionality principle for the unit type then is simply the univalence axiom:

ext 𝟙: x:𝟙 y:𝟙(x= 𝟙y)(El 𝟙(x)El 𝟙(y))\mathrm{ext}_\mathbb{1}:\prod_{x:\mathbb{1}} \prod_{y:\mathbb{1}} (x =_\mathbb{1} y) \simeq (\mathrm{El}_\mathbb{1}(x) \simeq \mathrm{El}_\mathbb{1}(y))

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 El 𝟙(x)\mathrm{El}_\mathbb{1}(x) and El 𝟙(y)\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= 𝟙yx =_\mathbb{1} y for any x:𝟙x:\mathbb{1} and y:𝟙y:\mathbb{1}. Thus the univalence axiom for 𝟙\mathbb{1} is true.

In addition, given any type AA, functions into the unit type A𝟙A \to \mathbb{1} are families of contractible types. The universe (𝟙,El 𝟙)(\mathbb{1}, \mathrm{El}_\mathbb{1}) is also closed under dependent sum types, as for any family of contractible types p:B𝟙p:B \to \mathbb{1},

( x:𝟙El 𝟙(B(x)))𝟙\left(\sum_{x:\mathbb{1}} \mathrm{El}_\mathbb{1}(B(x))\right) \simeq \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𝟙p:B \to \mathbb{1},

( x:𝟙B(x))𝟙\left(\prod_{x:\mathbb{1}} B(x)\right) \simeq \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

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

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.

Categorical semantics

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

References

On the unit type as an inductive type satisfying singleton induction:

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)-truncatedcontractible-if-inhabited(-1)-groupoid/​truth value(0,1)-sheaf/​idealmere proposition/​h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/​setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/​groupoid(2,1)-sheaf/​stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheaf/​2-stackh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheaf/​3-stackh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoid(n+1,1)-sheaf/​n-stackh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/​∞-stackh-\infty-groupoid

Last revised on October 22, 2023 at 03:42:33. See the history of this page for a list of all contributions to it.