Definition unit_woset : WellOrderedSet. Proof. exists (_,,isasetunit). use tpair. - intros x y. exists (x = y). abstract (apply isapropifcontr, isapropunit). - repeat split. + now intros x y z []. + now intros x. + intros [] [] H H2. now apply H2, inl. + intros T t'; apply (squash_to_hProp t'); clear t'; intros [[] H]. apply hinhpr; exists tt. now split; [|intros []]. 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.