Proposition pentagon_eq_holds_card : pentagon_eq tensor_functor_card tensor_associator_card. 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.
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.