{A B : Type} {f : A -> B} {A' B' : Type} {f' : A' -> B'} {wA : A <~> A'} {wB : B <~> B'} (wf : f' o wA == wB o f) : f o (wA ^-1) == (wB ^-1) o f'. Proof. intros a'. path_via (wB ^-1 (wB (f (wA ^-1 a')))). - apply inverse, eissect. - apply ap, (concat (wf _)^). apply ap, eisretr. Defined.
Require Import Basics.Overture Basics.PathGroupoids Basics.Tactics.