apg_typeside ty apg_instance G : T apg_mapping F : S -> T ---------------------------------- apg_instance (delta F G) : S