definitional equality for 2-logic

It is convenient, in stating the type rules and working in the type system, to have a notion of equality for objects of categories. For instance, we would like to say that from objects $x:A$ and $y:B$ we can construct a pair $\u27e8x,y\u27e9:A\times B$ such that ${\pi}_{1}(\u27e8x,y\u27e9)$ and ${\pi}_{2}(\u27e8x,y\u27e9)$ are *equal* to $x$ and $y$ respectively. Even if, in some desired 2-categorical models, they are only canonically isomorphic, carrying around all those canonical isomorphisms in the type theory is exceptionally tedious.

It turns out to cause no problems if we have a notion of equality for objects of categories, as long as that notion of equality is not a *proposition* but rather a separate kind of *syntactic* or *definitional* judgment about terms. This distinction is well-known in intensional type theory. We will write $\equiv $ for this *definitional equality* and reserve $=$ for *propositional equality*. Note that propositional equality applies only to terms of a $\mathrm{Set}$ type, while definitional equality applies, a priori, to terms of any type. However, any two terms of a $\mathrm{Prop}$ type are necessarily equal, and for terms of a $\mathrm{Set}$ type we can expect propositional and definitional equality to agree; thus definitional equality is really only a new thing for terms of a $\mathrm{Cat}$ type.

One important distinction between definitional and propositional equality is that definitional equality can never be a *hypothesis*, i.e. it can never appear on the left of a $\u22a2$. It should be viewed more as a “computation rule” defining the behavior of certain term-forming operations.

However, because we have types dependent on terms, we also need to allow definitional equality *between* types. That is, if $B(x)$ is a type dependent on $x$ and $x\equiv y$, then we should have $B(x)\equiv B(y)$. Again, this is not a problem as long as such equality of types is not a *proposition* but merely a syntactic/definitional statement.

Revised on May 29, 2012 22:04:00
by Andrew Stacey?
(129.241.15.200)