Notes from a Medium-Sized Island [entries|archive|friends|userinfo]

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

- [Mar. 28th, 2001|02:41 pm]
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.