Lemma counit_is_split_monic_if_right_adjoint_is_full : full G -> ∏ x, is_merely_split_monic (ε x). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. 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.Epis. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.SplitMonicsAndEpis. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Section HomSetIsoRightFromPartial. End HomSetIsoRightFromPartial. Section HomSetIsoLeftFromPartial. End HomSetIsoLeftFromPartial.