O Ocodeleft2c <~> coderight (r @ glue q11). Proof. unfold coderight, Ocodeleft2c. apply equiv_O_functor. apply equiv_functor_sigma_id; intros q01. apply equiv_moveL_pM. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.