C : Type u₁
inst✝ : Category C
J : C
⊢ Functor.PreservesEpimorphisms (coyoneda.obj J.op.op) ↔ Functor.PreservesEpimorphisms (yoneda.obj J)
C : Type u₁
inst✝ : Category C
J : C
⊢ Injective J ↔ Functor.PreservesEpimorphisms (yoneda.obj J)
rw [injective_iff_projective_op, Projective.projective_iff_preservesEpimorphisms_coyoneda_obj]
no goals
C : Type u₁
inst✝ : Category C
J : C
⊢ Functor.PreservesEpimorphisms (coyoneda.obj J.op.op) ↔ Functor.PreservesEpimorphisms (yoneda.obj J)
exact Functor.preservesEpimorphisms.iso_iff (Coyoneda.objOpOp _)