Proposition quotient_lower_set_order_on_el_comprel : iscomprelrel downward_closed_to_eqrel quotient_lower_set_order_on_el. Proof. intros x₁ x₂ y₁ y₂. use factor_through_squash. { use impred ; intro. apply hProp_set. } intros p₁. use factor_through_squash. { apply hProp_set. } intros p₂. induction p₁ as [ p₁ | p₁ ] ; induction p₂ as [ p₂ | p₂ ] ; use hPropUnivalence ; (use factor_through_squash ; [ apply propproperty | ]) ; cbn in * ; intro q ; apply hinhpr. - induction p₁, p₂. exact q. - induction p₁, p₂. exact q. - induction p₁. destruct q as [ q | q ]. + exact (inl q). + refine (inl _). exact (I_down x₁ y₁ q (pr1 p₂)). - induction p₁. induction q as [ q | q ]. + exact (inl q). + refine (inl _). exact (I_down x₁ y₂ q (pr2 p₂)). - exact (inl (pr2 p₁)). - exact (inl (pr1 p₁)). - exact (inl (pr2 p₁)). - exact (inl (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.