apg_typeside t apg_instance G1 : s1 apg_instance G2 : s2 apg_instance G3 : s3 apg_morphism h : G1 -> G2 apg_morphism h' : G2 -> G3 ---------------------------------- apg_morphism [h ; h'] : G1 -> G3