7
$\begingroup$

The categorical semantics of a dependent type theory is normally described as a CwA/CwF/CompCat/etc. and in these models, we can talk about propositional equality by interpreting an 'identity type'. So, what about judgmental equality?

My little analysis: I've heard people saying 'two terms are equal if they are interpreted as the same morphism (or uniquely isomorphic terms)'. This is not what I'm looking for. Take a contextual category as an example: if the base category $\cal C$ has all pullbacks and a terminal object, we can define in it the notion of equalizers, which interprets the extensional identity type. With that type, the definitional equality becomes propositional equality (is that true? I'm not sure -- please correct me if I'm wrong!). But there is certainly a difference in the type theory (where we do not always identify definitional equality and propositional ones).

So, what are definitional equalities in the categorical semantics?

$\endgroup$
1
  • $\begingroup$ To people who came across this question: both answers deserve reading, please don't just look at the accepted one. $\endgroup$
    – ice1000
    Jul 28 at 14:03
7
$\begingroup$

Definitional equality is the same as equality in the metatheory. It works exactly the same way as in 1-category theory. If I have a category $\mathbb{C}$ and some morphisms $f,g : \mathbb{C}(A, B)$, I write $f = g$ for their equality, where $=$ is a metatheoretical relation. I can assume a family structure on $\mathbb{C}$ to get a CwF, plus assume some type formers, and now I'm doing type theory, but $=$ remains the same.

In the initial model of some type theory (the syntax), $=$ is the same as convertibility, because the syntax only equates things which are provably equal from the specification. In other models, more things can be equal. For example, in the terminal model all terms are equal (and all types, contexts, morphisms).

If we have extensional equality, that specifies $\mathsf{Tm}\,\Gamma\,(\mathsf{Id}\,t\,u)$ to be naturally isomorphic to $t = u$. In that case, propositional and definitional equality are equivalent in any model. Intensional equality on the other hand is not always equivalent to $=$.

With that type, the definitional equality becomes propositional equality

If we're defining models of MLTT, if we have any model where equality reflection does hold, in that model definitional equality is equivalent to propositional equality. But we can also define models where equality reflection is false. In fact, the syntax of MLTT is such a model. MLTT gives us wiggle room, because the theory does not specify anything about equality reflection. If equality reflection is included in the specification ("signature") of the theory, we have no such freedom.

$\endgroup$
6
  • $\begingroup$ Just to confirm: since equalizers exist when the category has pullbacks, a CwF where the base category has pullbacks is such a category with equality reflection. Is that true? Does that (prove by contradiction) imply the syntax of MLTT as a CwF does not have pullbacks? $\endgroup$
    – ice1000
    Jul 28 at 11:55
  • 1
    $\begingroup$ @ice1000 Correct, the syntactic category of MLTT does not have pullbacks. $\endgroup$ Jul 28 at 12:02
  • $\begingroup$ That said, although not all parallel morphisms in the MLTT syntax have equalizers, we can decide whether there is an equalizer. The decision procedure is unification, and the equalizer is the most general unifier (mgu). $\endgroup$ Jul 28 at 12:10
  • $\begingroup$ The internal equality is a type and cannot be literally the same thing as judgemental equlity. What rather happens is that the identity type $\mathrm{Id}_A$ is interpreted as classifying equality of morphisms (which is how judgemental equality is interpreted). $\endgroup$ Jul 28 at 12:44
  • 1
    $\begingroup$ @AndrejBauer I did not mean literally the same, of course. Reworded it. $\endgroup$ Jul 28 at 12:54
4
$\begingroup$

Definitional equality is essentially a syntactic notion of equality, not witnessed by a term in the type theory: when two types or terms are definitionally equal, we are saying that they are precisely the same. Therefore, definitional equality of types is interpreted as equality of objects, and definitional equality of terms is interpreted as equality of morphisms.

This is orthogonal to the treatment of identity types. If our category has equalisers, we can interpret identity types. Furthermore, these come with equality reflection, in that having $\Gamma \vdash p : \mathrm{Id}_A(a, a')$ implies that $a$ and $a'$ are definitionally equal, and hence equal as morphisms of the category. However, we could consider weaker interpretations of identity types, such as a path space object, in which case we are able to model propositional equalities without involving definitional equalities at all. However, in this setting, definitional equality (where relevant) would still be interpreted as equality of types or morphisms.

$\endgroup$
7
  • $\begingroup$ But terms of equal interpretations in category theory are not always definitionally equal $\endgroup$
    – ice1000
    Jul 28 at 10:59
  • 1
    $\begingroup$ If your category is complete for the syntax, then the equality of two objects or morphisms in the category will imply that the corresponding types or terms are equal. However, category theorists may consider categories that are not complete for the syntax. The syntactic category in particular is always complete in this sense, and hence equality in the category exactly corresponds to definition equality. $\endgroup$
    – varkor
    Jul 28 at 11:15
  • $\begingroup$ Can I rephrase the last sentence as 'and hence equalities known in the category exactly corresponds to def equality'? $\endgroup$
    – ice1000
    Jul 28 at 11:46
  • 1
    $\begingroup$ What do you mean by "known"? A category is by definition a set of objects and morphisms, along with composition structure. So we always know whether two objects or morphisms are equal, depending on whether they are equal set-theoretically (i.e. equal elements of the set). $\endgroup$
    – varkor
    Jul 28 at 12:16
  • 1
    $\begingroup$ Both answers are great, and I have to make a choice to prevent the third to come out 🤣 I'm sorry that stackexchange only allows on answer to be accepted. What makes me accepted AK's answer is due to the comments to his post, which is not part of the answer anyway $\endgroup$
    – ice1000
    Jul 28 at 13:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.