Lemma is_monic_post_whisker_left_adjoint_unit_pointwise : ∏ x, isMonic (nat_trans_data_from_nat_trans Fη x). Proof. intro x. assert (is0 : isMonic (nat_trans_data_from_nat_trans (Fη · εF) x)). { rewrite (maponpaths nat_trans_data_from_nat_trans triangle_eq_l). apply identity_isMonic. } apply (isMonic_postcomp _ _ _ 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.