<p>Semantically, a coercion $c : A \leq B$ is just a morphism $c : A \to B$, which gets added to the interpretation of terms at the appropriate points. The  basic problem this creates is the issue of <em>coherence</em>: are you guaranteed that a term will have a unique meaning, given that the same term can potentially have coercions hidden in many possible places in the program?</p>

<p>One of the first treatments of this issue was John Reynolds' 1980 paper, <a href="http://www.cs.cmu.edu/~neelk/cattheodesign.pdf"><em>Using Category Theory to Design Implicit Conversions and Generic Operators</em></a>, which shows how you can give a categorical semantics to a system of coercions and use it to ensure that it is coherent. </p>

<p>If you're interested in coercive subtyping for rich (e.g., dependent) type theories, then <a href="http://www.cs.rhul.ac.uk/~zhaohui/subtyping.html">Zhaohui Luo</a> is the go-to guy. </p>

CC BY-SA 3.0
2013-04-18T13:47:48.760Z
The John Reynolds paper looks great, thanks! (I've heard  Philip Wadler once said that John Reynolds tends to be about 10 years ahead of time in research...) I actually am familiar with Zhaohui Luo, but what I've read from him seemed to primarily be working just with type theory and not exploring the other angles.
Darius Jahandarie
CC BY-SA 3.0
2013-04-18T08:21:39.533Z
2013-04-18T08:21:39.533Z
Neel Krishnaswami
<p>Starting from Curry-Howard-Lambek, there has been a nice trinity of type theories, logics, and categories. I'm curious what categorical semantics you get when you add (coercive) subtyping to a type theory -- it seems like this has not been explored very much, if at all.</p>

<p>In general, adding coercive subtyping to a type theory does not ruin its meta-theoretic properties such as strong normalization, so its categorical semantics should be something of actual interest, I think!</p>

<lo.logic><type-theory><ct.category-theory>
What is the categorical semantics of subtyping?
Darius Jahandarie
# What is the categorical semantics of subtyping?

(Asked by: username_0 on 2013-04-17)

Starting from Curry-Howard-Lambek, there has been a nice trinity of type theories, logics, and categories. I'm curious what categorical semantics you get when you add (coercive) subtyping to a type theory -- it seems like this has not been explored very much, if at all.

In general, adding coercive subtyping to a type theory does not ruin its meta-theoretic properties such as strong normalization, so its categorical semantics should be something of actual interest, I think!

**Tags:** lo.logic, type-theory, ct.category-theory

---

## 1 answers

### Answer by username_1 on 2013-04-18. Score: 18 | Accepted answer

Semantically, a coercion $c : A \leq B$ is just a morphism $c : A \to B$, which gets added to the interpretation of terms at the appropriate points. The basic problem this creates is the issue of *coherence*: are you guaranteed that a term will have a unique meaning, given that the same term can potentially have coercions hidden in many possible places in the program?

One of the first treatments of this issue was John Reynolds' 1980 paper, [*Using Category Theory to Design Implicit Conversions and Generic Operators*](http://www.cs.cmu.edu/~neelk/cattheodesign.pdf), which shows how you can give a categorical semantics to a system of coercions and use it to ensure that it is coherent.

If you're interested in coercive subtyping for rich (e.g., dependent) type theories, then [Zhaohui Luo](http://www.cs.rhul.ac.uk/~zhaohui/subtyping.html) is the go-to guy.

> **Comments:**
> **username_0**: The John Reynolds paper looks great, thanks! (I've heard  Philip Wadler once said that John Reynolds tends to be about 10 years ahead of time in research...) I actually am familiar with Zhaohui Luo, but what I've read from him seemed to primarily be working just with type theory and not exploring the other angles.  

---

