typeside t schema s1 : t schema s2 : t constraints c : s1 mapping m : s1 -> s2 ---------------------------------- constraints (sigma m c) : s2