O (Pushout (O_functor O codeleft01) (O_functor O Ocodeleft02)) <~> O (Pushout codeleft01 Ocodeleft02) := equiv_inverse (equiv_O_pushout O _ _).
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.