Functoriality and product-preservation of reflective subuniverses

Should this be `[(O; O_unit)]` rather than `([O],[O_unit])` (a sigma type rather than a pair)?