Definition U_μ : monoidal_functor_map AugmentedSimplexCategory FinCard U. Proof. unfold monoidal_functor_map. simpl. unfold "⟹". use tpair. - unfold nat_trans_data. unfold precategory_binproduct_data. simpl. simpl. intro x. induction x as [n m]. simpl. exact (idfun (⟦ n + m ⟧)%stn). - abstract(cbv beta; unfold is_nat_trans; simpl; intros x x'; induction x as [n m], x' as [n' m']; unfold precategory_binproduct_mor; intro fg; simpl in fg; induction fg as [f g]; simpl; set (s:= id_left (Δ_sdg_mor_constr (AugmentedSimplexCategory.sumfn (pr1 f) (pr1 g)))); unfold "id" in s; simpl in s; unfold Δ_sdg_mor_constr in s; unfold Δ_sdg_ob_constr in s; unfold idfun; simpl in s; simpl; induction f as [ffun fguarantee], g as [gfun gguarantee]; simpl in s; simpl; unfold "·"; unfold "·" in s; simpl in s; simpl; unfold idfun in s; rewrite s; reflexivity). 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.