David Corfield coercion

How to say ‘No cat is a dog’.

Luo adopts a ‘type for each common noun’ approach, while Bekki uses more subtypes. In the latter approach you might have taken a basic type to be $Animal$, and then have $Cat$ as $\sum _{x: Animal} Feline(x)$. Then you can easily have $x: Animal \vdash Feline(x) \to \neg Canine(x)$. But then you might think why not just have a single type Entity and use predicates all the time. Bekki suggests some fine-graining, which might restrict you from saying, e.g., ‘No cat is a rock’, if you ever wanted that.

But there is another approach. In the strictest ‘intrinsic’ typing approach, an element just comes typed, so there’s not a question of whether it belongs to another type. However, when I get acquainted with the type $Cat$, I learn there’s a canonical map, say $i$, to the type $Animal$, sending the cat to its ‘underlying’ animal. Similarly for $Dog$ and say $j$. Then no cat is a dog could be represented by $x: Cat, y: Dog \vdash \neg Id_{Animal}(i(x), j(y))$.

Maybe alternatively there’s a map $Animal \to Species$. But then the functional nature forces `no cat is a dog'.

In the context of mathematics, when using e.g. Lean, they’ll do something like this, calling it coercion.

A common worry you hear on presenting type theory for mathematics is that it’s forcing you to distinguish the $2$ of $\mathbb{N}, \mathbb{Z},\mathbb{Q},\mathbb{R},\mathbb{C}$ etc. But isn’t this really just happening because N is the initial rig/semifield, also explained by N being the free monoid on one generator, hence picking up a multiplication for free. We don’t get shocked that we have to specify the group that an identity element belongs to, even though with $\{e\}$ the free group, it’s going to appear in all groups.

What else could this happen for? Named entity in sphere spectrum?