proposition: Lemma φ_adj_inv_after_φ_adj {A : C} {B : D} (f : F A --> B) : φ_adj_inv (φ_adj f) = f.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Epis UniMath.CategoryTheory.SplitMonicsAndEpis UniMath.CategoryTheory.Monics UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering