fact: Definition codeglue5 : O (Pushout (fun x : Ocodeleft2a => pushr' codeleft01 Ocodeleft02b (Ocodeleft2ab x)) Ocodeleft2ac) <~> O (Pushout Ocodeleft2a1 Ocodeleft2ac).
imports: HoTT.Basics HoTT.Types Colimits.Pushout Colimits.SpanPushout Homotopy.Join.Core Truncations