Proposition isaprop_preserves_dependent_products {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₂) (R₁ : has_dependent_products HD₁) (R₂ : has_dependent_products HD₂) : isaprop (preserves_dependent_products FF R₁ R₂). Proof. do 4 (use impred ; intro). apply isaprop_is_z_isomorphism. Qed.
Require Import UniMath.Foundations.All. 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.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Pullbacks.