HfromJ.agda

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

open import HoTT-UF-Agda

ℍ' : {X : 𝓤 ̇ } (x : X) (B : (y : X) → x ＝ y → 𝓥 ̇ )
   → B x (refl x)
   → (y : X) (p : x ＝ y) → B y p
ℍ' {X = X} x B b y p = 𝕁 X A f x y p B b
  where
  A : (x' y' : X) → x' ＝ y' → _
  A x' y' p' = (B' : (y : X) → x' ＝ y → _) → B' x' (refl x') → B' y' p'

  f : (x' : X) → A x' x' (refl x')
  f x' B' b' = b'

ℍs-agreement : {X : 𝓤 ̇ } (x : X) (B : (y : X) → x ＝ y → 𝓥 ̇ )
               (b : B x (refl x)) (y : X) (p : x ＝ y)
             → ℍ x B b y p ＝ ℍ' x B b y p
ℍs-agreement x B b x (refl x) = refl b