Dependent equality in dependent type theory

這是從 https://mathstodon.xyz/@MartinEscardo/114751426538568913 學到的技巧。

{-# OPTIONS --safe --without-K #-}
module ag-000C where

open import Agda.Primitive
  renaming (Set to Type; Setω to Typeω)
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

假設我們有

a type X : Type
a family of types A : X → Type indexed by X

那我們常常會遇到有

x y : X
a : A x
b : A y
p : x ＝ y

＝ 是 MLTT 的 identity type，p 是一個 x ＝ y 的證明，這時候如果我們問 a ＝ b 是沒有答案的，因為根據 MLTT，a 跟 b 的類型壓根兒就不一樣，這導致問題連寫都寫不下來，那怎麼辦？

方法是定義高階等式（又稱為 dependent equality 或是 PathOver 或是 path transport），在該依賴項等價的情況下把問題變成新的等式來讓 dependent type 語言表達等式

用案例來說就是如果有個 equality 是「類型不同」的（出於依賴項的不透明性，比如這裡 vector length 輸入的 associative 不同）

先定義一些下面案例會用到的輔助程式：

cong : {X Y : Type} (f : X → Y) {x₀ x₁ : X} → x₀ ≡ x₁ → f x₀ ≡ f x₁
cong {X} {Y} f refl = refl

+-assoc : ∀ l m n → (l + m) + n ≡ l + (m + n)
+-assoc zero     m n = refl
+-assoc (suc l) m n = cong suc (+-assoc l m n)

具體案例 vector ++ 的 associativity

data Vec (A : Type) : Nat → Type where
  [] : Vec A 0
  _::_ : ∀{n} → A → Vec A n → Vec A (suc n)
infixl 40 _::_

_++_ : {Y : Type} {l m : Nat} → (xs : Vec Y l) → (ys : Vec Y m) → Vec Y (l + m)
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
infixl 30 _++_

基於 x₀ ≡ x₁ 定義一個更高階的 equality

higher-equality : {X : Type} (A : X → Type) {x₀ x₁ : X} → A x₀ → x₀ ≡ x₁ → A x₁ → Type
higher-equality A a₀ refl a₁ = a₀ ≡ a₁

但可以根據案例定義比較簡單的版本

_≡[_]_ : {X : Type} {x₀ x₁ : Nat} → Vec X x₀ → x₀ ≡ x₁ → Vec X x₁ → Type
a₀ ≡[ refl ] a₁ = a₀ ≡ a₁

命題 (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs) 無法寫下，因為（meta-level 的）型別不同。所以需要用高階等式描述

cong-cons : {X : Type} {m n : Nat} {xs : Vec X m} {ys : Vec X n}
  (x : X) (p : m ≡ n)
  → xs ≡[ p ] ys → x :: xs ≡[ cong suc p ] x :: ys
cong-cons {X}{A} x refl refl = refl

++-assoc : {X : Type} (l m n : Nat)
  (xs : Vec X l) (ys : Vec X m) (zs : Vec X n)
  → (xs ++ ys) ++ zs ≡[ +-assoc l m n ] xs ++ (ys ++ zs)
++-assoc {X} zero     m n []       ys zs = refl
++-assoc {X} (suc l) m n (x :: xs) ys zs = I
  where
  I : x :: (xs ++ ys) ++ zs ≡[ cong suc (+-assoc l m n) ] x :: (xs ++ (ys ++ zs))
  I = cong-cons x (+-assoc l m n) (++-assoc l m n xs ys zs)

Dependent equality in dependent type theory [ag-000C]