O (Pushout (O_functor O codeleft01) (O_functor O codeleft02)) <~> O (Pushout (O_functor O codeleft01) (O_functor O Ocodeleft02)). Proof. srefine (equiv_O_functor O (equiv_inverse (equiv_pushout (f := O_functor O codeleft01) (g := O_functor O Ocodeleft02) 1%equiv 1%equiv equiv_Ocodeleft2 _ _))). - intros x; reflexivity. - apply O_indpaths; intros x. abstract (rewrite !to_O_natural; apply Ocodeleft02_02b). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.