Amélia

Prose for Cat.Site.Base probably sucks, @ncfavier @TOTBWF could you review?

Looks good, are there places we can use it? (Sheaves, I guess? But I'm not done writing that yet :/)

(This was fixed by #7510.)

This also happens if `MyList` is marked `abstract`. I think it's perfectly sensible: Agda doesn't track polarities in types (yet), so as far as the positivity checker is concerned, `MyList`...

Like I said, my view could be swayed! I don't think it makes much sense for the positivity checker to see through opaque definitions like this, but since we don't...

This change *was* unintended, but I think I'd file it more under "happy accident" than "mistake"... > Removing instance a : A makes it fail in 2.6.4.3 and pass in...

> Old instance search was very happy to treat i as an instance for the "class" F. And the reason for this, even though `F` is reducible (and so would...