March 25th, 2001

beartato phd

-

More mad twelf hacking.
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
classifier.
Oh well.

Working on a comic, sort of.
Mmm, wacommy goodness.