{A B C D E F} {f : A -> B} {f': C -> D} {h : A -> C} {g : B -> D} (comm : f' o h == g o f) {f'': E -> F} {h' : C -> E} {g' : D -> F} (comm' : f'' o h' == g' o f') : f'' o (h' o h) == (g' o g) o f. Proof. intros x. path_via (g' (f' (h x))). apply ap, comm. Defined.
Require Import Basics.Overture Basics.PathGroupoids Basics.Tactics.