I spent a lot of the past year getting really into categorical logic (as in, using category theory to study logic),
because I'm really into logic, and category theory seemed to be able to provide cool alternate foundations of
mathematics.
Turns out it doesn't really.
Don't get me wrong, I still think it's interesting and useful, and it did provide me with a very cosmopolitan view of logical systems (more on that later). But category theory is not suitable for foundations or even meant to be foundational. Most category theorist use an extended version of set theory through the use of Grothendieck universes which are meant to provide a set in which all of mathematics can be performed. In fact, its purpose is best seen as exactly dual to that of foundations: while set theory allows you to build things from the ground up, category theory allows you to organize things from high above. A category by itself is not so interesting; one often studies a category in terms of how it maps from and into other categories (including itself!), with functors, and, most usefully, adjunctions.
A topos is perhaps best seen not even as a category, but as an alternate mathematical universe. They are, essentially, “weird set theories”. Case in point: $\mathbf{Set}$ itself is a topos, and other toposes are often constructed as categories of functors $F : C \to \mathbf{Set}$, for $C$ an arbitrary category.
(Functors assemble into categories if you take natural transformations between them. That basically means that you have maps $F(c) \to G(c)$, such that if you compare the images of a path under $F$ and $G$, all the little squares commute.)
Consider that natural numbers, with their usual ordering like $4 \leq 5$, can perform a category if you take instead $4 \to 5$. So one simple example is to consider the category of all functors $\mathbb{N} \to \mathbf{Set}$, which are really just sequences of sets, like
\[ X_1 \to X_2 \to X_3 \to \dots \]where the arrows are regular set theoretic functions. You can do practically any kind of mathematical reasoning using sequence of sets as long as it is constructive. Any result in ordinary mathematics whose proof is finitist and constructive automatically holds in any topos. Therefore, one can prove results in toposes and similar categories by reasoning, not about the objects and morphisms in the topos themselves, but instead about sets and functions in the normal language of structural set theory, which is more familiar to most mathematicians.
For example you have:
a bunch of empty sets and, at some position $n$, all points, meaning that we have as many truth values as natural numbers. This is our first glance into the cosmopolitan nature of topos theory; weird truth values! Notice, however, that if $n \leq m$, their corresponding subobjects will have this ordering reversed; so in the end it might have been better to use functors on $\mathbb{N}^\mathrm{op}$, natural numbers with their order reversed.
To sum up, we made the category $\mathbf{Set}^\mathbb{N}$ of sequences of sets, and realized that it was a topos with truth values $\mathbb{N}^\mathrm{op}$.
Turns out there's a big connection between toposes and topological spaces. The open sets of a topological space have the structure of a partially ordered set, if you set $U \leq V$ whenever $U \subset V$. Moreover. in that poset, you can describe $U \cap V$ as the greatest lower bound of $U$ and $V$, and $U \cup V$ as their least upper bound.
This is in fact almost exactly the structure we want of our topos-theoretic poset of truth values: the greatest lower bound corresponds to conjunction $p \land q$ and least upper bound is the disjunction $p \lor q$. So we can use topological spaces of truth values, and this is in fact the approach used in intuitionistic logic.
In classical logic, we often discuss the truth values that a formula can take. The values are usually chosen as the
members of a Boolean algebra. The meet and join operations in the Boolean algebra are identified with $\land$
and $\lor$ logical connectives, so that the value of a formula for the form $A \land B$ is the meet of the value of
$A$ and the value of $B$ in the Boolean algebra. Then we have the useful theorem that a formula is a valid
proposition of classical logic iff its value is 1 for every valuation, i.e., for any assignment of values to its
variables.
A corresponding theorem is true for intuitionistic logic, but instead of assigning each formula a value from a
Boolean algebra, one uses values from a Heyting algebra (of which Boolean algebra is a special case).
(so each open set, and not point, corresponds to a truth value; you take the $\mathsf{AND}$ of two open sets to be their intersection and the $\mathsf{OR}$ to be their union)
Alright, so as with $\mathbb{N}$, the poset of open sets can define a category if you set $U \to V$ whenever $U \leq V$. So take $X$ a topological space and $\mathcal{O}(X)$ its category of open sets. We'll define a new category $\mathbf{Sh}(X)$ of functors $\mathcal{O}(X)^\text{op} \to \mathbf{Set}$, except that they won't be all of the functors, only those that preserve the topo/logical structure (sheaves).
Guess what? Not only is $\mathbf{Sh}(X)$ a topos, but it turns out that its truth values are isomorphic to $\mathcal{O}(X)$! And since the truth values are the subobjects of the point, that means that the points of the topos are in face shaped like $X$... Now we have a fuller view of the logically cosmopolitan view that topos theory can bring us. You can create, just like that, a whole parallel mathematical universe of bizarro sets where everything is made up of, say, donuts. Or coffee cups. It is as you wish.
Since I deeply care about problems of logical induction and logical counterfactuals and whatnot, I spent a while trying to design a topos that would behave like manipulating probabilities. Or distributions. Or something. With the objective of making something that would represent beliefs.
Well, I'm sorry, but it doesn't work. At the minimum, we would expect that the truth values of this topos be probabilities, yeah? And with the cosmopolitan principle above, we could then just take the sheaves on this poset of probabilistic truth values. So these truth-values would be order-isomorphic to $[0,1]$. But for them to actually represent probabilities, we'd want that $p \land q = pq$, and yet the order on $[0,1]$ already describes that $p \land q = \mathrm{min}(p, q)$, and we are doomed from the start.
Furthermore, even in an inuitionistic logic, the provable statements all have the maximal truth values (which here would be 1); but we all know that 0 and 1 are not probabilities and so nothing should be provable... which seems like it wouldn't be very useful.
In order to legetimately use topos theory for rationality, we should have a way for the topos to “think about itself”. Analogously to the situation in Peano arithmetic, for a topos $\varepsilon$, we'd want some object $E \in \varepsilon$ (specifically, an internal category) to be isomorphic to $\varepsilon$ in some sense. We define an “element” of an object $E \in \varepsilon$ as being an arrow $* \to E$. So the objects of the internal category are given by the set $\mathrm{Hom}(*, E)$, and in fact the functor $\mathrm{Hom}(*, –) : \varepsilon \to \mathbf{Set}$ respects the structure of the internal category enough that is becomes a category internal to $\mathbf{Set}$, which is just a small category.
But wait. The toposes generated by sheaves on a topological space are at least as big as $\mathbf{Set}$, but the collection of all sets is too big to be a set, and thus we run into size issues.