Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Universal properties vs Type construction

Alex Kreitzberg (Jul 21 2025 at 19:08):

I'm aware of computational trinitarianism as a sort of slogan. But I recently noticed a nice example of it that I'd like to understand better.

When finding the representation of the functor $F X = \boldsymbol{C}(X, A) \times \boldsymbol{C}(X, B)$, The steps in the proof enumerate the requirements we need for the construction of a pair $A\times B$ as a type in type theory.

Explicitly, a representation for $F$ needs an object $A\times B \in \boldsymbol{C}$ and an element $(\pi_1 : A\times B \rightarrow A, \pi_2 : A\times B \rightarrow B)$ defining the natural transformation:

$\alpha : \boldsymbol{C}(-, A\times B) \implies F$
$\alpha(h) = (\pi_1 \circ h, \pi_2 \circ h)$

such that there exists a natural inverse $\alpha^{-1} : F \implies \boldsymbol{C}( -, A \times B)$ satisfying the equations:

$\alpha \circ \alpha^{-1} = id$

$\alpha^{-1} \circ \alpha = id$

I'll write $\alpha^{-1}(f, g)$ as $\left<f, g\right>$, then the two equations respectively require:

$(\pi_1 \circ \left<f, g\right>, \pi_2 \circ \left<f, g\right>) = (f, g)$

and

$h = \left<h \circ \pi_1, h \circ pi_2 \right>$

These rules contain the "computation rule" or normalization procedure for the constructors and eliminators of pairs in type theory.

I find a lot of things surprising about this. The rules for products, disjoint unions and function applications in type theory, and natural deduction in particular, were chosen in part so the programs are guaranteed to terminate. So I'm surprised the yoneda lemma basically gives us this by just carefully choosing certain simple functors (like the functor of pairs of functions sharing a domain).

Is there a reason universal properties are so similar to how judgments are built in natural deduction? Is the above construction the first step in defining a category's "Internal language" (whatever that is)? What's the right way to think about this analogy?

Mike Shulman (Jul 22 2025 at 05:09):

I would say rather the rules are chosen so that programs don't get stuck. That is, an elim applied to an intro can always be reduced. Actual termination is a much subtler "global" property of the whole system, while this is a "local" one to each type former. And the local property is precisely whal Yoneda is about: you can give a map into X if you can say what its composites should be with all maps out of X, i.e. if you can guarantee that it won't cause programs to get stuck on X.

Alex Kreitzberg (Jul 22 2025 at 22:28):

Your explanation is intuitive, so I'm trying to use it to infer something else.

My interpretation of it, is having a natural transformation between represented homsets, means our computation doesn't get stuck on one of the representating objects.

Let's say we're thinking about $A \times B$

If we keep our map natural in $A$ and $B$ as well, then the natural transformation isomorphism

$\text{hom}(-, A\times B) \cong \text{hom}(-, B)$
Corresponds to $\pi_1 : A\times B \rightarrow B$.

Therfore any arrow through $A\times B$ to $B$ can be simplified to an arrow straight to $B$. So implicit in this is some reduction $\pi_2(f,g) = g$, because the point is we assumed our composition would go through no matter where we ended up.

I guess naturality buys us just a bit more than "it never gets stuck", it also never gets stuck for the same reasons.

The above was still looser than I'd like, but I think I'm getting the idea.

Any feedback on how I explored that?

Mike Shulman (Jul 22 2025 at 22:41):

Alex Kreitzberg said:

I guess naturality buys us just a bit more than "it never gets stuck", it also never gets stuck for the same reasons.

Yes, I agree. Which is what you need, really, to be able to give a uniform proof of normalization.

My only other comment is that $\pi_1$ induces only a natural transformation, not a natural isomorphism.

Alex Kreitzberg (Jul 22 2025 at 22:42):

Thank you!