Proposition iseqrel_downward_closed_to_hrel : iseqrel downward_closed_to_hrel. Proof. refine ((_ ,, _) ,, _). - intros x₁ x₂ x₃. use factor_through_squash. { use impred ; intro. apply propproperty. } intros p₁. use factor_through_squash. { apply propproperty. } intros p₂. apply hinhpr. induction p₁ as [ p₁ | p₁ ] ; induction p₂ as [ p₂ | p₂ ] ; cbn in *. + exact (inl (p₁ @ p₂)). + induction p₁. exact (inr p₂). + induction p₂. exact (inr p₁). + exact (inr (pr1 p₁ ,, pr2 p₂)). - intros x ; cbn in *. exact (hinhpr (inl (idpath x))). - intros x₁ x₂. use factor_through_squash. { apply propproperty. } intros p. apply hinhpr. induction p as [ p | p ] ; cbn in *. + exact (inl (!p)). + exact (inr (pr2 p ,, pr1 p)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets.