(a : morphism C x3 x4) (b : morphism C x2 x3) (c : morphism C x1 x2) (d : morphism C x0 x1) : a o b o c o d = (a o ((b o c) o d)). Proof. rewrite !associativity; reflexivity. Qed.
Require Import Category.Core Functor.Core. Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.