proposition: Lemma compose4associativity_helper (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: Proof. rewrite !associativity; reflexivity. Qed.
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences