O (Pushout Ocodeleft2ab Ocodeleft2ac) <~> O codeleft2. Proof. refine ((equiv_O_functor O (equiv_sigma_contr (fun yqqu : codeleft2 => O (Join ((x0; codeleft2_q00 yqqu) = (x1; codeleft2_q10 yqqu)) ((codeleft2_y0 yqqu ; codeleft2_q10 yqqu) = (y1; q11)))))) oE _). refine ((equiv_O_sigma_O O _)^-1 oE _). apply equiv_O_functor. apply equiv_Ocodeleft2plus. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.