Proposition istrans_quotient_lower_set_order : istrans quotient_lower_set_order. Proof. use setquotunivprop'. { intro x. repeat (use impred ; intro). apply propproperty. } intros x₁. use setquotunivprop'. { intro x. repeat (use impred ; intro). apply propproperty. } intros x₂. use setquotunivprop'. { intro x. repeat (use impred ; intro). apply propproperty. } intros x₃. use factor_through_squash. { repeat (use impred ; intro). apply propproperty. } intro p₁. use factor_through_squash. { repeat (use impred ; intro). apply propproperty. } intro p₂. cbn in *. apply hinhpr. induction p₁ as [ p₁ | p₁ ]. - exact (inl p₁). - induction p₂ as [ p₂ | p₂ ]. + apply inl. exact (I_down x₁ x₂ p₁ p₂). + apply inr. exact (trans_PartialOrder RX p₁ 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.