# An equational way to prove associativity of least upper bounds

Traditionally, to prove the associativity of the least upper bounds, i.e. $x \vee (y \vee z) = (x \vee y) \vee z$ we need few lines to prove the inequality from the left hand side and conversely. However, by turning the definition of finit join to the adjunction form, we have a more compact and algebraic-like way to do it. Continue reading

# Yoneda argument – Application

A simple application of Yoneda argument is to prove that $a^1 \cong a$ in Cartesian closed category.

Lemma. In Cartesian closed category, $a^1 \cong a$ where $1$ is terminal.

Proof. $hom(b, a) \cong hom(b \times 1, a) \cong hom(b, a^1)$ for all objects $b$. Hene $a \cong a^1$.

It’s also quite easy to see that $a^{b \times c} \cong (a^b)^c$ since $hom(d, a^{b \times c}) \cong hom(d \times b \times c, a) \cong hom(d \times c, a^b) \cong hom(d, (a^b)^c)$.  Hence $a^{b \times c} \cong (a^b)^c$. It’s just like that we prvoe the equality $c \wedge b \rightarrow a = c \rightarrow (b \rightarrow a)$ in the Heyting algebra!

# Yoneda argument

I don’t want to repeat the Yoneda lemma, but one of the important corollary should be emphasized. Roughly speaking, given any object $c$ in the category $\mathcal{C}$, $c$ is determined by its morphisms up to isomorphism. That is, the natural isomorphism between hom-sets corresponds to the isomorphism between objects, i.e. $hom(-, c) \cong hom(-, d) \Leftrightarrow c \cong d$. How do we prove it? Well, let’s see a simpler analogy in partial orders.

Lemma. $\uparrow x = \uparrow y$ if and only if $x = y$.
Proof. If $\uparrow x = \uparrow y$, then $a \in \uparrow b$ and $b \in \uparrow a$ which imply $a \leq b$ and $b \leq a$. Hence $a = b$. The converse is quite trivial.

First, we can prove it by brute force method.

Lemma. $hom( - , c ) \cong hom( - , d )$ if and only if $c \cong d$.
Proof. Consider the following diagrams,



by replacing $f$ with $\phi^{-1}_{d}(id_{d})$, we will see that $id_{d} = \phi_{c}(id_c) \circ \phi^{-1}_{d}(id_{d})$ and we will have the other isomorphism by replacing $f$ with $\phi_{c}(id_c)$ and reversing the arrows.

However, the diagram above is exactly used in Yoneda lemma, and of course we can use Yoneda lemma to prove it.

First recall that Yoneda lemma states that $Nat ( hom ( - , r ), K ) \cong Kr$ where $K$ is a Set-valued functor and $r$ is an object in a locally small category $\mathcal{C}$. Let $K$ be the hom-set functor $hom(-, s)$. It gives the isomorphism between $Nat(hom(-, r), hom(-, s)) \cong hom(r, s)$. Hence, it indeed tells you that $Y(d) = hom(-, d)$ is fully faithful. Therefore, we have the second proof.

Proof2. Given that $Y$ is fully faithful, thus the natural isomorphisms $Y ( d ) \cong Y ( c )$ actually correspond to the isomorphism $d \cong c$ and vice verse. That’s it!

# a x 1 \cong a

A quick note: $A \times 1 \cong A$ where $1$ is the terminal object.

Consider the following diagram,



we have $id_a = \pi_1 \circ \langle id_a, ! \rangle$ already, and we attempt to find whether $\langle id_a, ! \rangle \circ \pi_1$ is equal to $id_{a \times a}$. However, $\langle id_a, ! \rangle \circ \pi_1 = \langle id_a \circ \pi_1, ! \circ \pi_1 \rangle$ where

.

Since $1$ is a terminal object, the morphism $a \times a \rightarrow 1$ is unique. So, $! \circ \pi_1 = \pi_2$ and therefore $\langle id_a \circ \pi_1, ! \circ \pi_1 \rangle = \langle \pi_1, \pi_2 \rangle$ which is the identity of $a \times 1$.

To see that $\langle \pi_1, \pi_2 \rangle$ is the identity, we just draw the following diagram,



where $id_{a \times b}$ also makes the diagram commute. Since $\langle \pi_1, \pi_2 \rangle$ is unique, it must be as same as $id_{a \times b}$.

Also, to see $\langle f, g \rangle \circ h = \langle f \circ h, g \circ h\rangle$ we just draw the following diagram,



where $\langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle$ by the similar argument.

# Exponential Notation

Let’s enjoy some familiar concepts in sets and be happy with the exponential notation of function space.

Normally, a function from set X to set Y is represented as $f:X \rightarrow Y$. Sometimes, people say that it is the exponential object in the category of Set, but what does it mean? Is it similar to the exponentiation of numbers, e.g. $2^3$?

Indeed, yes.

We can view the disjoint union and intersection as addition and multiplication respectively. For example, we have

$\displaystyle{ (\mathbf{2} \rightarrow A) \cong A \times A}$

where $\mathbf{2}$ denotes the two-pointed set. In face, the isomorphism is given by $f \mapsto (f(0), f(1))$ and $(x, y) \mapsto g$ where $g(0) = x$ and $g(1) = y$. In general, it means that

$\displaystyle{(B \rightarrow A) \cong \underbrace{A \times A \times \dots \times A}_{| B |}}$.

Using exponential notation, it reads that $A^{B} \cong \prod_{i = 1}^{|B|} A$. It satisfies familiar equalities we learned, e.g.

1. $A^B \times A^C \cong A^{B + C}$.
2. $(A^{B})^{C} \cong A^{B \times C}$.
3. $A^{0} \cong 1$ where $0$ is the empty set and $1$ is the one-pointed set.
4. $0^{A} \cong 0$ for any non-empty set $A$.

With this notation, we can drop the subset notation $\subseteq$ since $S \subseteq X$ is equivalent to $S \in \mathbf{2}^{X}$ where $S$ becomes the characteristic function on $S$. That is,

$\chi_{S}(x) = 1$ if $x \in S$ or $\chi_{S}(x) = 0$ otherwise.

Moreover, the belonging relation $\in$ can be viewed as a function from one-pointed set to $X$, e.g. $(* \rightarrow A) \equiv A^{*}$. Note that $x \in X$ is a proposition in set theory but a function $x : * \rightarrow A$ is a proposition in the meta-language.

Looking at the above discussion more carefully, we may suspect whether we can talk about set theory purely in terms of objects, morphisms, hom-set and so on. Well, indeed! Basically it is called topos theory and maybe I can say something about topos theory after I fully understand it …