Jason (jcreed) wrote,


I can do something like
e_drop : {A : obj} mor A 1.
drop = e_drop A.
to get an explicit and implicit version of drop.
In fact did do this, which allows defining
* : obj -> obj -> obj = [A] [B] (e_drop A) # (e_drop B)
and in fact defining all the other product
constructs in terms of pullbacks.

Also, I managed to go back through the construction
of the exponential and 'explicate' enough stuff to
permit defining the operation => on objects.

The map app now has the expected type
mor (B * (B => C)) C (although ccc.elf has
it as mor ((B => C) * B) C instead...)
but cur still isn't quite right. I need to
actually prove those remaining lemmas anyway.
Okay, proved them. One required proving that
the associators are actually inverse to each
other in one direction, which was sort of nice.
Twelf seems to go -really- slow checking the
proof, though.

I realized that it was unnecessary to prove
that monics are stable under pullback -- for
some reason I thought it was important that the
pi you get by pulling name-of-true back across u
is monic, but apparently it isn't. In fact, it's
much more reasonable to show that cur and app have
the right types when I don't bother with the
morphismified subobject smor sname_true
and just use the real arrow name(true @ drop).

Back to thinking about beta eta shit again. Hmm.
Got beta and eta proven! Yay. Copied them into
mine.good. In fact showing that pi is monic
-did- come up in confirming the equalities, even
though it didn't in -constructing- the exponential.
Unfortunately the existing proof of monic stability
didn't work because
#snd (smor sname_true) um
is not the same thing as
#snd (name(true @ drop)) um
even though smor sname_true == name(true @ drop).
So I just kind of reproved it directly, and
the monstab_=#pair= was still useful.

Also have a way of defining the subobject
classifier in terms of the pullback rather than
reencoding the pullback properties in it; it
suffices to axiomatize that there are arrows going
both ways between the subobject and the pullback
object, say map and unmap (map going into the sub-
object) such that map @ unmap is the identity and
smor M @ map == #fst (char M) true, where M is
the subobject in question.

Trouble is, I found out that the proof that
sing is monic is broken, because =cover= was
defined brokenly; I left out a prime on an M.
Should fix that.

Also still need to prove assr_lr==id.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded