Definition pr2_left_adjoint_equivalence {a b : C} (f : adjoint_equivalence a b) {aa : disp_dirprod_bicat a} {bb : disp_dirprod_bicat b} (ff : aa -->[ f] bb) : disp_left_adjoint_equivalence f ff → disp_left_adjoint_equivalence f (pr2 ff). Proof. intros H. use tpair. - use tpair ; repeat split. + exact (pr2 (disp_left_adjoint_right_adjoint f H)). + exact (pr2 (disp_left_adjoint_unit f H)). + exact (pr2 (disp_left_adjoint_counit f H)). - refine ((_ ,, _) ,, (_ ,, _)) ; cbn. + refine (maponpaths dirprod_pr2 (pr1(pr1(pr2 H))) @ _). refine (maponpaths dirprod_pr2 ((transportb_dirprod (f ==> f) (λ α, _ ==>[α] _) (λ α, _ ==>[α] _) (_ ,, (_ ,, _)) (_ ,, (_ ,, _)) (internal_triangle1 f) ))). * exact (transportb (λ z, _ ==>[z] _) (internal_triangle1 f) (disp_id2 _)). * exact (transportb (λ z, _ ==>[z] _) (internal_triangle1 f) (disp_id2 _)). + refine (maponpaths dirprod_pr2 (pr2(pr1(pr2 H))) @ _). refine (maponpaths dirprod_pr2 ((transportb_dirprod (_ ==> _) (λ α, _ ==>[α] _) (λ α, _ ==>[α] _) (_ ,, (_ ,, _)) (_ ,, (_ ,, _)) _ ))). * exact (transportb (λ z, _ ==>[z] _) (internal_triangle2 f) (disp_id2 _)). * exact (transportb (λ z, _ ==>[z] _) (internal_triangle2 f) (disp_id2 _)). + apply (pr2_is_disp_invertible_2cell (left_adjoint_unit f ,, pr1 (pr2 (pr2 (pr2 f)))) (disp_left_adjoint_unit (pr1 (pr2 f)) (pr1 H)) ). apply H. + apply (pr2_is_disp_invertible_2cell (left_adjoint_counit f ,, pr2 (pr2 (pr2 (pr2 f)))) (disp_left_adjoint_counit (pr1 (pr2 f)) (pr1 H)) ). apply H. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. 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.Examples.Initial. Require Import UniMath.Bicategories.Core.Examples.Final. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.