Definition two_out_of_three_first (HG : adj_equivalence_of_cats G) (HH : adj_equivalence_of_cats H) : adj_equivalence_of_cats F. Proof. pose (ζ := make_nat_z_iso (F ∙ functor_identity _) (F ∙ (G ∙ right_adjoint HG)) _ (pre_whisker_on_nat_z_iso F (unit_nat_z_iso_from_adj_equivalence_of_cats HG) (pr2 (unit_nat_z_iso_from_adj_equivalence_of_cats HG)))). use (nat_iso_adj_equivalence_of_cats _ _ (comp_adj_equivalence_of_cats HH (adj_equivalence_of_cats_inv HG))). - exact (nat_trans_comp (H ∙ right_adjoint HG) ((F ∙ G) ∙ right_adjoint HG) _ (post_whisker (nat_z_iso_inv ν) (right_adjoint HG)) (nat_z_iso_inv ζ)). - use is_nat_z_iso_comp. + use post_whisker_z_iso_is_z_iso. apply (nat_z_iso_inv ν). + apply (nat_z_iso_inv ζ). 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.