proposition: Lemma isasetmonfunstn n m : isaset ( monfunstn n m ) .
proof: 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.
imports: UniMath.MoreFoundations.Tactics UniMath.Combinatorics.FiniteSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.opp_precat