Proposition pentagon_eq_holds_ord : pentagon_eq tensor_functor_ord tensor_associator_ord. 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.
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.