J.agda

open import Data.Product
open import Relation.Binary.PropositionalEquality

singleton-contractible : {A : Set}(x : A) (p : Σ[ y ∈ A ] x ≡ y) → (x , refl) ≡ p
singleton-contractible x ( .x , refl )= refl

transport : {A : Set}(B : A → Set)(x y : A) → x ≡ y → B x → B y
transport B x .x refl b = b

J : {A : Set}(B : (x y : A) → x ≡ y → Set) → ((x : A) → B x x refl) → (x y : A)(p : x ≡ y) → B x y p
J {A} B base x y p = transport C (x , refl) (y , p) (singleton-contractible x (y , p)) (base x)
  where C : Σ[ y ∈ A ] x ≡ y → Set
        C (y , p) = B x y p