<p>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 <span class="math-container">$\mathbb{C}$</span> and some morphisms <span class="math-container">$f,g : \mathbb{C}(A, B)$</span>, I write <span class="math-container">$f = g$</span> for their equality, where <span class="math-container">$=$</span> is a metatheoretical relation. I can assume a family structure on <span class="math-container">$\mathbb{C}$</span> to get a CwF, plus assume some type formers, and now I'm doing type theory, but <span class="math-container">$=$</span> remains the same.</p>
<p>In the initial model of some type theory (the syntax), <span class="math-container">$=$</span> is the same as convertibility, because the syntax <em>only</em> 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).</p>
<p>If we have extensional equality, that specifies <span class="math-container">$\mathsf{Tm}\,\Gamma\,(\mathsf{Id}\,t\,u)$</span> to be naturally isomorphic to <span class="math-container">$t = u$</span>. In that case, propositional and definitional equality are equivalent in any model. Intensional equality on the other hand is not always equivalent to <span class="math-container">$=$</span>.</p>
<blockquote>
<p>With that type, the definitional equality becomes propositional
equality</p>
</blockquote>
<p>If we're defining models of MLTT, if we have any model where equality reflection does hold, <em>in that model</em> definitional equality is equivalent to propositional equality. But we can also define models where equality reflection is <em>false</em>. 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 (&quot;signature&quot;) of the theory, we have no such freedom.</p>

CC BY-SA 4.0
2021-07-28T11:55:39.017Z
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?
ice1000
CC BY-SA 4.0
2021-07-28T12:02:15.963Z
@ice1000 Correct, the syntactic category of MLTT does not have pullbacks.
András Kovács
CC BY-SA 4.0
2021-07-28T12:10:01.587Z
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).
András Kovács
CC BY-SA 4.0
2021-07-28T12:44:31.760Z
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).
Andrej Bauer
CC BY-SA 4.0
2021-07-28T12:54:49.493Z
@AndrejBauer I did not mean literally the same, of course. Reworded it.
András Kovács
CC BY-SA 4.0
2021-08-06T07:35:22.473Z
(correction: unification is semidecision procedure for MLTT)
András Kovács
CC BY-SA 4.0
2021-07-28T11:40:32.900Z
2021-07-28T12:53:53.523Z
2021-07-28T12:53:53.523Z
András Kovács
<p>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.</p>
<p>This is orthogonal to the treatment of identity types. If our category has equalisers, we can interpret identity types. Furthermore, these come with <em>equality reflection</em>, in that having <span class="math-container">$\Gamma \vdash p : \mathrm{Id}_A(a, a')$</span> implies that <span class="math-container">$a$</span> and <span class="math-container">$a'$</span> are definitionally equal, and hence equal as morphisms of the category. However, we could consider weaker interpretations of identity types, such as a <a href="https://ncatlab.org/nlab/show/path+space+object" rel="nofollow noreferrer">path space object</a>, 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.</p>

CC BY-SA 4.0
2021-07-28T10:59:03.457Z
But terms of equal interpretations in category theory are not always definitionally equal
ice1000
CC BY-SA 4.0
2021-07-28T11:15:08.567Z
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](https://ncatlab.org/nlab/show/syntactic+category) in particular is always complete in this sense, and hence equality in the category exactly corresponds to definition equality.
varkor
CC BY-SA 4.0
2021-07-28T11:46:39.570Z
Can I rephrase the last sentence as 'and hence equalities _known_ in the category exactly corresponds to def equality'?
ice1000
CC BY-SA 4.0
2021-07-28T12:16:36.070Z
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).
varkor
CC BY-SA 4.0
2021-07-28T13:48:13.463Z
@ice1000: I would be interested to know what András Kovács's answer clarified that mine did not, so that I might understand what point was confusing you.
varkor
CC BY-SA 4.0
2021-07-28T13:59:45.777Z
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
ice1000
CC BY-SA 4.0
2021-07-28T14:02:36.490Z
Basically, my first comment was just wrong, and I hoped you could point out directly
ice1000
CC BY-SA 4.0
2021-07-28T10:24:39.393Z
2021-07-28T10:24:39.393Z
varkor
<p>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?</p>
<p>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 <em>not</em> what I'm looking for. Take a contextual category as an example: if the base category <span class="math-container">$\cal C$</span> 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 <em>becomes</em> 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).</p>
<p>So, what are definitional equalities in the categorical semantics?</p>

CC BY-SA 4.0
2021-07-28T14:03:58.917Z
To people who came across this question: both answers deserve reading, please don't just look at the accepted one.
ice1000
<type-theory><dependent-type><semantics>
What's the categorical semantics of definitional equality?
ice1000
# What's the categorical semantics of definitional equality?

(Asked by: username_0 on 2021-07-28)

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?

**Tags:** type-theory, dependent-type, semantics

> **Comments:**
> **username_0**: To people who came across this question: both answers deserve reading, please don't just look at the accepted one.  

---

## 2 answers

### Answer by username_1 on 2021-07-28. Score: 8 | Accepted answer

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.

> **Comments:**
> **username_0**: 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?  
> **username_1**: @username_0 Correct, the syntactic category of MLTT does not have pullbacks.  
> **username_1**: 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).  
> **username_2**: 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).  
> **username_1**: @AndrejBauer I did not mean literally the same, of course. Reworded it.  
> **username_1**: (correction: unification is semidecision procedure for MLTT)  

---

### Answer by username_3 on 2021-07-28. Score: 4

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](https://ncatlab.org/nlab/show/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.

> **Comments:**
> **username_0**: But terms of equal interpretations in category theory are not always definitionally equal  
> **username_3**: 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](https://ncatlab.org/nlab/show/syntactic+category) in particular is always complete in this sense, and hence equality in the category exactly corresponds to definition equality.  
> **username_0**: Can I rephrase the last sentence as 'and hence equalities _known_ in the category exactly corresponds to def equality'?  
> **username_3**: 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).  
> **username_3**: @username_0: I would be interested to know what username_1's answer clarified that mine did not, so that I might understand what point was confusing you.  
> **username_0**: 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  
> **username_0**: Basically, my first comment was just wrong, and I hoped you could point out directly  

---

