fact: Definition codeglue1 : codeleft <~> O (Pushout (O_functor O codeleft01) (O_functor O codeleft02)) := equiv_O_pushout O _ _.
imports: HoTT.Basics HoTT.Types Colimits.Pushout Colimits.SpanPushout Homotopy.Join.Core Truncations