fact: Definition wlrnat_V {X} {a : X} {u v x y : idpath a = idpath a} p q : whiskerR (wlrnat p q) (eh v y) @ (ehrnat q x [-] ehlnat v p) = (ehlnat u p [-] ehrnat q y) @ whiskerL (eh u x) (wlrnat q p)^.
imports: HoTT(Basics Types)