Jason (jcreed) wrote,
Jason
jcreed

-

Interesting.
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.
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