parameterとindexとequality

Ind.agda

-- 各データ型に対する帰納法の定義を考えると，
-- ≡の定義の仕方(parameter1つとindex1つ/index2つ)による差がわかる
module Ind where

-- ℕ
data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

-- ℕに関する帰納法
ℕ-ind : (P : ℕ → Set) → P zero → (∀ n → P n → P (suc n)) → (∀ n → P n)
ℕ-ind P base step zero = base
ℕ-ind P base step (suc n) = ℕ-ind (λ x → P (suc x)) (step zero base) (λ x → step (suc x)) n

-- List
data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

-- Listに関する帰納法
List-ind : ∀ {A : Set} (P : List A → Set) → P [] → (∀ x xs → P xs → P (x ∷ xs)) → (∀ xs → P xs)
List-ind P base step [] = base
List-ind P base step (x ∷ xs) = step x xs (List-ind P base step xs)

-- Vec
data Vec (A : Set) : ℕ → Set where
  [] : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

-- Vecに関する帰納法
Vec-ind : ∀ {A : Set} (P : ∀ {n} → Vec A n → Set) → P [] → (∀ {n} x xs → P {n} xs → P (x ∷ xs)) → (∀ {n} xs → P {n} xs)
Vec-ind P base step [] = base
Vec-ind P base step (x ∷ xs) = step x xs (Vec-ind P base step xs)

-- ≡
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

-- ≡に関する帰納法
≡-ind : ∀ {A : Set} {x : A} (P : A → Set) → P x → (∀ y → x ≡ y → P y)
≡-ind P base x refl = base

-- ≡'
data _≡'_ {A : Set} : A → A → Set where
  refl : ∀ {x} → x ≡' x

-- ≡'に関する帰納法
≡'-ind : ∀ {A : Set} (P : A → A → Set) → (∀ x → P x x) → (∀ x y → x ≡' y → P x y)
≡'-ind P base x .x refl = base x

-- Pの形が違う
-- ≡'では 両辺込みでの命題 になるが，≡ では 片方のみでの命題 となり，
-- 左辺のみでの命題 から 右辺のみでの命題 を示せる
--
-- 「任意の命題Pに対しP xとP yが同じ結果になるときにxとyが等しいとする」
-- がLeibniz Equalityなので，parameterに1つindexに1つの≡が採用される
-- ちなみに，Relation.Binary.PropositionalEquality.Core.substは，
-- ≡-indと引数の順序が異なるだけ