Lemma iswofun_idfun {X : WellOrderedSet} : iswofun (idfun X). Proof. split. - now intros x. - intros x y hxy. now apply hinhpr; exists y. Qed.
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.