(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)). Proof. refine (ap (fun h => ap10 h r) (spushout_ind_beta_sglue Q (fun p => left x0 = p -> Type) (@codeleft x0) (@coderight x0) ap_code_glue x1 y1 q11) @ _). refine (ap10_path_arrow _ _ _ _). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.