fact: Definition center_code (p : P) (r : left x0 = p) : code p r := transport (fun (pr : {p : P & left x0 = p}) => code pr.1 pr.2) (path_contr (A := {p : P & left x0 = p}) (left x0; idpath) (p;r)) center_code1.
imports: HoTT.Basics HoTT.Types Colimits.Pushout Colimits.SpanPushout Homotopy.Join.Core Truncations