Lemma iswofun_funcomp {X Y Z : WellOrderedSet} (f : wofun X Y) (g : wofun Y Z) : iswofun (pr1 g ∘ pr1 f). Proof. induction f as [f [h1f h2f]]. induction g as [g [h1g h2g]]. split. - intros x y hxy. exact (h1g _ _ (h1f _ _ hxy)). - intros x z hf. apply (squash_to_hProp (h2g (f x) z hf)); intros [y [h1y h2y]]. apply (squash_to_hProp (h2f x y h1y)); intros [x' [h1x' h2x']]. apply hinhpr; exists x'; cbn. now rewrite h2x'. 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.