Bundles skipped in ...Construct.StrictToNonStrict

[mechvel]

Relation.Binary.Construct.StrictToNonStrict implements "structures". But where are the corresponding "bundles" ?
For example, where decTotalOrder is implemented?
A similar question is on Relation.Binary.Construct.Add.Infimum.Strict, Nonstrict.

[MatthewDaggitt]

With the current design of the file, it's not very elegant to add functions between bundles as the modules are parameterised by the two relations. This is actually a relatively common problem in the library's Construct folders.

I personally use a different design in my own libraries where the main module StrictToNonStrict is not parameterised by anything and then I have submodules for each bundle that re-exports all the instantiated proofs for that bundle, e.g. StrictToNonStrict.PartialOrder, StrictToNonStrict.TotalOrder, ... For example see my NonStrictToStrict folder.

I have considered adding these submodules to the standard library before, but I've never got round to putting together a proposal.

[mechvel]

There are many operations that need an instance of DecTotalOrder (sorting, minimum etc.).
A programmer has DecTotalOrder for some A. He adds an infimum value to A, obtaining A'.
Then he brings to A' _<=_ induced from A by applying a function from Relation.Binary.Construct.Add.Infimum.Nonstrict. This also brings many instances for _<='.
But one also needs the DecTotalOrder instance for A', to be able, say, to apply.
And the programmer is forced to compose this instance by hand from other instances prepared in
Relation.Binary.Construct.Add.... This is not difficult for a programmer.
But I do not understand why this is not done in Relation.Binary.Construct.Add...