proposition: Proposition triangle_eq_holds_ord : triangle_eq tensor_functor_ord tensor_unit tensor_left_unitor_ord tensor_right_unitor_ord tensor_associator_ord.
proof: Proof. unfold triangle_eq. simpl. intros a b. apply morphism_extensionality. unfold tensor_functor_ord, functor_fix_snd_arg_ob. simpl. unfold tensor_associator_ord_nat_trans_data. simpl. intro x. induction x as [xval xbd]. unfold sumfn. simpl. set (QJ := internal_paths_rew_r nat (a + 0 + b) _ _ _ _ ). simpl in QJ. assert (xval < a + b) as XLAB'. { rewrite (pathsinv0 (natplusr0 a)). exact xbd. } set (x' := ordconstr xval XLAB'). unfold "·". simpl. assert ((QJ (xval,, xbd)) = x') as RW. { apply subtypeInjectivity_prop. simpl in *. unfold QJ. generalize (natplusassoc a 0 b). simpl. generalize (a + b). induction p. reflexivity. } simpl in *. rewrite RW. apply subtypeInjectivity_prop. induction (natlthorgeh xval _) as [XLA | XGA]. - simpl. assert (xval < a) as XLA'. { rewrite (natplusr0 a) in XLA. exact XLA. } rewrite (natlthorgeh_left_branch XLA' _). simpl in *. induction (natplusr0 a). reflexivity. - simpl. assert (xval ≥ a) as XGA'. { rewrite (natplusr0 a) in XGA. exact XGA. } rewrite (natlthorgeh_right_branch XGA' _). simpl in *. rewrite (natplusr0 a). 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