Lemma isTotalOrder_TOSubset_plus_point {X:hSet} (S:TOSubset X) (z:X) (nSz : ¬ S z) : isTotalOrder (TOSubset_plus_point_rel S z nSz). Proof. split. { split. { split. { intros [w Ww] [x Wx] [y Wy] wx xy. apply (squash_to_hProp Wy); intros [Sy|ezy]. - induction (ishinh_irrel (ii1 Sy) Wy). apply (squash_to_hProp Ww); intros [Sw|ezw]. + induction (ishinh_irrel (ii1 Sw) Ww). apply (squash_to_hProp Wx); intros [Sx|ezx]. * induction (ishinh_irrel (ii1 Sx) Wx); change (hProptoType (TOSrel S (w,,Sw) (x,,Sx))) in wx; change (hProptoType (TOSrel S (x,,Sx) (y,,Sy))) in xy; change (hProptoType (TOSrel S (w,,Sw) (y,,Sy))). exact (TOtrans _ _ _ _ wx xy). * induction ezx; induction (ishinh_irrel (ii2 (idpath z)) Wx); change empty in xy. exact (fromempty xy). + induction ezw. induction (ishinh_irrel (ii2 (idpath z)) Ww). change hfalse. apply (squash_to_hProp Wx); intros [Sx|ezx]. * induction (ishinh_irrel (ii1 Sx) Wx); change (hProptoType (TOSrel S (x,,Sx) (y,,Sy))) in xy; change empty in wx. exact wx. * induction ezx; induction (ishinh_irrel (ii2 (idpath z)) Wx); change unit in wx; change empty in xy. exact xy. - induction ezy. apply (squash_to_hProp Ww); intros [Sw|ezw]. + induction (ishinh_irrel (ii1 Sw) Ww), (ishinh_irrel (ii2 (idpath z)) Wy). exact tt. + induction ezw, (ishinh_irrel (ii2 (idpath z)) Wy). induction (ishinh_irrel (ii2 (idpath z)) Ww). exact tt. } { intros [x Wx]. apply (squash_to_hProp Wx); intros [Sx|ezx]. - induction (ishinh_irrel (ii1 Sx) Wx). change (hProptoType (TOSrel S (x,,Sx) (x,,Sx))). apply TOrefl. - induction ezx. induction (ishinh_irrel (ii2 (idpath z)) Wx); change unit. exact tt. } } { intros [x Wx] [y Wy] xy yx. apply eqset_to_path. apply (squash_to_hProp Wx); intros [Sx|ezx]. - induction (ishinh_irrel (ii1 Sx) Wx). apply (squash_to_hProp Wy); intros [Sy|ezy]. + induction (ishinh_irrel (ii1 Sy) Wy); change (hProptoType (TOSrel S (x,,Sx) (y,,Sy))) in xy; change (hProptoType (TOSrel S (y,,Sy) (x,,Sx))) in yx. apply subtypePath_prop; change (x=y). exact (maponpaths pr1 (TOanti S _ _ xy yx)). + induction ezy. induction (ishinh_irrel (ii2 (idpath z)) Wy); change unit in xy; change empty in yx. apply subtypePath_prop; change (x=z). exact (fromempty yx). - induction ezx. induction (ishinh_irrel (ii2 (idpath z)) Wx). apply (squash_to_hProp Wy); intros [Sy|ezy]. + induction (ishinh_irrel (ii1 Sy) Wy); change unit in yx; change empty in xy. apply subtypePath_prop; change (z=y). exact (fromempty xy). + induction ezy. apply subtypePath_prop; change (z=z). reflexivity. } } { intros [x Wx] [y Wy]. apply (squash_to_hProp Wx); intros [Sx|ezx]. - induction (ishinh_irrel (ii1 Sx) Wx). apply (squash_to_hProp Wy); intros [Sy|ezy]. + induction (ishinh_irrel (ii1 Sy) Wy). generalize (TOtot S (x,,Sx) (y,,Sy)); apply hinhfun; intros [xy|yx]. * apply ii1. exact xy. * apply ii2. exact yx. + induction ezy. induction (ishinh_irrel (ii2 (idpath z)) Wy); change (htrue ∨ hfalse). exact (hinhpr (ii1 tt)). - induction ezx. induction (ishinh_irrel (ii2 (idpath z)) Wx). apply (squash_to_hProp Wy); intros [Sy|ezy]. + induction (ishinh_irrel (ii1 Sy) Wy); change (hfalse ∨ htrue). exact (hinhpr (ii2 tt)). + induction ezy. induction (ishinh_irrel (ii2 (idpath z)) Wy); change (htrue ∨ htrue). exact (hinhpr (ii2 tt)). } Defined.
Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets.