The most obvious intuition comes from the notion of well pointed categories. A well pointed category is simply a category $\cal C$ in which the final object $1$ exists and is a generator for $\cal C$. This means that for every $f,g:A \rightarrow B$,
$$ f = g \ \Leftrightarrow \forall p:1\rightarrow A, f\circ p = g\circ p$$
Note that $\circ$ is composition and not application! In haskell you would define:
f `comp` g = \x -> f (g x)
In programmatic notation the definition of well-pointedness gives
f == g iff for all p : () -> A, f `comp` p == g `comp` p
or unfolding the definitions
f == g iff for all p : () -> A, \x:() -> f (p x) == \x:() -> g (p x)
if we assume that the only inhabitant of () is in fact () (which is not the case in haskell, btw), then we get
f == g iff for all p : () -> A, \_ -> f (p ()) == \_ -> g (p ())
assuming extentionality (functions are equal if they are equal on all arguments)
f == g iff for all p, f (p ()) == g (p ())
Now the crucial observation, is that in "reasonable" categories, like $\mathrm{Set}$, morphisms $1\rightarrow A$ can be identified with elements of $A$ which gives
f == g iff for all x : A, f x == g x
which is obviously true in $\mathrm{Set}$ (this is exactly extentionality). Now note that "elements of an object of $\cal C$" doesn't even make sense in a general category, where objects are just "things" that can have morphisms into or out of them.
So the notion of well-pointedness says 2 things:
- It's reasonable to treat morphisms $1\rightarrow A$ as "elements" of the object $A$
- Extensionality holds.
It's reasonable to generalize this notion by replacing the terminal object $1$ by some arbitrary object $K$.
Now it might be useful to see a category where this doesn't hold (i.e. a category that is not well-pointed) just to see where this intuition can fail.
The simplest example I know of is the category of groups and group morphisms $\mathrm{Grp}$. Here the terminal (and initial) object $1$ is the group $\{e\}$ with a single element $e$, which is the unit for that group, and the operation $e*e=e$.
Because group morphisms must send $e$ to $e_G$ (the unit of $G$), there is always exactly 1 morphism $1\rightarrow G$ for any group $G$, namely, $\phi(e)=e_G$.
But now take any 2 distinct morphisms $f,g:\mathbb{Z}\rightarrow \mathbb{Z}$, for example $f(n) = n$ and $g(n) = 2\cdot n$.
It's not true that $f = g$ iff $\forall p : 1\rightarrow \mathbb{Z}, f\circ p = g\circ p$. Indeed there is only one $p$, namely $\phi$ from above, and $f\circ \phi(e) = g\circ \phi(e) = e_{\mathbb{Z}} = 0$. But $f \neq g$!
So $\mathrm{Grp}$ is not well-pointed, and it's not useful to treat morphisms $1\rightarrow G$ as points of $G$. However, in this case, there happens to be a generating object $K\neq 1$, so the generalization is useful after all! I'll leave it as an exercise to figure out what $K$ is...
I'll try to answer the questions more directly.
A morphism can be thought of as a a mapping from one type to another?
Sort of. It's a good intuition, but you shouldn't think that it always makes sense to talk about elements of type $A$, unless you're working in a well-pointed category as explained above..
Morphism f is equivalent to morphism g if and only if for the morphism type K to type A
It's equal rather than equivalent (though computer scientists tend to define equality in a much stricter sense than category theorists, e.g. by syntactic equality).
Also, it's "if and only if for every morphism from K to A", in general you can have many morphisms in K -> A
e applied to f is equivalent to e applied to g
Composition (written $\circ$) is not application! I've tried to break it down above.
The number of steps in this definition blows my mind, can anyone help me visualize the entire definition?
Category theory often offers very abstract definitions, and it's useful to work through examples and basic lemmas yourself to gain intuition.
However, if this helps, in the $\mathrm{Hask}$ category with types as objects and total programs of type A -> B as morphisms between A and B, the unit type () is a generator, as I tried to explain above.
