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 and we can construct a pair such that and are equal to and 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 for this definitional equality and reserve for propositional equality. Note that propositional equality applies only to terms of a type, while definitional equality applies, a priori, to terms of any type. However, any two terms of a type are necessarily equal, and for terms of a type we can expect propositional and definitional equality to agree; thus definitional equality is really only a new thing for terms of a 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 . 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 is a type dependent on and , then we should have . Again, this is not a problem as long as such equality of types is not a proposition but merely a syntactic/definitional statement.