Definition monfunmonprop { n m : nat } (f : monfunstn n m) := pr2 f. Local Arguments precategory_binproduct_mor /. Local Definition ordinal_hom : ∏ a b : ob (Δ ⊠ Δ), a --> b -> (ordinal_addition a) --> (ordinal_addition b). Proof. simpl. intros nn' mm'. induction nn' as [n n'], mm' as [m m']. intro fg. simpl in fg. induction fg as [f g]. unshelve refine (make_monfunstn _ _). - exact (sumfn f g). - intros x y. induction f as [f_fun f_guarantee]. induction g as [g_fun g_guarantee]. intro l. simpl. change (sumfn f_fun g_fun x ≤ sumfn f_fun g_fun y). unfold sumfn. induction natlthorgeh as [xl | xgth], (natlthorgeh y n) as [yl | ygth]. + simpl. exact (f_guarantee (pr_n_m_l x xl) (pr_n_m_l y yl) l). + simpl. apply natlthtoleh. apply (natgehgthtrans _ m _ ). * exact (natlehmplusnm _ m). * exact (stnlt (f_fun _)). + contradiction (natgthnegleh yl). exact (istransnatleh xgth l). + simpl. change (g_fun (pr_n_m_r x xgth) + m ≤ g_fun (pr_n_m_r y ygth) +m ). apply natlehandplusr. apply g_guarantee. rewrite pr_n_m_r_compute. rewrite pr_n_m_r_compute. exact (natgehandminusr _ _ n l). Defined.
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.