Definition assoc_right : (C ⊠ C) ⊠ C ⟶ C := functor_composite (precategory_binproduct_unassoc _ _ _) (functor_composite (pair_functor (functor_identity _) tensor) tensor).
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering.