Lemma preserves_comp_cat_dependent_prod_all_lemma {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₃} {H : C₃ ⟶ C₄} {K : C₂ ⟶ C₄} {HF HF' : is_left_adjoint F} {HH HH' : is_left_adjoint H} {τ : nat_z_iso (G ∙ H) (F ∙ K)} {x : C₂} (Hx : is_z_isomorphism (right_beck_chevalley_nat_trans HF HH τ x)) : is_z_isomorphism (right_beck_chevalley_nat_trans HF' HH' τ x). Proof. pose (C₁' := make_univalent_category C₁ HC₁). pose (C₂' := make_univalent_category C₂ HC₂). pose (C₃' := make_univalent_category C₃ HC₃). pose (C₄' := make_univalent_category C₄ HC₄). assert (HF = HF') as ->. { apply (@isaprop_is_left_adjoint C₁' C₂' F). } assert (HH = HH') as ->. { apply (@isaprop_is_left_adjoint C₃' C₄' H). } apply Hx. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Examples.OpMorBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.LiftDispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat. Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCat. Require Import UniMath.Bicategories.ComprehensionCat.CompCatNotations.