1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
TrM.A = M.A : Set TrM.A is not universe polymorphic OpM.A = M.A : Set OpM.A is not universe polymorphic TrM.B = M.B : Set TrM.B is not universe polymorphic *** [ OpM.B : Set ] OpM.B is not universe polymorphic