Definition rassociator_transf' (a b c d : C) : pair_functor hcomp_functor (functor_identity _) ∙ hcomp_functor ⟹ precategory_binproduct_unassoc (hom_precategory a b) (hom_precategory b c) (hom_precategory c d) ∙ pair_functor (functor_identity _) hcomp_functor ∙ hcomp_functor := rassociator_fun',, rassociator_fun'_natural.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.