codeleft0 -> codeleft2. Proof. intros [s y0 v q00 q10 w u d]. exact (Build_codeleft2 y0 q00 q10 u). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.