proposition: Theorem Functor_is_Enriched_over_Set (C D : Category) : EnrichedFunctor Sets (snd Category_is_Enriched_over_Set C) (snd Category_is_Enriched_over_Set D) ↔ (C ⟶ D).
proof: Proof. split; intros. - destruct X; simpl in *. construct. + now apply efobj0. + now apply efmap0. + proper. now apply efmap0. + now apply efmap_id0. + simpl in *. now srewrite (efmap_comp0 x y z (f, g)). - destruct X; simpl in *. construct. + now apply fobj. + construct. * now apply fmap. * proper. now apply fmap_respects. + now apply fmap_id. + simpl. symmetry. now apply fmap_comp. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Monoidal Category.Instance.Sets