{A : Type} {x y : A} (p : x = y) (q : idpath x = idpath x) : transport (fun a => idpath a = idpath a) p q = (concat_Vp p)^ @ whiskerL p^ ((concat_1p p)^ @ whiskerR q p @ concat_1p p) @ concat_Vp p. Proof. destruct p. simpl. refine (_ @ (concat_p1 _)^). refine (_ @ (concat_1p _)^). assert (H : forall (p : x = x) (q : 1 = p), (q @ (concat_p1 p)^) @ (concat_1p (p @ 1))^ = whiskerL (idpath x) (idpath 1 @ whiskerR q 1 @ idpath (p @ 1))). { intros p' q'. destruct q'. reflexivity. } transitivity (q @ (concat_p1 1)^ @ (concat_1p 1)^). { simpl; exact ((concat_p1 _)^ @ (concat_p1 _)^). } refine (H 1 q). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.