Ocodeleft2a <~> codeleft1. Proof. etransitivity. 2:{ rapply equiv_functor_sigma_id; intros s. apply frobnicate. } make_equiv. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.