{X} {a b : X} {u v w : a = b} (p : u = v) (q : v = w) : urnat p [-] urnat q = whiskerR (whiskerR_pp _ p q)^ _ @ urnat (p @ q). Proof. by destruct p, q, u. Defined.
From HoTT Require Import Basics Types.