[ add ] `Setoid`/`IsEquivalence` bundle/structure of propositions modulo bi-implication

[jamesmckinna]

This issue is derived from the OP of #2070 .

Given the 'bare' preorder of sets (propositions) under implication _→_, we can now add the structure/bundle using the constructions in Relation.Binary.Construct.Interior.Symmetric added in #2071 , so we should... somewhere.

[jamesmckinna]

oops... I meant this to be free-standing, rather a sub-issue (a feature we haven't made use of to date in stdlib, and this doesn't seem the place to start ;-))