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では半角の=
は定義の構文として利用されるため、ここでは全角の等号=
を使った。