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.
