Proposition quotient_poset_hrel_comp : iscomprelrel eqX quotient_poset_hrel_on_el. Proof. intros x₁ x₂ y₁ y₂ p q. assert (p' := pr1 (H x₁ x₂) p). revert p'. use factor_through_squash. { apply hPropset. } intros p'. assert (q' := pr1 (H y₁ y₂) q). revert q'. use factor_through_squash. { apply hPropset. } intros q'. induction p' as [ p' | p' ] ; induction q' as [ q' | q' ] ; use hPropUnivalence ; (use factor_through_squash ; [ apply propproperty | ]) ; cbn in * ; intro r ; apply hinhpr. - induction p', q'. exact r. - induction p', q'. exact r. - induction p'. induction r as [ r | r ]. + exact (inl r). + refine (inl _). exact (I_down x₁ y₁ r (pr1 q')). - induction p'. induction r as [ r | r ]. + exact (inl r). + refine (inl _). exact (I_down x₁ y₂ r (pr2 q')). - 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.