Proposition preserves_dependent_products_comp_cartesian (C₁ C₂ C₃ : full_comp_cat) (P₁ : comp_cat_dependent_prod C₁) (P₂ : comp_cat_dependent_prod C₂) (P₃ : comp_cat_dependent_prod C₃) (F : full_comp_cat_functor C₁ C₂) (G : full_comp_cat_functor C₂ C₃) (HF : preserves_comp_cat_dependent_prod F P₁ P₂) (HG : preserves_comp_cat_dependent_prod G P₂ P₃) : preserves_comp_cat_dependent_prod (F · G) P₁ P₃. Proof. intros Γ A B. refine (is_z_isomorphism_path _ _). - refine (!(right_beck_chevalley_nat_trans_comp (cartesian_comp_cat_type_functor F) (cartesian_comp_cat_type_functor G) (π A) B _ _ _) @ _). + use (dep_prod_comp_cat_iso P₂). * exact (comp_cat_type_functor F Γ A). * exact (full_comp_cat_functor_z_iso F A). * exact (comprehension_nat_trans_mor_comm (comp_cat_functor_comprehension F) Γ A). + 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_composite _ _) _ _ _). - use is_z_isomorphism_comp. + use functor_on_is_z_isomorphism. apply HF. + exact (preserves_comp_cat_dependent_prod_iso _ _ _ HG (comp_cat_type_functor F Γ A) _ _ _ _ _). 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.