Ocodeleft2a -> Ocodeleft2b. Proof. intros [s q01 w u]. exact (Build_Ocodeleft2b s y1 q01 q11 w u). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.