Definition adjoint_equivalence_2_from_comp : adj_equivalence_of_cats (pre_comp_functor (C := D) F) := two_out_of_three_second (pre_comp_functor F') (pre_comp_functor F) (pre_comp_functor F' ∙ pre_comp_functor F) (nat_z_iso_id _) (adjoint_equivalence_1_from_comp) Hequiv.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.LeftKanExtension. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.AlgebraicTheories.FundamentalTheorem.SurjectivePrecomposition. Section AdjointEquivalenceFromComp. End AdjointEquivalenceFromComp.