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. exact (pr2 (pr222 Φ) w x y z f g h ww). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations.