Definition make_local_equivalence (Fi₁ : ∏ (x y : B₁) (f : F x --> F y), x --> y) (Finv : ∏ (x y : B₁) (f : F x --> F y), invertible_2cell (# F (Fi₁ x y f)) f) (Fi₂ : ∏ (x y : B₁) (f g : x --> y) (τ : #F f ==> #F g), f ==> g) (Fp₁ : ∏ (x y : B₁) (f g : x --> y) (τ : #F f ==> #F g), ##F (Fi₂ x y f g τ) = τ) (Fp₂ : ∏ (x y : B₁) (f g : x --> y) (τ : f ==> g), Fi₂ x y f g (##F τ) = τ) : local_equivalence. Proof. intros x y. use equiv_cat_to_adj_equiv. use rad_equivalence_of_cats. - apply univalent_category_is_univalent. - intros f g ; cbn in f, g. use isweq_iso. + exact (Fi₂ x y f g). + apply Fp₂. + apply Fp₁. - intros f ; cbn in f ; cbn. use hinhpr. simple refine (_ ,, _) ; cbn. + exact (Fi₁ x y f). + use inv2cell_to_z_iso. exact (Finv x y f). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations.