Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Products can be presented purely algebraically (without explicit uniqueness conditions): see “Equational definition” in this Wikipedia page.
I expect that equalizers can also be presented purely algebraically (without explicit uniqueness conditions).
Please provide me with the explicit algebraic formulas for equalizers, if possible.
The best way to do it, would be to edit both nLab and Wikipedia wikis (and please send me the links).
I suppose you want something like this:
Given $f, g\colon A \to B$, we have an object $\{f = g\}$ (analogue of the operation $\times$) and a map $\iota_{\{f = g\}}\colon \{f = g\} \to A$ (analogue of the projection morphisms $\pi_1,\pi_2$, logically the elimination rule), satisfying $f \circ \iota_{\{f = g\}} = g \circ \iota_{\{f = g\}}$.
Given also $x\colon T \to A$ satisfying $f \circ x = g \circ x$, we also have ${x|^{\{f = g\}}}\colon T \to \{f = g\}$ (analogue of the pairing operation $\langle{-},{-}\rangle$, logically the introduction rule) and the equation $\iota_{\{f = g\}} \circ {x|^{\{f = g\}}} = x$ (the beta-rule).
Given instead $x\colon T \to \{f = g\}$, we have $f \circ (\iota_{\{f = g\}} \circ x) = g \circ (\iota_{\{f = g\}} \circ x)$ so that ${(\iota_{\{f = g\}} \circ x)|^{\{f = g\}}}\colon T \to \{f = g\}$ is defined (this line is a theorem so far), and then we have $x = {(\iota_{\{f = g\}} \circ x)|^{\{f = g\}}}$ (the eta-rule).
This may all be in Lambek & Scott (Wikipedia's reference for the equational form of the product). This all has a very type-theoretic flavour to it, and the relationship between category theory and type theory is what Lambek & Scott is all about!
1 to 2 of 2