|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination? for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
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.
Regarded as a positive type, we give primacy to the constructors, of which there is exactly one, denoted or .
The eliminator now says that to use something of type , 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 to depend on the unit type .
We then have the β-reduction rule:
and (if we wish) the η-reduction rule:
The -reduction rule is simple. The -reduction rule says that if is an expression involving a variable of type , and we substitute for in and use that (with the eliminator) to define a term involving another term of type , then the result is the same as what we would get by substituting for in directly.
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 and 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 , 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 , by doing nothing:
There is no -reduction rule, since there are no eliminators to compose with the constructor. However, there is an -conversion rule. In general, an -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 is an “-redex”, and it “reduces” to any term of type at all:
This is obviously not a well-defined “operation”, so in this case it is better to view -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 -conversion rule for the assumed negative unit type (at least, propositionally).
Of course, the positive -reduction rule holds by definition for the above defined eliminator.
For the -conversion rules, if we start from the negative presentation and define the positive eliminator as above, then is precisely , which is convertible to by the negative -conversion rule .
Conversely, if we start from the positive presentation, then we have
where in the first conversion we use and in the second we use .
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” , while the negative product becomes “top” .
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” , while the unit object of an additional monoidal structure interprets “one” .
|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||(-1)-groupoid/truth value||mere proposition, h-proposition|
|h-level 2||0-truncated||discrete space||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||h-2-groupoid|
|h-level 5||3-truncated||homotopy 3-type||3-groupoid||h-3-groupoid|