Definition biequivalence_to_object_equivalence : ob C ≃ ob D. Proof. pose (F := psfunctor_of_biequivalence e). pose (G := inv_psfunctor_of_is_biequivalence e). pose (η := is_biequivalence_adjoint_unit (pr2 e)). pose (ε := is_biequivalence_adjoint_counit (pr2 e)). use make_weq. - exact (λ x, F x). - use isweq_iso. + exact (λ x, G x). + intro x. cbn. apply (isotoid_2_0 (pr1 HC)). use tpair. * exact (unit_of_is_biequivalence (pr2 e) x). * cbn. apply (pointwise_adjequiv (unit_of_is_biequivalence (pr2 e))). apply η. + intro y. cbn. apply (isotoid_2_0 (pr1 HD)). use tpair. * exact (counit_of_is_biequivalence (pr2 e) y). * cbn. apply (pointwise_adjequiv (counit_of_is_biequivalence (pr2 e))). apply ε. 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.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Properties.ClosedUnderInvertibles. Require Import UniMath.Bicategories.Morphisms.Properties.Composition. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Transformations.Examples.Unitality. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.Modifications.Examples.Unitality. Import PseudoFunctor.Notations. Section Builder_From_Unit_Counit. End Builder_From_Unit_Counit.