for C being carrier-underlaid category
for a being Object of C holds the_carrier_of a = the carrier of (a as_1-sorted)