{y0 : Y} (q00 : Q x0 y0) (pr : { p : P & left x0 = p }) (c : code pr.1 pr.2) : center_code pr.1 pr.2 = c. Proof. revert c. srefine (transport (fun pr' => forall c, center_code pr'.1 pr'.2 = c) (path_contr (right y0 ; glue q00) pr) _). clear pr; cbn; intros c. apply contraction_code_right. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.