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