Proposition is_directed_nat {X : hSet} (PX : PartialOrder X) (D : ℕ → X) (HD : ∏ (i j : ℕ), i ≤ j → PX (D i) (D j)) : is_directed PX D. Proof. split. - exact (hinhpr 0). - intros i₁ i₂. assert (p := istotalnatleh i₁ i₂). revert p. use factor_through_squash. { apply propproperty. } intro p. apply hinhpr. induction p as [ p | p ]. + refine (i₂ ,, HD _ _ _ ,, HD _ _ _). * exact p. * apply isreflnatleh. + refine (i₁ ,, HD _ _ _ ,, HD _ _ _). * apply isreflnatleh. * exact p. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.