Jacques Carette
Jacques Carette
`PowerObject` is worse (i.e. even fewer people will find this.) Somehow (from #2351 ) `Copower` seems less bad. Current favourite remains `PointwiseLift`, though it remains a 'placeholder' in my mind...
About `Copower`: yes, of course. D'oh.
You can have one PR depend on another. There is of course a risk in that scheme.
This is against milestone Agda-2.6.5 (which doesn't exist) but Agda-2.7 is out. Is this obsolete?
I learned what displayed categories are by [reading the code](https://1lab.dev/Cat.Displayed.Base.html). The documentation is a work of art. (And has kept that style up with multiple authors.) In fact, it uses...
They certainly are related!
It almost feels like adding too many synonyms goes overboard? Doesn't pass the Fairbairn test. I'd be tempted to add these *as comments* in the code.
This is marked as 'completed' - but where is the work that corresponds to the completion?
You missed #3746 and #3747 -- aren't you looking at the recent discussions as well? There might be things on the wiki too. Those issues certainly form a good starting...
I'm not sure what you mean by the above comment? Can you expand on that please?