fact: Definition wlrnat_pp_p {X} {a b c : X} {u v : a = b} {x y z : b = c} (p : x = y) (q : y = z) (r : u = v) : (wlrnat p r [-] wlrnat q r) @ whiskerL _ (whiskerL_pp _ p q)^ = whiskerR (whiskerL_pp _ p q)^ _ @ wlrnat (p @ q) r.
imports: HoTT(Basics Types)