proposition: Lemma counit_is_split_monic_if_right_adjoint_is_full : full G -> ∏ x, is_merely_split_monic (ε x).
proof: Proof. intros fullG x. set (pcw c := (@precomp_with _ _ _ (ε x) c)). cut (∏ c : D, issurjective (pcw c)); [apply is_merely_split_monic_weq_precomp_is_surjection|]. intros c. cut (issurjective (hom_weq (nathomweq_from_adj are) ∘ @precomp_with _ _ _ (ε x) c)%functions); [apply issurjective_postcomp_with_weq|]. assert (E : (hom_weq (nathomweq_from_adj are) ∘ pcw c)%functions = # G). { apply funextfun; intro z; cbn. unfold φ_adj, pcw, precomp_with. rewrite functor_comp, assoc. change ε with (counit_from_are_adjoints are). refine (_ @ id_left _). apply (maponpaths (fun f => f · _)). apply (triangle_id_right_ad are x). } cut (issurjective (@functor_on_morphisms _ _ G x c)). - intros; cbn. unfold pcw in *; cbn in E. rewrite E. assumption. - apply fullG. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Epis UniMath.CategoryTheory.SplitMonicsAndEpis UniMath.CategoryTheory.Monics UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering