Jacques Carette

I understand this pragmatic choice. Nevertheless, I would like to see if it would be possible to have you use agda-categories in the future. I would like to at least...

Sounds great. I think my availability will be reasonable this fall term. The winter term might go a little sideways again (very heavy admin load). But I'm hoping to draft...

I don't really want to close this issue quite yet, it has too much valuable information on it. Maybe when we're done with #3067 (as an issue, not as a...

We should be able to filter out self-references easily enough. I'm going to have some real coding to do this summer!

That might be what's affecting some of the deeper modules in agda-categories. I've had to remove a number of 'helper modules' to help with type checking time. Those helpers really...

Interesting question. The current name describes the action performed on the proof term while you're proposing a name that indeed "just spells out the result". So the former describes what...

If I had to guess, I'd say that `≤-step` was named that way because of the one in equality reasoning, which is used to "take a step" in an equational...

[Catching up on backlog of things]. This looks really great - and should really help with the merge problems with `CHANGELOG`. And, with the latest changes, seems quite straightforward too.

In your "I wonder", do you mean that the rename ```agda ; x⊓y≤y to x≤y⊔x ``` should instead be ```agda ; x⊓y≤y to y≤x⊔y ``` ?

I think what @mechvel is after is what Bill Farmer and I called [high level theories](http://www.cas.mcmaster.ca/~carette/publications/hlt.pdf). Consider "Group Theory": this denotes two things, 1) the 'presentation of a Group', given...