fact: Definition eh_V_p_pp_gen {X : Type} {a b c d e f : X} {wlx0 x0 wrx0 : a = b} {wlx1 x1 wrx1 : c = d} {wlx2 x2 wrx2 : e = f} {wly0 y0 wry0 : b = d} {wly1 y1 wry1 : a = c} {wlz0 z0 wrz0 : d = f} {wlz1 z1 wrz1 : c = e} {wlyz0 wryz0 : b = f} {wlyz1 wryz1 : a = e} {ulnat_x0 : wlx0 @ 1 = 1 @ x0} {urnat_x0 : wrx0 @ 1 = 1 @ x0} {ulnat_x1 : wlx1 @ 1 = 1 @ x1} {urnat_x1 : wrx1 @ 1 = 1 @ x1} {ulnat_x2 : wlx2 @ 1 = 1 @ x2} {urnat_x2 : wrx2 @ 1 = 1 @ x2} {ulnat_y0 : wly0 @ 1 = 1 @ y0} {urnat_y0 : wry0 @ 1 = 1 @ y0} {ulnat_y1 : wly1 @ 1 = 1 @ y1} {urnat_y1 : wry1 @ 1 = 1 @ y1} {ulnat_z0 : wlz0 @ 1 = 1 @ z0} {urnat_z0 : wrz0 @ 1 = 1 @ z0} {ulnat_z1 : wlz1 @ 1 = 1 @ z1} {urnat_z1 : wrz1 @ 1 = 1 @ z1} {ulnat_yz0 : wlyz0 @ 1 = 1 @ (y0 @ z0)} {urnat_yz0 : wryz0 @ 1 = 1 @ (y0 @ z0)} {ulnat_yz1 : wlyz1 @ 1 = 1 @ (y1 @ z1)} {urnat_yz1 : wryz1 @ 1 = 1 @ (y1 @ z1)} {ehlnat_x0 : wlx0 @ 1 = 1 @ wrx0} {ehlnat_x1 : wlx1 @ 1 = 1 @ wrx1} {ehlnat_x2 : wlx2 @ 1 = 1 @ wrx2} {ehrnat_y0 : wry0 @ 1 = 1 @ wly0} {ehrnat_y1 : wry1 @ 1 = 1 @ wly1} {ehrnat_z0 : wrz0 @ 1 = 1 @ wlz0} {ehrnat_z1 : wrz1 @ 1 = 1 @ wlz1} {ehrnat_yz0 : wryz0 @ 1 = 1 @ wlyz0} {ehrnat_yz1 : wryz1 @ 1 = 1 @ wlyz1} {wlrnat_x_y : wlx0 @ wry0 = wry1 @ wlx1} {wlrnat_y_x : wly1 @ wrx1 = wrx0 @ wly0} {wlrnat_x_z : wlx1 @ wrz0 = wrz1 @ wlx2} {wlrnat_z_x : wlz1 @ wrx2 = wrx1 @ wlz0} {wlrnat_x_yz : wlx0 @ wryz0 = wryz1 @ wlx2} {wlrnat_yz_x : wlyz1 @ wrx2 = wrx0 @ wlyz0} {wrpp_yz0 : wry0 @ wrz0 = wryz0} {wlpp_yz0 : wly0 @ wlz0 = wlyz0} {wrpp_yz1 : wry1 @ wrz1 = wryz1} {wlpp_yz1 : wly1 @ wlz1 = wlyz1} {H_ulnat_yz0 : (ulnat_y0 [-] ulnat_z0) = whiskerR wlpp_yz0 _ @ ulnat_yz0} {H_urnat_yz0 : (urnat_y0 [-] urnat_z0) = whiskerR wrpp_yz0 _ @ urnat_yz0} {H_ulnat_yz1 : (ulnat_y1 [-] ulnat_z1) = whiskerR wlpp_yz1 _ @ ulnat_yz1} {H_urnat_yz1 : (urnat_y1 [-] urnat_z1) = whiskerR wrpp_yz1 _ @ urnat_yz1} {H_ehrnat_yz0 : (ehrnat_y0 [-] ehrnat_z0) @ whiskerL _ wlpp_yz0 = whiskerR wrpp_yz0 _ @ ehrnat_yz0} {H_ehrnat_yz1 : (ehrnat_y1 [-] ehrnat_z1) @ whiskerL _ wlpp_yz1 = whiskerR wrpp_yz1 _ @ ehrnat_yz1} {H_wlrnat_x_yz : (wlrnat_x_y [I] wlrnat_x_z) @ whiskerR wrpp_yz1 _ = whiskerL _ wrpp_yz0 @ wlrnat_x_yz} {H_wlrnat_yz_x : (wlrnat_y_x [-] wlrnat_z_x) @ whiskerL _ wlpp_yz0 = whiskerR wlpp_yz1 _ @ wlrnat_yz_x} (ehlnat_1p_x0 : (ehlnat_x0 [I] urnat_x0) @ 1 = 1 @ ulnat_x0) (ehlnat_1p_x1 : (ehlnat_x1 [I] urnat_x1) @ 1 = 1 @ ulnat_x1) (ehlnat_1p_x2 : (ehlnat_x2 [I] urnat_x2) @ 1 = 1 @ ulnat_x2) {ehrnat_p1_y0 : (ehrnat_y0 [I] ulnat_y0) @ 1 = 1 @ urnat_y0} {ehrnat_p1_y1 : (ehrnat_y1 [I] ulnat_y1) @ 1 = 1 @ urnat_y1} {ehrnat_p1_z0 : (ehrnat_z0 [I] ulnat_z0) @ 1 = 1 @ urnat_z0} {ehrnat_p1_z1 : (ehrnat_z1 [I] ulnat_z1) @ 1 = 1 @ urnat_z1} {ehrnat_p1_yz0 : (ehrnat_yz0 [I] ulnat_yz0) @ 1 = 1 @ urnat_yz0} {ehrnat_p1_yz1 : (ehrnat_yz1 [I] ulnat_yz1) @ 1 = 1 @ urnat_yz1} {wlrnat_V_x_y : whiskerR wlrnat_x_y _ @ (ehrnat_y1 [-] ehlnat_x1) = (ehlnat_x0 [-] ehrnat_y0) @ whiskerL _ wlrnat_y_x^} {wlrnat_V_x_z : whiskerR wlrnat_x_z _ @ (ehrnat_z1 [-] ehlnat_x2) = (ehlnat_x1 [-] ehrnat_z0) @ whiskerL _ wlrnat_z_x^} {wlrnat_V_x_yz : whiskerR wlrnat_x_yz _ @ (ehrnat_yz1 [-] ehlnat_x2) = (ehlnat_x0 [-] ehrnat_yz0) @ whiskerL _ wlrnat_yz_x^} (H_ehrnat_p1_yz0 : Ehrnat_p1_pp 1 1 H_ehrnat_yz0 H_ulnat_yz0 H_urnat_yz0 ehrnat_p1_y0 ehrnat_p1_z0 = ehrnat_p1_yz0) (H_ehrnat_p1_yz1 : Ehrnat_p1_pp 1 1 H_ehrnat_yz1 H_ulnat_yz1 H_urnat_yz1 ehrnat_p1_y1 ehrnat_p1_z1 = ehrnat_p1_yz1) (H_wlrnat_V_x_yz : Wlrnat_V_p_pp H_ehrnat_yz0 H_ehrnat_yz1 H_wlrnat_x_yz H_wlrnat_yz_x wlrnat_V_x_y wlrnat_V_x_z = wlrnat_V_x_yz) : let eh_x_y := concat_p_pp x0 y0 z0 @ whiskerR (((rlucancel_inv (ulnat_x0 [-] urnat_y0))^ @ wlrnat_x_y) @ rlucancel_inv (urnat_y1 [-] ulnat_x1)) z0 in whiskerR (concat_p1 _ @@ concat_p1 _) eh_x_y @ whiskerR (eh_V_gen (ehlnat_1p_x0) (ehlnat_1p_x2) (ehrnat_p1_yz0) (ehrnat_p1_yz1) wlrnat_V_x_yz) eh_x_y @ lrucancel 1 @ whiskerL eh_x_y (Syllepsis.concat_pp_p_p_pp _ _ _)^ @ whiskerL eh_x_y (concat_p1 _ @@ concat_p1 _)^ = (eh_p_pp_gen H_urnat_yz0 H_urnat_yz1 H_wlrnat_x_yz [-] lrucancel (whiskerL _ (ap (fun p => whiskerL y1 p) (moveL_V1 _ _ (eh_V_gen ehlnat_1p_x1 ehlnat_1p_x2 ehrnat_p1_z0 ehrnat_p1_z1 wlrnat_V_x_z))))) [-] (eh_pp_p_gen H_ulnat_yz1 H_ulnat_yz0 H_wlrnat_yz_x [-] lrucancel (whiskerL _ (ap (fun p => whiskerR p z0) (moveL_1V _ _ (eh_V_gen ehlnat_1p_x0 ehlnat_1p_x1 ehrnat_p1_y0 ehrnat_p1_y1 wlrnat_V_x_y))))).
imports: HoTT(Basics Types)