{A B : Type} {f : A -> B} {g : B -> A} {x1 x2 : A} (p : x1 = x2) (q : x1 = g (f x1)) (r : x2 = g (f x2)) : q @ ap g (ap f p) = p @ r <~> transport (fun x => x = g (f x)) p q = r. Proof. destruct p; simpl. transitivity (q @ 1 = r). - exact (equiv_concat_r (concat_1p r) (q @ 1)). - exact (equiv_concat_l (concat_p1 q)^ r). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.