`{Univalence} {A : Type} {x : A} (B : forall (y : A), (x = y) -> Type) {y : A} (p : x = y) (u : B x idpath) (f : forall (q:x=x), B x q <~> B y (q @ p)) (ev : ap10 (apD B p) p = transport_arrow_toconst p (B x) p @ path_universe_uncurried (@equiv_transport _ (B y) ((p @ p^) @ p) p (concat_pV_p p p) oE (f (p @ p^)) oE @equiv_transport _ (B x) (transport (fun y => x = y) p^ p) (p @ p^) (transport_paths_r p^ p))) : transport (fun yp:{y:A & x=y} => B yp.1 yp.2) (path_contr (A := {y:A & x=y}) (x;idpath) (y;p)) u = transport (B y) (concat_1p _) (f idpath u). Proof. destruct p; cbn in *. apply (fun e => e @ concat_1p _) in ev. apply moveR_equiv_V in ev. apply (ap equiv_fun) in ev. apply ap10 in ev. specialize (ev u). cbn in ev. exact ev. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.