|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-level 1-type/h-prop|
|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 monad||modal type theory, monad (in computer science)|
Whereas -reduction tells us how to simplify a term that involves an eliminator applied to a constructor, -reduction tells us how to simplify a term that involves a constructor applied to an eliminator.
In contrast to -reduction, whose “directionality” is universally agreed upon, the directionality of -conversion is not always the same. Sometimes one may talk about -reduction, which (usually) simplifies a constructor–eliminator pair by removing it, but we may also talk about -expansion, which (usually) makes a term more complicated by introducing a constructor–eliminator pair. Although one might expect that of course we always want to use reduction to simplify, it is possible to put bounds on -expansion, and -reduction is ill-defined for the unit type (the exception prompting ‘usually’ above).
The equivalence relation generated by -reduction/expansion is called -equivalence, and the whole collection of processes is called -conversion.
The most common example is for a function type .
In this case, the constructor of is a -expression: given a term of type containing a free variable of type , then is a term of type .
The eliminator of says that given a term of type and a term of type , we can apply to to obtain a term of type .
An -redex? (a term that can be reduced by -reduction) is then of the form – the constructor (lambda expression) applied to the eliminator (application). Eta reduction reduces such a redex to the term .
Conversely, -expansion expands any bare function term to the form . If -expansion is applied again to this, we get , but -reduction returns this to ; therefore, this last form is considered to be fully -expanded. In general, the rule when applying -expansion is to use it only when the result is not a -redex.
Although function types are the most publicized notion of -reduction, basically all types in type theory can have a form of it. For instance, in the negative presentation of a product type , the constructor is an ordered pair , while the eliminators are projections and which yield elements of or .
The -expansion rule then says that for a term , the term — the constructor applied to the eliminators — is equivalent to itself. (Again, we do not repeat the -expansion, as this would produce a -redex.) If we use -reduction instead, then we simplify any subterm of the form to (and leave anything not of that form alone).
Above we did a product type with two factors, although it's easy to generalise to any natural number of factors. The case with zero factors is known as the unit type, and -conversion behaves a bit oddly there; let us examine it.
In the negative presentation of the unit type , the constructor is an empty list , while there are no eliminators. The -expansion rule then says that any term is equivalent to the term — the constructor applied to no eliminators. In this case, if we repeat the -expansion, this does not produce a -redex (indeed, there is no -reduction for the unit type), but simply makes no change. If we try to apply -reduction to , then this is ill-defined; we could ‘simplify’ this to any term that we might be able to construct.
Eta-reduction/expansion is not as well-behaved formally as beta-reduction, and its introduction can make computational equality undecidable. For this reason and others, it is not always implemented in computer proof assistants.
Coq versions 8.3 and prior do not implement -equivalence (definitionally), but versions 8.4 and higher do implement it for dependent product types (which include function types). Even in Coq v8.4, -equivalence is not implemented for other types, such as inductive and coinductive types. This is a good thing for homotopy type theory, since -equivalence for identity types forces us into extensional type theory.
When -equivalence is not an implemented as a direct identity, it may be derived for a defined (coarser than identity) equality. For example, if is defined to mean (where is assumed to have been previously defined) and is taken to be identical to (implementing -reduction), then and are provably equal even if not identical. Thus, eta-equivalence for function types follows from function extensionality (relative to any appropriate notion of equality).
Similarly, if “equality” refers to a Martin-Löf identity type in dependent type theory, then a suitable form of -equivalence is provable for inductively defined types (with -reduction and a dependent eliminator). This includes the identity types themselves, but this form of -equivalence does not imply the identity types are extensional because the identity type itself must be incorporated in stating the equivalence. See the next section.
In dependent type theory, an important role is played by propositional -conversions which “compute to identities” along constructors. For example, consider binary products with -reduction, but not (definitional) -conversion. We say that -conversion holds propositionally if
For any we have a term , and
Similar definitions apply for any other type.
The reason this notion is important is that it is “equivalent” to the ability to extend the eliminator of non-dependent type theory to a dependent eliminator, where the type being eliminated into is dependent on the type under consideration.
For instance, in the case of the binary product, suppose that -conversion holds propositionally as above, and that we have a dependent type along with a term defined over the constructor. Then for any we can “transport” along to obtain a term defined over , yielding the dependent eliminator. The rule ensures that this dependent eliminator satisfies the appropriate -reduction rule.
Conversely, if we have a dependent eliminator, then can be defined by eliminating into the dependent type , since when is we have inhabiting this type.
Note that this “equivalence” is itself only “propositional”, however; if we go back and forth, we should not expect to get literally the same dependent eliminator or propositional term, only a propositionally-equal one.