proposition: Lemma Full_Implies_Full_Functor : Full → Functor.Full Incl.
proof: Proof. unfold Full; intros. construct. - exists g. destruct x, y. apply X; auto. - proper. - reflexivity. - reflexivity. - reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor