Jason (jcreed) wrote,


Flight back to Madison.
Got my car back --- there was a slight issue
getting it out of the storage locker, since
some ice had frozer over the little metal tabs
that needed to be lifted up, but dad chopped it
away with a jack.
Mad, mad twelf hacking. Made a bunch of progress
proving some lemmas about producting arrows
and I have an implementation of the definition
of pullbacks that looks like it may be viable.
We'll see, though.
I have the proof that {*}_A is monic right up
to the point where the pullback property is
necessary. I've yet to prove that the 'obvious'
cell is a pullback, but I have gotten that
it commutes. Also need to formulate that subobject
classifiers are pullbacks, somehow.

Hrmm. Maybe this definition of pullback isn't what
I want after all. Maybe something more akin
to the definition of subobjects rather than
products, the latter being the way I have it
right now.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded