I'm up to the end of defining the exponential with application
and currying maps, modulo a few little lemmas. Still need
to check beta and eta reduction.
The definition of pullback is sort of redundant though;
there's one definition for the general existence of pullbacks,
and the definition is sort of re-encoded into the subobject
Working on a comic, sort of.
Mmm, wacommy goodness.