Definition Directed_hsubtype (P : Poset) : UU := ∑ A : hsubtype P, isdirected (pr1carrier A). Coercion pr1_Directed_hsubtype {P} : Directed_hsubtype P -> hsubtype P := pr1. Coercion Directed_of_Directed_hsubtype (P : Poset) : Directed_hsubtype P -> Directed_family P. Proof. intros C. exact (carrier C,, (pr1carrier C,, pr2 C)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo. Require Import UniMath.OrderTheory.Posets.Subposets.