Definition locally_posetal_left_adj_equiv_to_z_iso {B : bicat} (HB : is_locally_posetal_bicat B) {x y : B} {f : x --> y} (Hf : left_adjoint_equivalence f) : @is_z_isomorphism (locally_posetal_bicat_to_category HB) x y f. Proof. exists (left_adjoint_right_adjoint Hf). split. + abstract (use (isotoid_2_1 (pr1 HB)) ; exact (inv_of_invertible_2cell (left_equivalence_unit_iso Hf))). + abstract (use (isotoid_2_1 (pr1 HB)) ; exact (left_equivalence_counit_iso Hf)). 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.Univalence. 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.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique.