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