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.