Lemma counit_is_epi_if_right_adjoint_is_faithful : faithful G -> ∏ x, isEpi (ε x). Proof. intros faithfulG. intros x y f g H. apply (Injectivity (# G)). apply incl_injectivity. - apply faithfulG. - apply (is_epi_post_whisker_right_adjoint_counit_pointwise x). apply (maponpaths #G) in H. do 2 rewrite functor_comp in H. assumption. 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.