Definition comp_adj_equivalence_of_cats : adj_equivalence_of_cats (functor_composite F F'). Proof. exists (is_left_adjoint_functor_composite HF HF'). use tpair. - intro. apply is_z_isomorphism_comp. + apply (pr1 (pr2 HF)). + simpl. refine (eqweqmap (maponpaths is_z_isomorphism _) _). refine (_ @ !id_right _). exact (!id_left _). apply functor_on_is_z_isomorphism, (pr1 (pr2 HF')). - cbn. intro. apply is_z_isomorphism_comp. + refine (eqweqmap (maponpaths is_z_isomorphism _) _). refine (_ @ !id_left _). refine (_ @ !id_left _). exact (!id_right _). apply functor_on_is_z_isomorphism, (pr2 (pr2 HF)). + apply (pr2 (pr2 HF')). Defined.
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.