Lemma φ_adj_inv_after_φ_adj {A : C} {B : D} (f : F A --> B) : φ_adj_inv (φ_adj f) = f. Proof. unfold φ_adj, φ_adj_inv. rewrite functor_comp. assert (X2 := nat_trans_ax ε); simpl in *. rewrite <- assoc. rewrite X2; clear X2. rewrite assoc. intermediate_path (identity _ · f). - apply cancel_postcomposition. apply triangle_id_left_ad. - apply id_left. 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.