apg_typeside t apg_instance G1 : s1 apg_instance G2 : s2 ---------------------------------- apg_morphism (snd G1 G2) : (G1 * G2) -> G2