proposition: Proposition isaprop_preserves_dependent_sums {C₁ C₂ : category} {D₁ : disp_cat C₁} {HD₁ : cleaving D₁} {D₂ : disp_cat C₂} {HD₂ : cleaving D₂} {F : C₁ ⟶ C₂} (FF : cartesian_disp_functor F D₁ D₂) (L₁ : has_dependent_sums HD₁) (L₂ : has_dependent_sums HD₂) : isaprop (preserves_dependent_sums FF L₁ L₂).
proof: Proof. do 4 (use impred ; intro). apply isaprop_is_z_isomorphism. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Pullbacks