|
| 1 | +--- |
| 2 | +title: "Products, Exponentials, and Adjoint Functors" |
| 3 | +date: 2026-04-25T12:40:59-07:00 |
| 4 | +slug: 2026-04-25-adjoint |
| 5 | +type: posts |
| 6 | +draft: false |
| 7 | +tags: |
| 8 | + - Type Theory |
| 9 | + - Category Theory |
| 10 | +--- |
| 11 | + |
| 12 | +In category theory, you often think something is a certain type of thing but |
| 13 | +actually it turns out to also be a different type of thing. In a first |
| 14 | +introduction, it appears that functors are somehow one level higher than |
| 15 | +morphisms, because functors map morphisms to morphisms. Similarly, natural |
| 16 | +transformations should be one level higher than functors because they map |
| 17 | +functors to functors. This is true if you want to be closed-minded and sad. But |
| 18 | +it ignores a beautiful thing about category theory: it is so abstract and |
| 19 | +general that it can do category theory about itself. |
| 20 | + |
| 21 | +A functor is only a morphism in the category of categories, and a natural |
| 22 | +transformation is only a morphism in a functor category. We can just keep going |
| 23 | +around and around, and nothing means anything anymore. We can also go in the |
| 24 | +opposite direction! If morphisms connect objects, are they one level higher than |
| 25 | +objects? Not at all! Certain categories contain exponentials, which are objects |
| 26 | +that somehow encapsulate the hom-set between two other objects. |
| 27 | + |
| 28 | +## Exponentials |
| 29 | + |
| 30 | +To gain a little more intuition for exponentials, consider the category |
| 31 | +$\textsf{Pos}$ of posets. For posets $A$ and $B$, the set $\textsf{Hom}(A,B)$ is |
| 32 | +the set of all monotone functions between them. Interestingly, we can define a |
| 33 | +partial ordering on these functions by comparing them pointwise. So |
| 34 | +$\textsf{Hom}(A,B)$ is a poset, which means it must be an object in |
| 35 | +$\textsf{Hom}$. This is an exponential object, which we denote $B^A$. |
| 36 | + |
| 37 | +A brief aside on notation: I think it is very confusing. It helps me to think |
| 38 | +about the category $\textsf{Set}$, where $B^A$ denotes the set of functions from |
| 39 | +$A$ to $B$. The cardinality of this set is given by $|B^A|=|B|^{|A|}$ because |
| 40 | +each function picks an element of $B$ for each element of $A$. I think that's |
| 41 | +why this notation is used, but that doesn't mean I like it. |
| 42 | + |
| 43 | +### Direct Definition |
| 44 | + |
| 45 | +Before we talk about adjunctions, let's look at a slightly more straightforward |
| 46 | +definition of an exponential. We define an exponential as $(B^A, \epsilon)$ |
| 47 | +where $B^A$ is the exponential object and $\epsilon : B^A \times A \rightarrow |
| 48 | +B$ is called the evaluation morphism. The requirement is that, for every $f : C |
| 49 | +\times A \rightarrow B$, there exists a unique morphism $\stackrel{\sim}{f} : C |
| 50 | +\rightarrow B^A$ such that the following commutes: |
| 51 | +{{< cd src="https://q.uiver.app/#q=WzAsMyxbMCwwLCJCXkEgXFx0aW1lcyBBIixbMCwwLDEwMCwxXV0sWzAsMiwiQyBcXHRpbWVzIEEiLFswLDAsMTAwLDFdXSxbMiwwLCJCIixbMCwwLDEwMCwxXV0sWzEsMCwiXFxzdGFja3JlbHtcXHNpbX17Zn1cXHRpbWVzIDFfQSIsMCx7ImNvbG91ciI6WzAsMCwxMDBdfSxbMCwwLDEwMCwxXV0sWzAsMiwiXFxlcHNpbG9uIiwwLHsiY29sb3VyIjpbMCwwLDEwMF19LFswLDAsMTAwLDFdXSxbMSwyLCJmIiwyLHsiY29sb3VyIjpbMCwwLDEwMF19LFswLDAsMTAwLDFdXV0=&embed" >}} |
| 52 | +The main thing that I think is confusing about this definition is the sudden |
| 53 | +appearance of $C$. This is a random third element that has nothing to do with |
| 54 | +the exponential of interest. The reason that we need it is because we want to |
| 55 | +deal with morphisms. If we turn a morphism $g:A\rightarrow B$ into an object, it |
| 56 | +is no longer a morphism. But by including $C$, we are able to retain the origin |
| 57 | +point of a morphism. With that in mind, we can think of $f$ as a two-argument |
| 58 | +function and $\stackrel{\sim}{f}$ in a vague sense as the curried version of |
| 59 | +that function. Then, all the diagram is saying is that we can always partially |
| 60 | +apply $f$ to its argument in $C$, bringing us to the exponential object, and |
| 61 | +then use our evaluation function to apply it to its argument in $A$. This is the |
| 62 | +same as just applying it to both arguments. |
| 63 | + |
| 64 | +### Adjoint Functors |
| 65 | + |
| 66 | +We can also think of exponentiation as the right adjoint to the cartesian |
| 67 | +product: for some fixed object $A$, $(- \times A) \dashv (-)^A$. This means that |
| 68 | +they kind of basically undo each other. Because they are adjoint functors, they |
| 69 | +must have a counit $\epsilon$, which is a natural transformation from $(-)^A |
| 70 | +\times A$ to the identity functor. In other words, given any object $B$, we can |
| 71 | +find a morphism $B^A \times A \rightarrow B$. But this is exactly the evaluation |
| 72 | +morphism at $B$. |
| 73 | + |
| 74 | +## Dependent Sum and Product Types |
| 75 | + |
| 76 | +This raises an interesting question. In dependent type theory, function types |
| 77 | +$B^A$ get lifted to product types $\Pi_{x\in A}B(x)$ and pairs $A \times B$ get |
| 78 | +lifted to sum types $\sum_{x \in A}B(x)$. When thinking of these as |
| 79 | +propositions, we can think of them as universal and existential quantification, |
| 80 | +respectively. These are duals to each other in logic. Is this duality an |
| 81 | +extension of the adjunction thing? |
| 82 | + |
| 83 | +Well, kind of. We get the relationship $\sum \dashv \iota^* \dashv \prod$. |
| 84 | +The reason we don't get a direct adjunct relationship here is because in |
| 85 | +dependent type world, these functors bind variables. In other words, their |
| 86 | +source category is not the same as their target category, so they can't be |
| 87 | +considered as opposites. |
| 88 | + |
| 89 | +The new functor $\iota^*$ is a weakening functor. Given a substitution $\iota : |
| 90 | +(\Gamma,x:A) \rightarrow \Gamma$, we get an induced map $\iota^* : |
| 91 | +\mathsf{Type}(\Gamma) \rightarrow \mathsf{Type}(\Gamma,x:A)$. We can think of |
| 92 | +this as binding another term in the context. Therefore, the adjoints have type |
| 93 | +$$ |
| 94 | +\Pi,\Sigma : \mathsf{Type}(\Gamma,x:A) \rightarrow \mathsf{Type}(\Gamma) |
| 95 | +$$ |
| 96 | +where the input is the type $B(x)$ from above, since it includes an additional |
| 97 | +binding for $x$. |
| 98 | + |
| 99 | +<!-- There's a middle man now, in the form of the base change functor. --> |
| 100 | +<!-- That is, dependent sums are the left adjoint of the base change functor and --> |
| 101 | +<!-- dependent products are the right adjoint. So first, what is a base change --> |
| 102 | +<!-- functor? --> |
| 103 | + |
| 104 | +<!-- ### Base Change Functor --> |
| 105 | + |
| 106 | +<!-- To talk about a base change functor, we need to understand what bases we're --> |
| 107 | +<!-- changing between. Sometimes, it's helpful to think about a category focalized --> |
| 108 | +<!-- over a single element. For a category $C$ and object $A \in C$, the slice --> |
| 109 | +<!-- category $C/A$ is the category whose objects are morphisms in $C$ whose target --> |
| 110 | +<!-- are $A$, and whose morphisms are composable maps between these objects. For --> |
| 111 | +<!-- example, the following commuting diagram shows two objects $f$ and $f'$ with a --> |
| 112 | +<!-- morphism $g : f \rightarrow f'$. --> |
| 113 | +<!-- {{< cd src="https://q.uiver.app/#q=WzAsMyxbMSwxLCJBIixbMCwwLDEwMCwxXV0sWzAsMCwiWCIsWzAsMCwxMDAsMV1dLFsyLDAsIlgnIixbMCwwLDEwMCwxXV0sWzEsMCwiZiIsMix7ImNvbG91ciI6WzAsMCwxMDBdfSxbMCwwLDEwMCwxXV0sWzIsMCwiZiciLDAseyJjb2xvdXIiOlswLDAsMTAwXX0sWzAsMCwxMDAsMV1dLFsxLDIsImciLDAseyJjb2xvdXIiOlswLDAsMTAwXX0sWzAsMCwxMDAsMV1dXQ==&embed" >}} --> |
| 114 | +<!-- This is called a slice category because we can think about slicing up $X$ and --> |
| 115 | +<!-- $X'$ over $A$. If $C$ were the category $\mathsf{Set}$, these slices would be --> |
| 116 | +<!-- the fibers of $f$ and $f'$ over each element of $A$. --> |
| 117 | + |
| 118 | +<!-- Now, given two slice categories $C/A$ and $C/B$, along with a morphism $f : A --> |
| 119 | +<!-- \rightarrow B$, we define the base change functor $f^* : C/B \rightarrow C/A$. --> |
| 120 | +<!-- This gives us the pullback --> |
| 121 | +<!-- {{< cd src="https://q.uiver.app/#q=WzAsNCxbMCwwLCJmXipFIixbMCwwLDEwMCwxXV0sWzEsMCwiRSIsWzAsMCwxMDAsMV1dLFswLDEsIkEiLFswLDAsMTAwLDFdXSxbMSwxLCJCIixbMCwwLDEwMCwxXV0sWzAsMiwiZl4qcCIsMCx7ImNvbG91ciI6WzAsMCwxMDBdfSxbMCwwLDEwMCwxXV0sWzEsMywicCIsMCx7ImNvbG91ciI6WzAsMCwxMDBdfSxbMCwwLDEwMCwxXV0sWzIsMywiZiIsMSx7ImNvbG91ciI6WzAsMCwxMDBdfSxbMCwwLDEwMCwxXV0sWzAsMSwiZyIsMSx7ImNvbG91ciI6WzAsMCwxMDBdfSxbMCwwLDEwMCwxXV0sWzAsMywiIiwxLHsiY29sb3VyIjpbMCwwLDEwMF0sInN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dXQ==&embed" >}} --> |
| 122 | +<!-- We won't go into all the details, but basically $f^*E$ should capture all fibers --> |
| 123 | +<!-- over $A$ that correspond to fibers over $B$. --> |
| 124 | + |
| 125 | +<!-- ### Dependent Sums --> |
| 126 | + |
| 127 | +So this adjoint-ness is kind of different. It makes sense, because the |
| 128 | +relationship between the two is clearly different. They contain more information |
| 129 | +in the form of their $B(x)$ types, so it no longer makes sense to think about |
| 130 | +them "undoing each other." They are just duals, meaning that they interact with |
| 131 | +binding in similar but opposite ways. |
| 132 | + |
| 133 | +## Sources |
| 134 | + |
| 135 | +1. [Steve Awodey's Notes on Type Theory](https://awodey.github.io/typetheory/notes/typetheory.pdf) |
| 136 | +2. [Dependent sum/product and the base-change functor adjunctions on MathOverflow](https://mathoverflow.net/questions/446516/dependent-sum-product-and-the-base-change-functor-adjunctions) |
| 137 | +3. [Andrej Bauer's Notes on Realizability](https://github.com/andrejbauer/notes-on-realizability/tree/master) |
| 138 | +4. The Dao of Functional Programming by Bartosz Milewski |
0 commit comments