Cyl f <~> B. Proof. symmetry. srapply Build_Equiv. 1:apply cyr. srapply Build_IsEquiv. - srapply Cyl_rec. + exact f. + exact idmap. + reflexivity. - srapply Cyl_ind. + intros a; cbn. symmetry; apply cyglue. + intros b; reflexivity. + intros a; cbn. apply dp_paths_FFlr. rewrite Cyl_rec_beta_cyglue. apply concat_pV_p. - intros b; reflexivity. - intros b; reflexivity. Defined.
Require Import HoTT.Basics Cubical.DPath Cubical.PathSquare. Require Import Colimits.Pushout.