O (Pushout Ocodeleft2a1 Ocodeleft2ac) <~> O Ocodeleft2c := equiv_O_functor O (equiv_inverse (Build_Equiv _ _ (pushr' Ocodeleft2a1 Ocodeleft2ac) _)).
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.