apg_typeside t apg_instance G1 : s1 apg_instance G2 : s2 apg_instance G : s apg_morphism h : G -> G1 apg_morphism h' : G -> G2 ---------------------------------- apg_morphism (( h , h')) : G -> (G1 * G2)