Try making the associated Ok constraint depend on the object/type parameter as well as the category, and eliminate classes introduced to accommodate the current single-parameter dependency. See Make the Obj' type family depend on object as well as category.
conal
commented
3 years ago
Try making the associated
Okconstraint depend on the object/type parameter as well as the category, and eliminate classes introduced to accommodate the current single-parameter dependency. See Make theObj'type family depend on object as well as category.