Jason (jcreed) wrote,


Took car into the shop.

Fixed the broken use of =cover=. Now I don't
use it at all, actually.

Proved assr_lr==id, finally. Also added some stuff
involving the twist arrow, and obtained the existence
of terms
app2 : mor ((B => C) * B) C
cur2 : mor (A * B) C -> mor A (B => C)
which satisfy the exact same equations from ccc.elf.

I fiddled with the higher-order stuff some more;
I actually proved that a category equivalent to the terminal
category exists - it takes like 30s to check the final declaration,
and it spits out 3 pages of type information!.
It's funny that the way I have things defined, categories
are only determined up to equivalence.
I supposed this is because of a
lack of definition of object equality.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded