Proposition isantisymm_quotient_lower_set_order : isantisymm quotient_lower_set_order. Proof. use setquotunivprop'. { intro x. repeat (use impred ; intro). apply setproperty. } intros x₁. use setquotunivprop'. { intro x. repeat (use impred ; intro). apply setproperty. } intros x₂. use factor_through_squash. { repeat (use impred ; intro). apply setproperty. } intro p₁. use factor_through_squash. { apply setproperty. } intro p₂. use iscompsetquotpr ; cbn in *. apply hinhpr. induction p₁ as [ p₁ | p₁ ] ; induction p₂ as [ p₂ | p₂ ]. - exact (inr (p₁ ,, p₂)). - refine (inr (p₁ ,, _)). exact (I_down x₂ x₁ p₂ p₁). - refine (inr (_ ,, _)). + exact (I_down x₁ x₂ p₁ p₂). + exact p₂. - apply inl. exact (antisymm_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.