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