Proposition is_left_adjoint_equivalence {C₁ C₂ C₃ C₄ : category} (HC₁ : is_univalent C₁) (HC₂ : is_univalent C₂) (HC₃ : is_univalent C₃) (HC₄ : is_univalent C₄) {F : C₁ ⟶ C₂} {G : C₃ ⟶ C₄} {E : C₁ ⟶ C₃} {E' : C₂ ⟶ C₄} (τ : nat_z_iso (E ∙ G) (F ∙ E')) (HE : adj_equivalence_of_cats E) (HE' : adj_equivalence_of_cats E') (HF : is_left_adjoint F) : is_left_adjoint G. Proof. use (is_left_adjoint_equivalence_help (C₁ := C₁ ,, HC₁) (C₂ := C₂ ,, HC₂) (C₃ := C₃ ,, HC₃) (C₄ := C₄ ,, HC₄)). - exact F. - refine (E ,, _). use equiv_cat_to_adj_equiv. exact HE. - refine (E' ,, _). use equiv_cat_to_adj_equiv. exact HE'. - use nat_z_iso_to_invertible_2cell. exact τ. - exact HF. 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.