Definition app_directed_set_depfun (E : directed_set (depfunction_poset (λ i, D i) (λ i, D i))) (i : I) : directed_set (D i). Proof. use make_directed_set. - exact E. - exact (λ e, E e i). - split. + exact (directed_set_el E). + abstract (intros e₁ e₂ ; assert (k := directed_set_top E e₁ e₂) ; revert k ; use factor_through_squash ; [ apply propproperty | ] ; intros k ; induction k as [ k [ H₁ H₂ ]] ; exact (hinhpr (k ,, (H₁ i ,, H₂ i)))). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Examples.Propositions. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO.