feat(category_theory): equivalences preserve epis and monos (#6994)

Note that these don't follow from the results in `limits/constructions/epi_mono.lean`, since the results in that file are less universe polymorphic.

src/category_theory/epi_mono.lean

@@ -40,6 +40,14 @@ begin
     cancel_mono, equiv.apply_eq_iff_eq] at H
 end
 
+instance is_equivalence.epi_map {F : C ⥤ D} [is_left_adjoint F] {X Y : C} {f : X ⟶ Y}
+  [h : epi f] : epi (F.map f) :=
+left_adjoint_preserves_epi (adjunction.of_left_adjoint F) h
+
+instance is_equivalence.mono_map {F : C ⥤ D} [is_right_adjoint F] {X Y : C} {f : X ⟶ Y}
+  [h : mono f] : mono (F.map f) :=
+right_adjoint_preserves_mono (adjunction.of_right_adjoint F) h
+
 lemma faithful_reflects_epi (F : C ⥤ D) [faithful F] {X Y : C} {f : X ⟶ Y}
   (hf : epi (F.map f)) : epi f :=
 ⟨λ Z g h H, F.map_injective $