2
$\begingroup$

$\DeclareMathOperator\dom{dom}$What follows is preamble to motivate the question; for users who prefer to just see the question, please scroll down to the end of the question.

One possible interpretation of the Yoneda lemma is that it is 'enough' to define things set theoretically if we want a definition of something in an arbitrary category:

Let $\mathcal{C}$ be a category, using the one hom-class definition. For each object $X\in{\bf Ob}_\mathcal{C}$, we define $\overline X$ to be the set of all arrows in $\mathcal{C}$ with codomain $X$; that is, $$\overline X = \{f\in{\bf Hom}_\mathcal{C}:\operatorname{cod}(f)=X\}.$$ For each arrow $f:X\to Y\in{\bf Hom}_\mathcal{C}$, we define a function $$f\circ:\overline X\to\overline Y$$ $$g\mapsto f\circ g.$$ More generally, we will say that a function $g:\overline X\to\overline Y$ respects domains iff $g$ commutes with the domain selection function in $\mathcal{C}$, so for all $f\in\overline X$ $$\dom(g(f))=\dom(f).$$ We will say that $g$ is precomposition linear iff for all objects $f\in\overline X$ and all objects $h\in\overline{\dom(f)}$ we have that $$g(f\circ h)=g(f)\circ h.$$ Note that postcomposition functions trivially satisfy both conditions. This is essentially just a repackaging of the data of hom-presheaves and natural transformations between them 'one dimension lower', where we encode the extra dimensional information as axioms on the collapsed data. In this case, the separation into hom-sets that hom-presheaves usually provide is taken care of by requiring functions between collections of generalized global elements to respect domains, and naturality is taken care of by precomposition linearity.

This is all ultimately justified by Yoneda, since transformations between hom-presheaves come uniquely from arrows in the underlying category. For example, consider exponential objects -- for objects $X,Y\in{\bf Ob}_\mathcal{C}$, we can define an exponential object without finite products using this method in the same way that we can using presheaves. That is, an exponential object for $X$ and $Y$ consists of an object $Z$ together with a function $$\overline\epsilon:\overline Z\times\overline Y\to \overline X$$ which respects domains and is precomposition linear such that for any other object $A$ together with a function $$\overline f:\overline A\times\overline Y\to\overline X$$ which respects domains and is precomposition linear, there exists a unique function $$\overline{\tilde{f}}:\overline A\to\overline Z$$ which respects domains and is precomposition linear such that

commutes in ${\bf Set}$.

In the previous version of this post, I mentioned an 'interpretation of the language of set theory' provided by this approach; to make this more precise, what I mean is that for an arbitrary category $\mathcal{C}$ we can define a family of generalized global membership relations $$\{\in^\mathcal{C}_X\}_{X\in{\bf Ob}_\mathcal{C}}$$ on ${\bf Hom}_\mathcal{C}\times{\bf Ob}_\mathcal{C}$ by $$f\in^\mathcal{C}_XY\iff f:X\to Y\in{\bf Hom}_\mathcal{C},$$ then take any set theoretical statement and pop a universal quantifier outside of it quantifying over all objects in a category to interpret that statement inside the category in a way that reproduces the construction the formula defines in the category of sets. For example, for two sets $A$ and $B$ and a set $C$ together with functions $\pi_A:C\to A$ and $\pi_B:C\to B$ the following formula encodes the information that $C$ is a product of $A$ and $B$: $$a\in A\wedge b\in B\iff\exists! c\in C\big(\pi_A(c)=a\wedge\pi_B(c)=b\big).$$ Now, working inside an arbitrary category $\mathcal{C}$, we interpret the above formula inside $\mathcal{C}$ by replacing all instances of sets with objects, universally quantifying over all objects of $\mathcal{C}$, replacing all instances of membership with generalized global membership at objects, and interpreting functions acting on elements as postcomposition by the corresponding arrows. That is, $$\forall X\in{\bf Ob}_\mathcal{C}\Big(a\in^\mathcal{C}_X A\wedge b\in^\mathcal{C}_X B\iff\exists! c\in^\mathcal{C}_X C\big(\pi_A(c)=a\wedge\pi_B(c)=b\big)\Big),$$ where $\pi_A(c):=\pi_A\circ c$ etc.. This formula encodes the information that an object $C$ together with arrows $\pi_A:C\to A$ and $\pi_B:C\to B$ is the product object of objects $A$ and $B$, in identical fashion to how the formula pre-'interpretation' encoded the information that one set together with functions was the product of two other sets.

The motivation for doing this is that sets, functions, respect for domains, precomposition linearity, or language interpretation are all concepts that someone familiar with logic/set theory but not $1$-category theory could easily grasp with some short explanation as soon as we define a category for them, while an explanation of presheaves and natural transformations would require more categorical machinery in place before it became clearer than the explanation above. This process 'collapses the algebra' under consideration by one dimension in a certain sense; instead of having to consider commutative diagrams in a category ($1$-dimensional algebra) to prove things, I can work with functions acting on elements ($0$-dimensional algebra) with the extra dimensional information encoded in axioms we impose on the functions.

Now, stepping things up a dimension, I believe that one possible interpretation of $2$-Yoneda should be that it is 'enough' to define things category theoretically if we want a definition of something in an arbitrary $2$-category. I have a few pages of notes exploring this approach and it seems to work (with bigger axioms imposed to collapse the algebra), but I'm curious if this approach has been written up anywhere; my goal is really just to get comfortable enough with $2$-category theory to use it for other purposes, but I hope that an 'interpretation' of the language of categories inside an arbitrary $2$-category similar to the above 'interpretation' of the language of set theory inside an arbitrary category might allow someone like me (comfortable with $1$-category theory but not $2$-category theory) to process what's going one more easily in a $2$-D setting, in similar fashion to how the above interpretation helps me understand things more clearly in dimension $1$. Any pointers are appreciated.

Note: This post has been almost entirely reworked since initially being posted, thanks to users who pointed out that I was using terminology incorrectly. All comments below were addressed at the original version of this post.

$\endgroup$
13
  • 1
    $\begingroup$ Like varkor, I'm also feeling internal resistance to how you're using "internal language", and maybe even more resistance to "interpretation of the language of ZF". which is single-sorted with a single binary predicate $\in$. But it sounds like maybe you want embedding/completeness theorems in the 2-categorical context. So for example, in the 1-categorical context, to prove a general statement about finite limits, it suffices to prove it for Set, since we have the Yoneda embedding which is fully faithful and left exact, to do the remaining work. $\endgroup$ Commented Apr 6 at 22:05
  • $\begingroup$ @ToddTrimble I don’t mean to appropriate any language incorrectly; I’ll remove the question until I can find the correct way to phrase it. $\endgroup$
    – Alec Rhea
    Commented Apr 7 at 0:43
  • $\begingroup$ I was going to say that maybe "completeness theorems" or "embedding theorems" (for statements in 2-category theory) might be useful buzzphrases. But now I don't know whether you'll see this comment -- you deleted too quickly for me to insert this comment in time. $\endgroup$ Commented Apr 7 at 0:46
  • $\begingroup$ I agree that "interpretation of the language of ZF" seems slightly off here, certainly if you are dealing with an arbitrary category. Without at least finite products you can't say much at all. This is a matter of the expressiveness of the logic, as well. The internal language of a regular category allows use of the regular fragment of FOL, less than the background full FOL assumed for ZF. $\endgroup$
    – David Roberts
    Commented Apr 7 at 7:48
  • $\begingroup$ @ToddTrimble I did see it for future reference, and thank you. $\endgroup$
    – Alec Rhea
    Commented Apr 24 at 20:46

0

You must log in to answer this question.