proposition: Proposition pentagon_eq_holds_ord : pentagon_eq tensor_functor_ord tensor_associator_ord.
proof: Proof. unfold pentagon_eq. intros. apply U_faithful. rewrite (functor_comp U), (functor_comp U), (functor_comp U). apply fincard_hom_extensionality. unfold tensor_associator_ord. simpl. unfold tensor_associator_ord_nat_trans_data. simpl. intro x. induction (natplusassoc b c d), (natplusassoc a b (c + d)). unfold "·". simpl. induction (natplusassoc (a + b) c d). set (j:= (tensor_id_card (make_dirprod a (b + c + d)))). unfold tensor_data_card in j. simpl in j. unfold "id" in j. simpl in j. unfold idfun. simpl. unfold idfun in j. rewrite j. induction (natplusassoc a (b + c) d). simpl. induction (natplusassoc a b c). simpl. set (j' := (tensor_id_card (make_dirprod (a + b + c) d))). unfold tensor_data_card in j'. simpl in j'. simpl in j'. unfold "id" in j'. simpl in j'. unfold idfun in *. rewrite j'. 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