Definition U_Mon_Strong : strong_monoidal_functor AugmentedSimplexCategory FinCard. Proof. exists U_Mon_Lax. split. - cbn. unfold is_z_isomorphism. use tpair. + simpl. exact (idfun (⟦ tensor_unit ⟧)%stn). + abstract(simpl; unfold is_inverse_in_precat; split; unfold U_ε; exact (id_right (C:=Δ_sdg) (idfun _)); unfold U_ε; exact (id_right (C:=Δ_sdg) (idfun _))). - unfold is_nat_z_iso. simpl. intro c. induction c as [n m]. unfold is_z_isomorphism. simpl. exists (idfun (⟦ n + m⟧)%stn). abstract(unfold is_inverse_in_precat; split; exact (id_right (C:=Δ_sdg) (idfun _)); exact (id_right (C:=Δ_sdg) (idfun _))). 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.