Definition make_dependent_sum_of_mor_poset {Γ₁ Γ₂ : C} (s : Γ₁ --> Γ₂) : dependent_sum HD s. Proof. use right_adjoint_left_from_partial. - exact (ex _ _ s). - exact (ex_i _ _ s). - intros ψ χ p. use iscontraprop1. + abstract (use invproofirrelevance ; intros ζ₁ ζ₂ ; use subtypePath ; [ intro ; apply homset_property | ] ; apply HD'). + simple refine (_ ,, _) ; [ | apply HD' ]. apply ex_e. 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.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Pullbacks.