proposition: Proposition istrans_quotient_lower_set_order : istrans quotient_lower_set_order.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets