[ 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.