Definition make_dependent_product_of_mor_poset {Γ₁ Γ₂ : C} (s : Γ₁ --> Γ₂) : dependent_product HD s. Proof. use left_adjoint_from_partial. - exact (all _ _ s). - exact (all_e _ _ s). - intros ψ χ p. use iscontraprop1. + abstract (use invproofirrelevance ; intros ζ₁ ζ₂ ; use subtypePath ; [ intro ; apply homset_property | ] ; apply HD'). + simple refine (_ ,, _) ; [ | apply HD' ]. apply all_i. exact p. Defined.
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.