meithecatte

%define is_gpr(r) \
    (%isidni(r, ax) || %isidni(r, cx) || %isidni(r, dx) || %isidni(r, bx) || \
     %isidni(r, sp) || %isidni(r, bp) || %isidni(r, si) || %isidni(r, di))

%define num_gpr(r) \
    (0*%isidni(r, ax) + 1*%isidni(r, cx) + 2*%isidni(r, dx) + 3*%isidni(r, bx) + \
     4*%isidni(r, sp) + 5*%isidni(r, bp) + 6*%isidni(r, si) + 7*%isidni(r, di))

%macro reginstr 4
    %if is_gpr(%3) && is_gpr(%4)

meithecatte

{-# 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' → _