Definition adjequiv_in_E₂ (x y : E₂) : adjoint_equivalence (E₂_to_E₁ x) (E₂_to_E₁ y) → adjoint_equivalence x y. Proof. intros l. use equiv_to_adjequiv. - exact (mor_E₁_to_E₂ l). - use tpair. + use tpair. * exact (mor_E₁_to_E₂ (left_adjoint_right_adjoint l)). * split. ** exact (cell_E₁_to_E₂ (left_adjoint_unit l)). ** exact (cell_E₁_to_E₂ (left_adjoint_counit l)). + split. * exact (cell_E₁_to_E₂_is_invertible _ (left_equivalence_unit_iso l)). * exact (cell_E₁_to_E₂_is_invertible _ (left_equivalence_counit_iso l)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.