fact: Definition code (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.
imports: HoTT.Basics HoTT.Types Colimits.Pushout Colimits.SpanPushout Homotopy.Join.Core Truncations