scratch
§ Categorification of Sets Works Because It's a Presheaf on a Single Point
created 2024-10-03
- Why are sets the categorification of the naturals?
- It's because they obey the same "free theory"!
- We build sets as the presheaf of a single point, which means that we get all sets by gluing sets freely. This is similar in spirit to how we build the natural numbers with 0 and successor.
- However, because we are freely cocompleting the category, we get much more "free gluings": indeed, one for each diagram.
- This means that sets have fewer "defeqs" than nats, while preseving all the same isos.
- This is extremely useful for dependent typing, where we want to remember how we built the object, so it's a good thing! e.g.
Sum a b versus a + b: Sum a b is free!
❦