Jason (jcreed) wrote,
Jason
jcreed

-

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.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments