David Corfield

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 AnimalAnimal, and then have CatCat as x:AnimalFeline(x)\sum _{x: Animal} Feline(x). Then you can easily have x:AnimalFeline(x)¬Canine(x)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 CatCat, I learn there’s a canonical map, say ii, to the type AnimalAnimal, sending the cat to its ‘underlying’ animal. Similarly for DogDog and say jj. Then no cat is a dog could be represented by x:Cat,y:Dog¬Id Animal(i(x),j(y))x: Cat, y: Dog \vdash \neg Id_{Animal}(i(x), j(y)).

Maybe alternatively there’s a map AnimalSpeciesAnimal \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 22 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}\{e\} the free group, it’s going to appear in all groups.

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

Last revised on November 22, 2020 at 15:25:45. See the history of this page for a list of all contributions to it.