proposition: Proposition pentagon_eq_holds_card : pentagon_eq tensor_functor_card tensor_associator_card.
proof: Proof. unfold pentagon_eq. intros. apply fincard_hom_extensionality. simpl. unfold tensor_associator_card_nat_trans_data. simpl. intro x. induction (natplusassoc b c d). simpl. induction (natplusassoc a b (c + d)). simpl. unfold "·". simpl. induction (natplusassoc (a + b) c d). simpl. unfold "id". simpl. set (k:=(tensor_id_card (make_dirprod a (b + c + d)))). unfold "id" in k. simpl in k. simpl. unfold "id" in k. simpl in k. unfold Δ_sdg_ob_constr. rewrite k. induction (natplusassoc a (b + c) d), (natplusassoc a b c). simpl. set (k':=(tensor_id_card (make_dirprod (a + b + c) d))). unfold "id" in k'. simpl in k'. unfold "id" in k'. simpl in k'. rewrite k'. reflexivity. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.NaturalNumbers UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.FiniteSets UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.CategoryTheory.SimplicialSets