Lemma is_epi_post_whisker_right_adjoint_counit_pointwise : ∏ x, isEpi (nat_trans_data_from_nat_trans Gε x). Proof. intro x. assert (is0 : isEpi (nat_trans_data_from_nat_trans (ηG · Gε) x)). { rewrite (maponpaths nat_trans_data_from_nat_trans triangle_eq_r). apply identity_isEpi. } apply (isEpi_precomp _ _ _ is0). 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.