Definition id_is_biequivalence (B : bicat) : is_biequivalence (id_psfunctor B). Proof. use make_is_biequivalence_from_unit_counit. - exact (id_psfunctor B). - use tpair. + apply lunitor_pstrans. + apply lunitor_pstrans. - apply linvunitor_pstrans. - apply linvunitor_pstrans. - apply lunitor_linvunitor_pstrans. - apply linvunitor_lunitor_pstrans. - apply lunitor_linvunitor_pstrans. - apply linvunitor_lunitor_pstrans. 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.