Definition adj_equivalence_to_left_equivalence {C₁ C₂ : univalent_category} {F : C₁ ⟶ C₂} (A : adj_equivalence_of_cats F) : @left_equivalence bicat_of_univ_cats _ _ F. Proof. simple refine ((_ ,, (_ ,, _)) ,, (_ ,, _)). - exact (adj_equivalence_inv A). - exact (pr1 (unit_nat_z_iso_from_adj_equivalence_of_cats A)). - exact (pr1 (counit_nat_z_iso_from_adj_equivalence_of_cats A)). - apply is_nat_z_iso_to_is_invertible_2cell. exact (pr2 (unit_nat_z_iso_from_adj_equivalence_of_cats A)). - apply is_nat_z_iso_to_is_invertible_2cell. exact (pr2 (counit_nat_z_iso_from_adj_equivalence_of_cats A)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Univalence.