Proposition id_preserves_comp_cat_dependent_prod (C : full_comp_cat) (P : comp_cat_dependent_prod C) (F := id₁ C : full_comp_cat_functor C C) : preserves_comp_cat_dependent_prod (id₁ C) P P. Proof. intros Γ A B. refine (is_z_isomorphism_path _ _). - refine (!(id_preserves_comp_cat_dependent_prod_lem _ _ _ B) @ _). refine (maponpaths (λ z, right_beck_chevalley_nat_trans _ _ z _) _). exact (fiber_functor_natural_nat_z_iso_eq (cleaving_of_types C) (cleaving_of_types C) (disp_functor_identity _) _ _ (π A)). - apply z_iso_is_z_isomorphism. 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.