proposition: Lemma iswofun_funcomp {X Y Z : WellOrderedSet} (f : wofun X Y) (g : wofun Y Z) : iswofun (pr1 g ∘ pr1 f).
proof: 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.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets