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

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.