Lemma form_adjunction_inv : form_adjunction _ F (nat_z_iso_inv εiso) (nat_z_iso_inv ηiso). Proof. split. - intro b. refine (_ @ triangle_id_right_ad (pr2 (pr1 adEquivF)) b). apply (pre_comp_with_z_iso_is_inj' (f:=#G (nat_z_iso_to_pointwise_z_iso εiso b))); [apply (functor_on_is_z_isomorphism G), z_iso_is_z_isomorphism |]. unfold adjunit; unfold adjcounit. unfold pr2, pr1. rewrite assoc. rewrite <- functor_comp. unfold left_functor; unfold pr1. rewrite nat_z_iso_inv_after_nat_z_iso. rewrite functor_id. rewrite id_left. rewrite assoc. use (pre_comp_with_z_iso_is_inj' (f:=(nat_z_iso_to_pointwise_z_iso ηiso (G b)))); [apply z_iso_is_z_isomorphism; rewrite z_iso_inv_after_z_iso|]. rewrite (nat_z_iso_inv_after_nat_z_iso ηiso). refine (!triangle_id_right_ad (pr2 (pr1 adEquivF)) _ @ _). refine (!id_left _ @ _). repeat rewrite assoc. do 2 rewrite <- assoc. apply (maponpaths (fun f => f · _)). apply (!triangle_id_right_ad (pr2 (pr1 adEquivF)) _). - intro a. refine (_ @ triangle_id_left_ad (pr2 (pr1 adEquivF)) a). apply (pre_comp_with_z_iso_is_inj' (f:=nat_z_iso_to_pointwise_z_iso εiso (F a))); [apply z_iso_is_z_isomorphism; rewrite z_iso_inv_after_z_iso|]. rewrite assoc. rewrite (nat_z_iso_inv_after_nat_z_iso εiso). rewrite id_left. apply (pre_comp_with_z_iso_is_inj' (f:=#F (nat_z_iso_to_pointwise_z_iso ηiso a))); [apply (functor_on_is_z_isomorphism F), z_iso_is_z_isomorphism |]. unfold adjunit; unfold adjcounit. unfold right_functor. unfold pr2, pr1. refine (_ @ !assoc _ _ _). refine (!functor_comp F _ _ @ _). rewrite (nat_z_iso_inv_after_nat_z_iso ηiso). rewrite functor_id. refine (!triangle_id_left_ad (pr2 (pr1 adEquivF)) _ @ _). refine (!id_left _ @ _). repeat rewrite assoc. do 2 rewrite <- assoc. apply (maponpaths (fun f => f · _)). apply (!triangle_id_left_ad (pr2 (pr1 adEquivF)) _). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.