Description: The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017)