Definition Δ_mor_constr { n m : nat } ( f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn ) ( pk : ∏ x y : (⟦ n ⟧)%stn, x ≤ y -> f x ≤ f y) : (Δ_ob_constr n) --> (Δ_ob_constr m) := (make_monfunstn f pk).
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.CategoryTheory.SimplicialSets.