code (left x0) 1. Proof. change (codeleft (idpath (left x0))). unfold codeleft. apply to, pushl. unfold codeleft1. exact (idpath; idpath). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.