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: Is a universal property just a property?

Julius Hamilton (Jul 28 2024 at 22:17):

If we formalized category theory in logic, a “universal property” just seems to be a property. We can define categorical concepts like products in the usual way we extend a theory with a definition, by equating a term with a term, like so: $\forall A, B [\times(A, B) \equiv \{X | \forall Y [\exists f \in Hom(Y, A), g \in Hom(Y, B) \rightarrow (\exists h \in Hom(Y, X), \pi_1 \in Hom(X, A), \pi_2 \in Hom(X, B)) s.t. (\pi_1 \circ h \equiv f) \wedge (\pi_2 \circ h \equiv g) \wedge \exists h_2 \text{ “fulfilling the same conditions” } \rightarrow (h_2 \equiv h)]]$. Ok, maybe it’s not perfect, but you get the idea.

So, doesn’t every possible equivalence on terms in a formal theory of categories define a “universal property”, and we actually just mean “a collection of things satisfying the following property”, just like in any logical theory?

Ryan Wisnesky (Jul 28 2024 at 23:14):

To my way of thinking, universal properties are usually properties of the form, "for every x y z such that p(x,y,z), there exists a w, unique up to isomorphism, such that q(w, x, y, z)". so even though they are properties (and are true/false), when doing category theory on a computer or in detail what you often end up using is the induced assignment/function x y z -> w. In other words, universal properties can often be used like functions in addition to being true/false, which I suspect relates to the choice of name 'universal'.

Patrick Nicodemus (Aug 03 2024 at 17:38):

Julius Hamilton said:

If we formalized category theory in logic, a “universal property” just seems to be a property. We can define categorical concepts like products in the usual way we extend a theory with a definition, by equating a term with a term, like so: $\forall A, B [\times(A, B) \equiv \{X | \forall Y [\exists f \in Hom(Y, A), g \in Hom(Y, B) \rightarrow (\exists h \in Hom(Y, X), \pi_1 \in Hom(X, A), \pi_2 \in Hom(X, B)) s.t. (\pi_1 \circ h \equiv f) \wedge (\pi_2 \circ h \equiv g) \wedge \exists h_2 \text{ “fulfilling the same conditions” } \rightarrow (h_2 \equiv h)]]$. Ok, maybe it’s not perfect, but you get the idea.

Julius, there is one detail in your treatment which is missing, namely that a product can be a product in multiple different ways, and if we merely said it "Is a product" it would be erasing the different, non-equivalent ways in which it can be a product. This is fine for some purposes and not fine for other purposes.

https://en.wikipedia.org/wiki/Pairing_function
If you scroll down to "Other pairing functions" you will see that people have suggested a variety of different ways of building isomorphisms $\mathbb{N}\times\mathbb{N}\cong\mathbb{N}$, each with its own practical advantages and disadvantages. Thus, $\mathbb{N}$ is the product of $\mathbb{N}$ and $\mathbb{N}$ in multiple different ways. Without knowing _which_ way, it is impossible for us to extract the first and second components of the ordered pair.

In this case, a fix to the problem could be to say that a triple $(X, \pi_1, \pi_2)$ has the universal property of the categorical product if
$\forall Y, f : Y\to A, g : Y\to B, \exists! h : Y\to X. \pi_1\circ h = f \land \pi_2\circ h = g$
I would be perfectly fine in saying that this is an equivalent description of the universal property.

($\exists! h. P(h)$ is a common shorthand for $(\exists h. P(h)) \land \forall h_1,h_2. P(h_1)\land P(h_2)\implies h_1=h_2)$.

Josselin Poiret (Aug 22 2024 at 13:47):

Patrick summed it up pretty well here (but it's also something that bears repeating): it's almost never just an object that's the subject of a UP, but a diagram, here the triple $(X, \pi_1, \pi_2)$. This triple is actually an object of the category of "possible product-structures" on $A, B$, and being a product corresponds to being terminal in that category ("a limit is a terminal cone"). So, naively, having a product is first a choice of structure, here the triple, followed by the fact that it satisfies a property.

However, some categories can be nicer than others: a univalent category (or [[gaunt+category]]) is one in which all isomorphisms are identities. In usual set-based mathematics, they are quite rare (usually partial orders), but in HoTT, there are quite a lot: categories of algebraic gadgets always are for example. In this case, one can show that this choice of structure is actually trivial, or rather that any two choices are equal. There, "having a product" ends up being an actual property!