(p : P) (r : left x0 = p) : code p r := transport (fun (pr : {p : P & left x0 = p}) => code pr.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.