Definition image_is_directed {P:Poset} {I:UU} (p : I -> P) : isdirected p -> isdirected (pr1carrier (image p)). Proof. intros p_directed. split. - apply (squash_to_hProp (isdirected_inhabited p_directed)). intros i; apply hinhpr. apply to_image; assumption. - use (pr1 (image_carrier_univ' p (fun x => ∀ j, ∃ k, x ≤ _ ∧ _))). intros i. use (pr1 (image_carrier_univ' p (fun y => ∃ k, _ ∧ y ≤ _))); intros j. apply (squash_to_hProp (isdirected_compatible p_directed i j)). intros [k [le_ik le_jk]]. apply hinhpr. exists (to_image _ k). split; assumption. 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.