Definition depfunction_poset {X : UU} (Y : X → hSet) (RY : ∏ (x : X), PartialOrder (Y x)) : PartialOrder (forall_hSet Y). Proof. use make_PartialOrder. - exact (λ f g, ∀ (x : X), RY x (f x) (g x)). - repeat split. + abstract (intros f g h p q x ; exact (trans_PartialOrder (RY x) (p x) (q x))). + abstract (intros f x ; exact (refl_PartialOrder (RY x) (f x))). + abstract (intros f g p q ; use funextsec ; intro x ; exact (antisymm_PartialOrder (RY x) (p x) (q x))). Defined.
Require Import UniMath.MoreFoundations.All.