proposition: Proposition indexed_cat_lassociator {w x y z : C} (f : w --> x) (g : x --> y) (h : y --> z) (ww : Φ w) : indexed_cat_comp Φ g h ((Φ $ f) ww) · indexed_cat_comp Φ f (g · h) ww · idtoiso (maponpaths (λ k, (Φ $ k) ww) (assoc f g h)) = # (Φ $ h) (indexed_cat_comp Φ f g ww) · indexed_cat_comp Φ (f · g) h ww.
proof: Proof. exact (pr2 (pr222 Φ) w x y z f g h ww). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations