[DRY] what's the best way to `public`ly re-export properties/structure?

[jamesmckinna]

Cf. #2255 of which this is somehow a generalisation ...

Thanks to the sophistication of the re-exporting strategies embodied in Relation.Binary.Bundles, we could streamline concrete instances of such strategies, such as in Data.List.Binary.Relation.Equality.DecSetoid.

Compare the following (23 LOC; 3 imports; 1 explicit definition; and 2 public re-exports, the first of which also introduces the correct fixity, the second shared with the existing version):

open import Relation.Binary.Bundles using (DecSetoid)

module Data.List.Relation.Binary.Equality.DecSetoid
  {a ℓ} (DS : DecSetoid a ℓ) where

import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
open import Data.List.Relation.Binary.Pointwise using (decSetoid)

------------------------------------------------------------------------
-- Additional properties

≋-decSetoid : DecSetoid _ _
≋-decSetoid = decSetoid DS

open DecSetoid ≋-decSetoid public
  using (setoid)
  renaming (isDecEquivalence to ≋-isDecEquivalence; _≟_ to _≋?_)

------------------------------------------------------------------------
-- Make all definitions from setoid equality available

open SetoidEquality setoid public

with the existing version (31 LOC; 7 imports; 3 explicit definitions, incl. the fixity declaration; and the 1 public re-export shared with the above).

So we trade economy of expression/export for explicitness of definition... although in each case, such definitions are largely by delegation, so it's not immediately clear that there is much gain in understanding, except the documentation afforded by the types...

Which is 'better'/preferable, and which style should the library adopt from v2.* onwards?

[jamesmckinna]

Similarly, existing style seems to be to build up, definition-by-definition, towards eg Setoid instances, as in eg. Data.List.Binary.Relation.Equality.Setoid, rather than define the Setoid first, and then open it publicly and suitably renaming its components... as:

------------------------------------------------------------------------
-- Relational properties
------------------------------------------------------------------------

≋-setoid : Setoid _ _
≋-setoid = PW.setoid S

open Setoid ≋-setoid public
  using ()
  renaming (refl to ≋-refl; reflexive to ≋-reflexive; sym to ≋-sym; trans to ≋-trans; isEquivalence to ≋-isEquivalence)

[jamesmckinna]

Cf. For contrast/illustration of the status quo, my earlier comments on #2382 (and @Taneb 's recent review of #2393 ), the refinement of the above heuristic would be to emphasise re-export of bundles/structures...