Proposition is_left_adjoint_equivalence_help {C₁ C₂ C₃ C₄ : bicat_of_univ_cats} {F : C₁ --> C₂} {G : C₃ --> C₄} {E : adjoint_equivalence C₁ C₃} {E' : adjoint_equivalence C₂ C₄} (τ : invertible_2cell (E · G) (F · E')) (HF : is_left_adjoint F) : is_left_adjoint G. Proof. revert C₁ C₃ E C₂ C₄ E' F G τ HF. use J_2_0. { exact univalent_cat_is_univalent_2_0. } intro C₁. use J_2_0. { exact univalent_cat_is_univalent_2_0. } intro C₂. intros F G τ. assert (invertible_2cell F G) as τ'. { exact (comp_of_invertible_2cell (rinvunitor_invertible_2cell _) (comp_of_invertible_2cell (inv_of_invertible_2cell τ) (linvunitor_invertible_2cell _))). } clear τ. revert C₁ C₂ F G τ'. use J_2_1. { exact univalent_cat_is_univalent_2_1. } intros C₁ C₂ F H. exact H. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Univalence.