What structure do natural isomorphisms preserve?

Question

My understanding from model theory is that, given groups A and B, the statement $ A \cong B $ implies that any for any first order statement $P$ in the language of groups, $P(A) \iff P(B) $.

Can an analogous statement be made for naturally isomorphic functors F and G? IE is it true that $F \cong G \implies P(F) \iff P(G)$ for some collection of propositions about functors?

I've been told that isomorphisms are the "right" notion of equivalence for algebraic structures because they "preserve structure," and I'm struggling greatly to see why natural isomorphisms are the "right" notion of equivalence of functors.

I've seen explainations like:

Set functions $X \times C \rightarrow D $ can be identified with functions $X \rightarrow D^C $. Morphisms in a category $X$ can be identified with functors $2 \rightarrow X$, so morphisms in the functor category $D^C$ should be identified with functors $2 \rightarrow D^C$. But in analogy with set functions, $2\rightarrow D^C$ 'equals' $2 \times C \rightarrow D$ from which the definition of natural transformations can be derived.

The above explanation intuitively relates to a basic property of set functions and products, but doesn't on the surface tell me about what specifically is true/preserved about isomorphic functors.

The definition of natural transformation is forced if we mandate that $Cat$ be cartesian closed, but again I fail to see the relation to preservation of 'structure.'

I've seen references to the 'principle of equivalence' which seems to support the idea that isomorphic objects should be be indistinguishable in some language.

From ncatlab:

Michael Makkai proposed the Principle of Isomorphism, “all grammatically correct properties of objects of a fixed category are to be invariant under isomorphism”

How does the definition of natural isomorphisms make this statement true in the category $D^C$ with functors as objects and morphisms as natural transformations? What's invariant? If natural transformations represent a "change in perspective" analogous to conjugation, what is preserved between the perspectives?

Can anyone give a formalization of the ideas behind the responses at https://math.stackexchange.com/questions/1077895/functorial-properties-preserved-by-natural-isomorphism?

I'm really stuck here. I feel like I'm missing something obvious.

Further reading: https://math.stackexchange.com/questions/1432782/how-different-can-equivalent-categories-be, https://math.stackexchange.com/questions/1685227/why-not-just-define-equivalence-relations-on-objects-and-morphisms-for-equivalen, and Can skeleta simplify category theory?.

Answer 1

There's a paper of Peter Freyd that addresses a similar question, not about natural isomorphism of functors but about equivalence of categories. I conjecture that what Freyd proved about equivalence may suggest similar (maybe even easier?) results about natural isomorphism. The Math Reviews data for Freyd's paper are:

MR0412249 (54 #376) Freyd, Peter Properties invariant within equivalence types of categories. Algebra, topology, and category theory (a collection of papers in honor of Samuel Eilenberg), pp. 55–61. Academic Press, New York, 1976.

Answer 2

The simplest case is that for a fixed (small) category $C$, there is a (multi-sorted) first-order theory whose models are functors $C\to \rm Set$: it has one sort for every object of $C$, and one function symbol for every morphism of $C$, plus axioms saying that these functions preserve identities and composition. So the same reasoning as in the case of groups implies that for functors $F,G:C\to \rm Set$, if $F\cong G$ then $F$ and $G$ satisfy all the same first-order statements in the language of this theory. Moreover, as pointed out in the comments, the first-order qualification is unnecessary; they satisfy all the same statements even in higher-order or infinitary logic.

To deal with functors $C\to D$ with $D\neq\rm Set$ (where $C$ and $D$ are small), we can embed them representably in the category of profunctors, i.e. functors $D^{\rm op}\times C\to \rm Set$. A functor $F:C\to D$ thus corresponds to the profunctor $\hat F(d,c) = D(d,F(c))$. This is a full embedding, so in particular two functors are isomorphic if and only if their corresponding profunctors are. Since profunctors, being set-valued functors on a small category $D^{\rm op}\times C$, are a model of a multi-sorted first-order theory as above, it follows that two isomorphic functors satisfy all the same statements in the language of this theory (even in higher-order or infinitary logic).

One may object that the language of profunctors does not include all the reasonable things one may want to say about a functor. For instance, how can we talk about "$F(c)$" for some $c\in C$? The answer is that the profunctors $H$ arising in this way are those that are representable, i.e. such that for every $c\in C$ there exists a $d\in D$ and an element $h\in H(d,c)$ such that for any $d'\in D$ and $x\in H(d',c)$ there is a unique morphism $f:d'\to d$ such that $H(f,1)(h) = x$. Representability is not a first-order axiom in this theory, but it can be expressed in infinitary logic:

$$ \bigwedge_{c\in C} \bigvee_{d\in D} \exists h\in H(d,c)\, \bigwedge_{d'\in D} \forall x\in H(d',c) \,\Big(\Big(\bigvee_{f:d'\to d} H(f,1)(h) = x\Big)\wedge \Big(\bigwedge_{g:d'\to d} (H(g,1)(h) = x) \Rightarrow (f\equiv g) \Big)\Big) $$

where $(f\equiv g)$ denotes $\top$ if in fact $f=g$ and $\bot$ otherwise. The bit of this formula after the first $\bigwedge\bigvee$ is then a characterization of when "$d=F(c)$", so that we can use infinitary logic to talk about "$F(c)$" and thereby say everything we would want to say about a functor. (To be more precise, an $h$ as in the first $\exists$ is a "witness" that $d=F(c)$ and has to be kept track of.)

Finally, so that the HoTT fans are not disappointed, let me add a bit about that perspective. In dependent type theory, the naive way to define a category is with a type $C_0:\rm Type$ of objects, a dependent type $C_1 : C_0 \times C_0 \to \rm Type$ of morphisms, and composition and identity operations satisfying axioms. Similarly, a naive functor consists of a function $F_0: C_0 \to D_0$ and a family of functions $F_1 : \prod_{c,c':C_0} C_1(c,c') \to D_1(F_0(c),F_0(c'))$ satisfying axioms.

Now, there is an interpretation of dependent type theory in which types correspond to groupoids (and, in fact, even ∞-groupoids, but that's not necessary here). The identity type "$x=_A y$", for $x,y:A$, is interpreted by the set of isomorphisms $x\cong y$ in the groupoid $A$. Since identity types in dependent type theory satisfy a strong "indiscernibility of identicals" rule, anything in the theory that is true about $x$ must then also be true about $y$.

When the naive notion of category is interpreted in this model, it gives something more general than the ordinary notion of category, but there are two ways to embed ordinary categories in such things. Given an ordinary category $C$, we could take the types $C_0$ and $C_1(c,c')$ to be the discrete groupoids corresponding to the set of objects of $C$ and the homsets of $C$. Or, we could take $C_0$ to be the underlying groupoid of $C$ consisting of all its objects and isomorphisms, and $C_1(c,c')$ as before to be the discrete groupoid corresponding to the homset. The former kind of category is called strict, the latter univalent. (There are also ways to pick out these two kinds of category inside the type theory, and a strong argument that the univalent ones are those that should be called simply "categories" for practical purposes.)

Finally, if $C$ and $D$ are univalent categories, then the functor category $D^C$ is also univalent. Thus, if $F,G:C\to D$ are ordinary functors such that $F\cong G$, and we embed $C$ and $D$ in the groupoid model of type theory as univalent categories, then $F$ and $G$ become objects of the univalent category $D^C$ that are actually equal as elements of its type of objects $(D^C)_0$, i.e. we have an inhabitant of $F=_{(D^C)_0}G$. Thus, any statement expressible in type theory that is true about $F$ must also be true about $G$. (This is arguably a fancier version of Freyd's argument for categories, which IIRC also uses dependent type theory to characterize the properties of categories that are invariant under equivalence.)