Make U^pre and U^hcom Kan again!
Closed this issue · 3 comments
favonia commented
I was enlightened by the comments given by Andrew Pitts. I believe it also works for U^hcom.
favonia commented
How about ECOM for empty composition types?
favonia commented
I still cannot figure out the elimination rule for this type, but maybe we never need to do so? I'm going to add this type once I'm able to work on RedPRL again.