apg_typeside t apg_instance G1 : s1 apg_instance G2 : s2 ---------------------------------- apg_morphism (inr G1 G2) : G2 -> <G1 + G2>