agda
[Add] Initial files for Domain theory - Continuation of #2721
This pull request aims to continue and complete the work started in #2721
The first version already includes changes requested by @JacquesCarette, such as moving the definition of DirectedFamily to Relation.Binary.Definitions.agda and IsDirectedFamily to Relation.Binary.Structures.agda, as well as the proper bundling of Lub.
I'm going to try to have an in-person discussion (with @TOTBWF and @gabriellisboaconegero ) early next week to try to hash things out.
The main thing to discuss will be the differences in design between "in Agda in general", stdlib-style and 1lab-style. I have definitely participated in designs for stdlib that I personally consider sub-optimal but they are consistent with the rest of stdlib. Reading the many comments, this seems to be what's going on here, a clash of styles. And a non-trivial one at that, as a stdlib-coherent set of definitions may well be sub-optimal wrt what can be done in Agda in a standalone library.
