Pushout Ocodeleft2ab Ocodeleft2ac <~> codeleft2plus. Proof. refine ((equiv_sigma_pushout _ _ _ _ _)^-1 oE _). srefine (equiv_pushout _ _ _ _ _). - srefine (equiv_functor_sigma_id _ oE _). 2:intro; refine (equiv_functor_prod' _ _); apply equiv_path_sigma. make_equiv_contr_basedpaths. - srefine (equiv_functor_sigma_id _ oE _). 2:intro; apply equiv_path_sigma. make_equiv. - srefine (equiv_functor_sigma_id _ oE _). 2:intro; apply equiv_path_sigma. make_equiv_contr_basedpaths. - intros; reflexivity. - intros; reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.