This means that bundled types are *not* visible to the Iris logic itself!

show that products preserve pcmType of the RA order, and that pcmType is trivial for discrete metrics

now that preoType already covers compatibility with a setoid, pcmType does not have to do that anymore

move the things that are only needed for the category-theoretic part (including bundled types) to CatBasics.v