fact: Definition ehlnat_pp {X} {a : X} (u : idpath a = idpath a) {v w : idpath a = idpath a} (p : v = 1) (q : 1 = w) : (ehlnat u p [-] ehlnat u q) @ whiskerL _ (whiskerR_pp _ p q)^ = (whiskerR (whiskerL_pp _ p q)^ _) @ ehlnat u (p @ q).
imports: HoTT(Basics Types)