Reed Mullanix

Some timings: the master build of agda takes [418.785 seconds](https://github.com/agda/agda/actions/runs/15653547589/job/44101780101#step:7:1165) to typecheck the standard library in CI. After these changes, we are down to [402.391 seconds](https://github.com/agda/agda/actions/runs/15765385635/job/44441241555?pr=7951#step:7:1165)!

Just tested this against a clean `1lab` build, and we save 100 seconds on my machine. Some stats: ``` -- master Total 1,315,318ms Miscellaneous 3,903ms Typing 132,030ms (796,698ms) Typing.CheckRHS 215,773ms...

After some further investigation, it does seem like Gool does have a concept of lvalues (though it calls them `VariableSym`). The problem here really lies with `LanguagePolymorphic`, which tries to...

After further investigation, I think that `LanguagePolymorphic` should probably be razed to the ground, and we should take large parts of `RenderClasses` with it. This is causing enough problems with...

This is an extension of the `Elim` problem that was mentioned before. Most of those classes are things like [InternalVarElim](https://github.com/JacquesCarette/Drasil/blob/795898c6867dfe4f6bce8db710bf9c2f59125a0d/code/drasil-gool/lib/Drasil/Shared/RendererClassesCommon.hs#L133-L135): ```haskell class InternalVarElim r where variableBind :: r (Variable r)...

What needs to be done to take this out of draft status? Working on injective objects right now, and I'd like to show that every subobject classifier is injective 🙂

Delay monads like the one in `Effect.Monad.Partiality` require some degree of countable choice to be equivalent to the partiality monad here: I think "Quotienting the delay monad by weak bisimilarity"...

Also, I forgot to mention that modulo proof-relevance, this is the free pointed DCPO, whereas delay-like monads are aiming to be the free omega-CPO.

Partial setoids move the problem of partiality to maps between partial setoids. There are a bunch of options here, and all of them are varying degrees of tricky: 1. A...

As per my comment on #2829, I think the nicest way to define upwards/downwards closed subsets is via homomorphisms into the order on `Set`, which seems to be hinted at...