Anon, a young researcher, sits down with Saunders Mac Lane.
Anon: Please, explain to me in full detail, everything you know about category theory. Indicate where you are uncertain so I may better understand your epistemic state.
-- End Prompt
Saunders: It's the foundation of modern mathematics and computer science. It deals with sets of objects called categories, which can be thought of as collections of things. For example, there is a set called the natural numbers that we use for counting. There is also another set called the real numbers, which are used for computing. The idea behind it is that if two things are in one category, then they must have some relationship to each other. If two things are in two different categories, then they probably don't have any relationship to each other.
Anon: Can you describe how these objects and arrows get used in practice?
Saunders: Sure. So, each arrow in the diagram stands for a rule that allows us to go from one object to another. So, for example, if we wanted to take the natural numbers and add three to each of them, then we would start with 1, then 2, then 3, then 4. If we were to take the integers and multiply each of them by three, then we would get 1, then 3, then 6, then 9. Each of these mappings is a functor.
Anon: Got it. I think.
Saunders: If you take a look at the diagram, you'll see there are three main objects in this category: N, Z, and R. Each of these has special relationships with each other. N is linked to Z by addition, and Z is linked to R by multiplication. If you look carefully, you'll see that addition is also linked to multiplication. We call this an adjunction. It's a very special relationship.
Anon: Fascinating. I'm not sure I understand it all yet, but this is great stuff.
Saunders: Glad to hear it. So, are you ready to tackle the second theorem?
Anon: The second one? I thought there was just one.
Saunders: Oh no, this is the "Curry-Howard isomorphism," but that's a lot bigger than the first one. It says that for any computer program, you can write a logical expression that, when evaluated, produces the value true if and only if the program will eventually output "Hello, World."
Anon: That's a pretty bold claim.