Definition two_out_of_three_second (HF : adj_equivalence_of_cats F) (HH : adj_equivalence_of_cats H) : adj_equivalence_of_cats G. Proof. use (nat_iso_adj_equivalence_of_cats _ _ (comp_adj_equivalence_of_cats (adj_equivalence_of_cats_inv HF) HH)). - exact (nat_trans_comp (right_adjoint HF ∙ H) (right_adjoint HF ∙ F ∙ G) G (pre_whisker (right_adjoint HF) (nat_z_iso_inv ν)) (post_whisker (counit_nat_z_iso_from_adj_equivalence_of_cats HF) G)). - use is_nat_z_iso_comp. + apply (pre_whisker_on_nat_z_iso (right_adjoint HF) (nat_z_iso_inv ν)). apply (nat_z_iso_inv ν). + apply (post_whisker_z_iso_is_z_iso (counit_nat_z_iso_from_adj_equivalence_of_cats HF) G). apply (counit_nat_z_iso_from_adj_equivalence_of_cats 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.