agda
[ refactor ] `Relation.Unary.Closure.Base.`
... for all that I do know or remember, I still forget that
Relation.Unary.Closure.Base.{box|diamond}, when specialised to the relation R given by the graph of f (understood propositionally, and/or setoidally) give us the constructions we want (please check!), together with variations on curry/uncurry to define the various adjunctions should/might give you what you want?
The fine print needs checking though!
in particular, we need to generalise from Rel to REL...
Originally posted by @jamesmckinna in https://github.com/agda/agda-stdlib/issues/2840#issuecomment-3436130597
Namely: to generalise from R : Rel A _ to R : REL A B _, and chase through the knock-on consequences.
Possibly in the first instance as a new Construct module, and instantiate Closure in terms of it.
I had already created that tag (where you'd tagged me on the original version of this issue about discoverability).
