Ocodeleft2a1 == codeleft01 o Ocodeleft02b^-1 o Ocodeleft2ab. Proof. intros; reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.