Lemma are_adjoints_closed_under_iso_laws {A B : category} (F G : functor A B) (H : functor B A) (αiso : @z_iso [A,B] F G) (HF : are_adjoints F H) : form_adjunction' (are_adjoints_closed_under_iso_data F G H αiso HF). Proof. set (α := pr1 αiso : nat_trans F G). set (αinv := inv_from_z_iso αiso : nat_trans G F). destruct HF as [[α' β'] [HF1 HF2]]; simpl in HF1, HF2. split. - unfold triangle_1_statement. simpl; intro a; rewrite assoc, functor_comp. etrans; [ apply cancel_postcomposition; rewrite <- assoc; apply maponpaths, (nat_trans_ax αinv)|]. etrans; [ rewrite assoc, <- !assoc; apply maponpaths, maponpaths, (nat_trans_ax β')|]. simpl; rewrite assoc. etrans; [ apply cancel_postcomposition, (nat_trans_ax αinv)|]. rewrite assoc. etrans; [ apply cancel_postcomposition; rewrite <- assoc; apply maponpaths, HF1|]. now rewrite id_right; apply (nat_trans_eq_pointwise (z_iso_after_z_iso_inv αiso)). - unfold triangle_2_statement in *. simpl; intro b; rewrite functor_comp, assoc. etrans; [ apply cancel_postcomposition; rewrite <- assoc; eapply maponpaths, pathsinv0, functor_comp|]. etrans; [ apply cancel_postcomposition, maponpaths, maponpaths, (nat_trans_eq_pointwise (z_iso_inv_after_z_iso αiso))|]. cbn. rewrite (functor_id H), id_right. apply (HF2 b). 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.