Lemma is_nat_trans_monic_from_pointwise_monics (C D : category) (F G : ob (functor_category C D)) (α : F --> G) (H : ∏ a : ob C, isMonic (pr1 α a)) : isMonic α. Proof. intros G' β η H'. use (nat_trans_eq). - apply D. - intros x. set (H'' := nat_trans_eq_pointwise H' x). cbn in H''. apply (H x) in H''. exact H''. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Subcategory.Core.