(inh : merely { y0 : Y & Q x0 y0 }) (p : P) (r : left x0 = p) : Contr (code p r). Proof. strip_truncations. destruct inh as [y0 q00]. exact (Build_Contr _ (center_code p r) (contraction_code q00 (p;r))). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.