fact: Definition code_beta_glue (x1 : X) (y1 : Y) (q11 : Q x1 y1) (r : left x0 = right y1) : ap10 (apD code (glue q11)) r = transport_arrow_toconst (glue q11) codeleft r @ path_universe_uncurried (@equiv_transport _ coderight ((r @ (glue q11)^) @ glue q11) r (concat_pV_p r (glue q11)) oE (codeglue (r @ (glue q11)^) q11) oE @equiv_transport _ codeleft (transport (fun y : SPushout Q => left x0 = y) (glue q11)^ r) (r @ (glue q11)^) (transport_paths_r (glue q11)^ r)).
imports: HoTT.Basics HoTT.Types Colimits.Pushout Colimits.SpanPushout Homotopy.Join.Core Truncations