You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Scott Lingran (Jul 26 2020 at 15:09):Under the computational trinitarianism, "implication" within logic is isomorphic to the "internal hom" within category theory. I'm struggling to understand this.
Let's say we have a statement like "All bachelors are unmarried", which I'll rephrase as "If x is a bachelor, then x is unmarried."
If we work within Set, how would the function space between two sets be equivalent to this implication?
Also, are there any resources anyone can point to?
Thank you!
Morgan Rogers (he/him) (Jul 26 2020 at 17:49):I can answer the concrete question: a model of this situation would have a set of bachelors and a set of unmarried people, identified as subsets of all people, say. Then the implication is realised as an inclusion of the former subset in the latter. The internal hom is not in all of Set here, but in the Heyting algebra of subobjects of a given object, and in Set such an internal hom externalises to a set with exactly 0 or 1 elements.