(x1 : X) (y1 : Y) (q11 : Q x1 y1) : transport (fun p : SPushout Q => left x0 = p -> Type) (glue q11) codeleft = coderight. Proof. apply path_arrow; intros z. refine ((transport_arrow_toconst _ _ _) @ _). apply path_universe_uncurried. refine (_ oE equiv_transport codeleft (transport_paths_r _ _)). refine (_ oE codeglue _ q11). refine (equiv_transport coderight _). refine (concat_pV_p z (glue q11)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.