Definition make_is_biequivalence : is_biequivalence F. Proof. refine (G,, _). refine ((ηinv,, ε),, _). split. - apply equiv_to_isadjequiv. + use tpair. * use tpair. ** exact η. ** split. *** exact (pr1 pη). *** exact (pr1 qη). * split. ** apply pη. ** apply qη. - apply equiv_to_isadjequiv. + use tpair. * use tpair. ** exact εinv. ** split. *** exact (pr1 pε). *** exact (pr1 qε). * split. ** apply pε. ** apply qε. 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.