# What does it mean for an isomorphism to exist in the internal logic of a (quasi-)topos

When are two types isomorphic in the internal logic of a (quasi-)topos and what implications does this have for terms definable internally?

For instance, consider the topos of directed graphs, where the terminal $$1$$ is the graph with one vertex and a loop, and the graph $$P_2$$ is defined to be the graph with two nodes $$\\{0, 1\\}$$, and two edges: $$\\{0 \rightarrow 1, 1 \rightarrow 0\\}$$.

Then it would seem that $$P_2$$ and $$2 = 1 + 1$$, are isomorphic in the internal logic. In the easiest way, note that in the context of $$P_2$$, that is in the slice category $$Gph/P_2$$ we have an explicit isomorphism between $$P_2 \times P_2$$ and $$2 \times P_2$$ respecting the projection to $$P_2$$. Alternatively, we can work explicitly with the objects $$2^{P_2}$$ and $$P_2^2$$ without exorbitant pain, but I haven't checked everything.

In either case, it seems we have "$$P_2$$-many" isomorphisms between $$2$$ and $$P_2$$, which has no global points reflecting the lack of external isomorphism between these, but is internally inhabited since the unique map to $$1$$ is epic. So it would suffice to prove the internal notion of existence. This seems similar to the more intuitive case of $$G-Sets$$, such as sets with involutions, but it surprises me nonetheless.

Is this logic correct? If so, what does it imply about statements in the internal logic, can we add terms which would be able to distinguish these? Or would said terms not respect isomorphism? For instance, a connected components functor for instance, seems to violate this since it would send $$P_2$$ to $$1$$ but $$2$$ to $$2$$, and those are definitely distinct.

Yes, it can happen that in a topos you have non-isomorphic objects $$X$$ and $$Y$$ such that, for some inhabited $$T$$, $$T \times X$$ and $$T \times Y$$ are isomorphic over $$T$$. To give a geometric example, consider the topos of sheaves on the circle: then let $$X$$ be the trivial line bundle, let $$Y$$ be the Möbius strip, and let $$Z$$ be another Möbius strip. (In some sense, your example is a combinatorial version of this.) Geometrically speaking, "internally" means "locally", and $$X$$ and $$Y$$ are certainly locally isomorphic.
Thus, as you surmise, the connected components functor cannot be "internal". Strictly speaking this is a category error because an ordinary functor is not enough to determine an "internal" functor, and the usual way of inducing an "internal" functor from an ordinary functor requires the preservation of pullbacks. Given a category $$\mathcal{S}$$ with pullbacks, an "internal" endofunctor on $$\mathcal{S}$$ is an endofunctor $$F$$ on the arrow category of $$\mathcal{S}$$ that preserves pullback squares, in the sense that given a pullback square in $$\mathcal{S}$$ of the form below, $$\require{AMScd} \begin{CD} X_0 @>{f_0}>> Y_0 \\ @V{X_*}VV @VV{Y_*}V \\ X_1 @>>{f_1}> Y_1 \end{CD}$$ then $$\begin{CD} F (X)_0 @>{F (f)_0}>> F (Y)_0 \\ @V{F (X)_*}VV @VV{F (Y)_*}V \\ F (X)_1 @>>{F (f)_1}> F (Y)_1 \end{CD}$$ is also a pullback square in $$\mathcal{S}$$, and furthermore $$F (f)_1 : F (X)_1 \to F (Y)_1$$ is (strictly equal to) $$f_1 : X_1 \to Y_1$$. This means $$F$$ restricts to an endofunctor on each slice of $$\mathcal{S}$$, and these endofunctors "commute with pullbacks". You could try to define a slicewise connected components functor, but the incompatibility with pullback is what makes it not "internalisable".
• In fact, in algebraic geometry, with some conditions you can say $H^1(X, \mathscr{F})$ is equivalent to the isomorphism classes of $\mathscr{F}$-torsors, which are exactly the $\mathscr{F}$-sets which are locally isomorphic to $\mathscr{F}$. So in a sense, $H^1(X, \mathscr{F})$ studies the difference between local (internal) isomorphism and global isomorphism of $\mathscr{F}$-sets. Dec 1, 2022 at 23:00