(c : codeleft0) : equiv_Ocodeleft2 (to O _ (Ocodeleft02 c)) = to O _ (codeleft02 c). Proof. destruct c. unfold equiv_Ocodeleft2. Opaque equiv_Ocodeleft2plus. cbn. refine (ap _ (ap _ (to_O_natural _ _ _)) @ _). refine (ap _ (to_O_natural _ _ _) @ _). refine (to_O_natural _ _ _ @ _). apply ap. rapply Ocodeleft02plus_02b. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.