Definition pair_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 (pr1 ff) × disp_left_adjoint_equivalence f (pr2 ff) → disp_left_adjoint_equivalence f ff. Proof. intros H. use tpair. - use tpair ; repeat split. + exact (disp_left_adjoint_right_adjoint f (pr1 H)). + exact (disp_left_adjoint_right_adjoint f (pr2 H)). + exact (disp_left_adjoint_unit f (pr1 H)). + exact (disp_left_adjoint_unit f (pr2 H)). + exact (disp_left_adjoint_counit f (pr1 H)). + exact (disp_left_adjoint_counit f (pr2 H)). - refine ((_ ,, _) ,, (_ ,, _)) ; cbn. + refine (total2_paths2 (disp_internal_triangle1 _ (pr1 H)) (disp_internal_triangle1 _ (pr2 H)) @ _). refine (!(transportb_dirprod (f ==> f) (λ α, _ ==>[α] _) (λ α, _ ==>[α] _) (_ ,, (_ ,, _)) (_ ,, (_ ,, _)) _ )). * exact (transportb (λ z, _ ==>[z] _) (internal_triangle1 f) (disp_id2 _)). * exact (transportb (λ z, _ ==>[z] _) (internal_triangle1 f) (disp_id2 _)). + refine (total2_paths2 (disp_internal_triangle2 _ (pr1 H)) (disp_internal_triangle2 _ (pr2 H)) @ _). refine (!(transportb_dirprod (_ ==> _) (λ α, _ ==>[α] _) (λ α, _ ==>[α] _) (_ ,, (_ ,, _)) (_ ,, (_ ,, _)) _ )). * exact (transportb (λ z, _ ==>[z] _) (internal_triangle2 f) (disp_id2 _)). * exact (transportb (λ z, _ ==>[z] _) (internal_triangle2 f) (disp_id2 _)). + apply (pair_is_disp_invertible_2cell (_ ,, pr1 (pr2 (pr2 (pr2 f))))). split. * apply (pr1 H). * apply (pr2 H). + cbn. apply (pair_is_disp_invertible_2cell (left_adjoint_counit (pr1 (pr2 f)) ,, pr2 (pr2 (pr2 (pr2 f))))). split. * apply (pr1 H). * apply (pr2 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.