Lemma isasetmonfunstn n m : isaset ( monfunstn n m ) . Proof. intros . apply ( isofhleveltotal2 2 ) . { apply impred. intro t. apply isasetstn. } intro f. apply impred; intro i. apply impred; intro j. apply impred; intro l. apply isasetaprop, propproperty. Defined.
Require Import UniMath.MoreFoundations.Tactics.