(c : codeleft0) : (equiv_Ocodeleft2plus (Ocodeleft02 c)).1 = codeleft02 c. Proof. destruct c; reflexivity. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.