Proposition preserves_comp_cat_dependent_prod_iso_eq {C₁ C₂ : full_comp_cat} (F : full_comp_cat_functor C₁ C₂) {Γ Δ : C₁} {A : ty Γ} {s : z_iso Δ (Γ & A)} {s' : Δ --> Γ} (p : s · π A = s') : z_iso_comp (functor_on_z_iso F s) (full_comp_cat_functor_z_iso F A) · π (comp_cat_type_functor F Γ A) = #F s'. Proof. cbn. rewrite !assoc'. etrans. { apply maponpaths. apply comprehension_nat_trans_mor_comm. } rewrite <- functor_comp. apply maponpaths. exact p. 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.