Inductive Identity

https://1lab.dev/Data.Id.Base.html#inductive-identity

data _≡i_ {ℓ} {A : Type ℓ} (x : A) : A → Type ℓ where
  refli : x ≡i x

{-# BUILTIN EQUALITY _≡i_ #-}