Lemma isaprop_iswofun {X Y : WellOrderedSet} (f : X → Y) : isaprop (iswofun f). Proof. intros h; apply isapropdirprod; do 3 (apply impred_isaprop; intros). - now apply propproperty. - now apply isapropishinh. 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.