(y1 : Y) (r : left x0 = right y1) (c : code (right y1) r) : center_code (right y1) r = c. Proof. change (coderight r) in c. unfold coderight in c. revert c; refine (O_indpaths _ _ _); intros [q01 t]. unfold center_code, center_code1. destruct t. rewrite (transport_singleton code (glue q01) _ (fun r => @codeglue x0 x0 r y1 q01) (code_beta_glue x0 y1 q01 (glue q01))). unfold codeglue. do 6 change_apply_equiv_compose. rewrite codeglue1_pushl, codeglue2_pushl, codeglue3_pushl, codeglue4_pushl, codeglue5_pushl, codeglue6_pushl, codeglue7_to_O. rewrite <- (ap_transport (concat_1p (glue q01)) (fun r => to O (hfiber glue r)) _). apply ap; unfold hfiber; rewrite transport_sigma'. apply ap; rewrite transport_paths_r. Transparent frobnicate. cbn. Opaque frobnicate. rewrite (transport_compose (fun q => glue q @ (glue q01)^ = 1%path) pr1). unfold path_sigma'; rewrite ap_V, ap_pr1_path_sigma, transport_1. destruct (glue q01); reflexivity. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.