O (Pushout (fun x : Ocodeleft2a => pushr' codeleft01 Ocodeleft02b (Ocodeleft2ab x)) Ocodeleft2ac) <~> O (Pushout Ocodeleft2a1 Ocodeleft2ac). Proof. srefine (equiv_O_functor O (equiv_inverse (equiv_pushout (f := Ocodeleft2a1) (g := Ocodeleft2ac) 1%equiv _ 1%equiv _ _))). - exact (Build_Equiv _ _ (pushl' codeleft01 Ocodeleft02b) _). - intros x. refine (ap _ (Ocodeleft2a1_through_2b0 x) @ _). refine (pglue' codeleft01 Ocodeleft02b _ @ _). apply ap, eisretr. - intros x; reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.