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