apg_typeside t apg_instance G1 : s1 apg_instance G2 : s2 apg_instance G : s3 apg_morphism h : G1 -> G apg_morphism h' : G2 -> G ---------------------------------- apg_morphism (<h | h'>) : <G1 + G2> -> GCase analysis morphism in the category of APGs.