Definition dependent_products_per_subobject : has_dependent_products (disp_cat_per_subobject_cleaving H). Proof. simple refine (_ ,, _). - exact (λ A B φ, dependent_product_of_per_subobject φ). - intros A₁ A₂ A₃ A₄ s₁ s₂ s₃ s₄ p Hp. use right_from_left_beck_chevalley. + apply dependent_sums_per_subobject. + apply dependent_sums_per_subobject. + apply dependent_sums_per_subobject. use is_symmetric_isPullback. exact Hp. Defined.
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.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DualBeckChevalley. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.SubobjectDispCat. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.Existential.