[ refactor ] Relation.Unary.Closure.Base. #2864
Description
... 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 #2840 (comment)
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.