Functoriality and product-preservation of reflective subuniverses

Rather than commenting this, do we want to define the above as an `IsEquiv` about precomposing with this function?