(p : P) (r : left x0 = p) : Type := SPushout_ind Q (fun p => left x0 = p -> Type) (@codeleft x0) (@coderight x0) ap_code_glue p r.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.