同一視型

定義

数学において、「2つの数学的対象が等しい」ということは重要な概念である。Martin-löf型理論において、同一視型(identity type)がその役割を果たす。

module identity-type where

data Id (A : Set) (x : A) : A → Set where
  refl : Id A x x

infix 40 _＝_
_＝_ : {A : Set} → A → A → Set
x ＝ y = Id _ x y

演算と性質

2つの数学的対象が等しいとき、片方に成り立つ性質はもう一方にも成り立つ。これは以下のtransportによって表現される:

private
  variable
    A B C : Set
    w x y z : A

transport : (P : A → Set) → x ＝ y → P x → P y
transport _ refl Px = Px

これはxとyが等しいとき、述語Pがxについて成り立つのであれば、Pはyに対しても成り立つことを意味する。

合同規則(congruence)は次のように与えられる。

cong : (f : A → B) → x ＝ y → f x ＝ f y
cong _ refl = refl

cong₂ : (f : A → B → C) → w ＝ y → x ＝ z → f w x ＝ f y z
cong₂ _ refl refl = refl

同一視型は対称律と推移律を満たす:

sym : x ＝ y → y ＝ x
sym refl = refl

trans : ∀ {x y z : A} → x ＝ y → y ＝ z → x ＝ z
trans refl e = e

infixl 50 _∙_
_∙_ : ∀ {x y z : A} → x ＝ y → y ＝ z → x ＝ z
_∙_ = trans

記法上の利便性を得るため、e1 ∙ e2 ∙ e3のように書いてtrans (trans e1 e2) e3を表現できるようにした。

以下の定義は複数の等式を数珠繋ぎにして、より長い等式を示すための便利な道具である。自然数のページなど、色々な所で使われている。

infix 60 _∎
_∎ : (x : A) → x ＝ x
_ ∎ = refl

infixr 40 _＝⟨_⟩_
_＝⟨_⟩_ : (x : A) → ∀ {y z} → (x ＝ y) → (y ＝ z) → x ＝ z
_ ＝⟨ e1 ⟩ e2 = e1 ∙ e2