Definition iswofun {X Y : WellOrderedSet} (f : X → Y) : UU := (iscomprelrelfun (WOrel X) (WOrel Y) f) × (∏ (x : X) (y : Y), y < f x → ∃ (z : X), z < x × f z = y).
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.