同一視型

module foundations.identity-type where

open import foundations.universe

private variable ℓ : Level

同一視型を定義する。

data Id (A : Type ℓ) (x : A) : A → Type ℓ where
  refl : Id A x x

この型の除去規則は次のように与えられる。

private variable A : Type ℓ

J : ∀ {a : A} (P : (y : A) → Id A a y → Type ℓ)
  → P a refl
  → {x : A}
  → (p : Id A a x)
  → P x p
J P base refl = base

ちなみに、Jの型に現れるℓとAの型に現れるℓは別物である。

また、Aが文脈から明らかであるときは、次のような記法を使う。

_＝_ : ∀ {A : Type ℓ} → A → A → Type ℓ
x ＝ y = Id _ x y

Agdaでは半角の=は定義の構文として利用されるため、ここでは全角の等号＝を使った。