對 List 取 quotient

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan hiding (_+_)
open import MLTT.List
open import MGS.MLTT using (has-decidable-equality)
open import UF.FunExt
open import UF.Base using (ap₂; happly)
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Sets
open import UF.Sets-Properties
open import Quotient.Type
open import Integers.Type
open import Integers.Addition
open import Integers.Negation

module ag-YGG9
  (fe : Fun-Ext)
  (sq : general-set-quotients-exist (λ 𝓥 → 𝓥))
  where
open general-set-quotients-exist sq

data Unit : 𝓤₀ ̇ where
  Meter Kilogram Second : Unit

Unit-≟ : has-decidable-equality Unit
Unit-≟ Meter    Meter    = inl refl
Unit-≟ Kilogram Kilogram = inl refl
Unit-≟ Second   Second   = inl refl
Unit-≟ Meter    Kilogram = inr λ ()
Unit-≟ Meter    Second   = inr λ ()
Unit-≟ Kilogram Meter    = inr λ ()
Unit-≟ Kilogram Second   = inr λ ()
Unit-≟ Second   Meter    = inr λ ()
Unit-≟ Second   Kilogram = inr λ ()

最直覺的想法是繼續用 List (Unit × ℤ) 為 raw representation，但需要定義等價類取 quotient 去掉那些我們不想要的情況。為此我們需要定義指數在所有單位相同來決定的等價關係

exp : Unit → List (Unit × ℤ) → ℤ
exp u [] = pos 0
exp u ((v , n) ∷ xs) with Unit-≟ u v
... | inl _ = n + exp u xs
... | inr _ = exp u xs

us₁ ≈ us₂ 若且唯若 exp u us₁ = exp u us₂ 對所有 u 成立

_≈_ : List (Unit × ℤ) → List (Unit × ℤ) → 𝓤₀ ̇
us₁ ≈ us₂ = (u : Unit) → exp u us₁ ＝ exp u us₂

≈-prop : is-prop-valued _≈_
≈-prop us₁ us₂ = Π-is-prop fe (λ u → ℤ-is-set)

≈-refl : reflexive _≈_
≈-refl us u = refl

≈-sym : symmetric _≈_
≈-sym us vs h u = (h u) ⁻¹

≈-trans : transitive _≈_
≈-trans us vs ws h k u = h u ∙ k u

≋ : EqRel (List (Unit × ℤ))
≋ = _≈_ , ≈-prop , ≈-refl , ≈-sym , ≈-trans

Units : 𝓤₀ ̇
Units = List (Unit × ℤ) / ≋

這邊證明了單位 u 在兩個 List 中的指數相加跟對 concat 起來的 List 計算 u 的指數一定是同一個數字

exp-++ : (u : Unit) (xs ys : List (Unit × ℤ))
       → exp u (xs ++ ys) ＝ exp u xs + exp u ys
exp-++ u []              ys = ℤ-zero-left-neutral (exp u ys) ⁻¹
exp-++ u ((v , n) ∷ xs) ys with Unit-≟ u v
... | inl _ = ap (n +_) (exp-++ u xs ys) ∙ ℤ+-assoc n (exp u xs) (exp u ys) ⁻¹
... | inr _ = exp-++ u xs ys

再來證明 concat 是遵守 ≈ 關係的

++-resp : {us₁ us₁' us₂ us₂' : List (Unit × ℤ)}
        → us₁ ≈ us₁' → us₂ ≈ us₂' → (us₁ ++ us₂) ≈ (us₁' ++ us₂')
++-resp {us₁} {us₁'} {us₂} {us₂'} h k u =
  exp u (us₁ ++ us₂)    ＝⟨ exp-++ u us₁ us₂ ⟩
  exp u us₁ + exp u us₂ ＝⟨ ap₂ _+_ (h u) (k u) ⟩
  exp u us₁' + exp u us₂' ＝⟨ exp-++ u us₁' us₂' ⁻¹ ⟩
  exp u (us₁' ++ us₂') ∎

這邊定義一個 helper，實現 raw representation 乘上 Units 得到 Units 的運算，這可以幫助我們簡化等一下要定義的完整單位乘法

*-unit-r : List (Unit × ℤ) → Units → Units
*-unit-r xs = mediating-map/ ≋ (/-is-set ≋)
                (λ ys → η/ ≋ (xs ++ ys))
                (λ {ys} {ys'} k →
                   η/-identifies-related-points ≋
                     (++-resp {xs} {xs} (≈-refl xs) k))

定義最後的單位乘法

*-unit : Units → Units → Units
*-unit = mediating-map/ ≋ (Π-is-set fe (λ _ → /-is-set ≋))
           *-unit-r
           λ {xs} {xs'} h → dfunext fe (λ q → resp-left q h)
  where
  resp-left : (q : Units) {xs xs' : List (Unit × ℤ)}
            → xs ≈ xs' → *-unit-r xs q ＝ *-unit-r xs' q
  resp-left q {xs} {xs'} h =
    /-induction ≋ (λ q → /-is-set ≋ {*-unit-r xs q} {*-unit-r xs' q})
      on-list
      q
    where
    on-list : (ys : List (Unit × ℤ))
            → *-unit-r xs (η/ ≋ ys) ＝ *-unit-r xs' (η/ ≋ ys)
    on-list ys =
      *-unit-r xs (η/ ≋ ys) ＝⟨ universality-triangle/ ≋ (/-is-set ≋) _ _ ys ⟩
      η/ ≋ (xs  ++ ys)      ＝⟨ η/-identifies-related-points ≋
                                  (++-resp {xs} {xs'} {ys} {ys} h (≈-refl ys)) ⟩
      η/ ≋ (xs' ++ ys)      ＝⟨ universality-triangle/ ≋ (/-is-set ≋) _ _ ys ⁻¹ ⟩
      *-unit-r xs' (η/ ≋ ys) ∎

我們構造一些案例

1m : Units
1m = η/ ≋ ((Meter , pos 1) ∷ [])

1s : Units
1s = η/ ≋ ((Second , pos 1) ∷ [])

1/s : Units
1/s = η/ ≋ ((Second , negsucc 0) ∷ [])

這裏證明了純量 1 確實是單位乘法的 identity

ε : Units
ε = η/ ≋ []

*-unit-η : (xs ys : List (Unit × ℤ))
         → *-unit (η/ ≋ xs) (η/ ≋ ys) ＝ η/ ≋ (xs ++ ys)
*-unit-η xs ys =
  *-unit (η/ ≋ xs) (η/ ≋ ys)
    ＝⟨ happly
          (universality-triangle/ ≋ (Π-is-set fe (λ _ → /-is-set ≋)) _ _ xs)
          (η/ ≋ ys) ⟩
  *-unit-r xs (η/ ≋ ys) ＝⟨ universality-triangle/ ≋ (/-is-set ≋) _ _ ys ⟩
  η/ ≋ (xs ++ ys) ∎

ε-is-unit-of-* : (xs : List (Unit × ℤ)) → *-unit ε (η/ ≋ xs) ＝ *-unit (η/ ≋ xs) ε
ε-is-unit-of-* xs =
  *-unit ε (η/ ≋ xs) ＝⟨ *-unit-η [] xs ⟩
  η/ ≋ ([] ++ xs) ＝⟨ ap (λ - → η/ ≋ -) ([]-right-neutral xs) ⟩
  η/ ≋ (xs ++ []) ＝⟨ *-unit-η xs [] ⁻¹ ⟩
  *-unit (η/ ≋ xs) ε ∎

單位取消確實如想像中一樣運作

cancel : *-unit 1s 1/s ＝ ε
cancel =
  *-unit 1s 1/s ＝⟨ *-unit-η _ _ ⟩
  η/ ≋ (((Second , pos 1) ∷ []) ++ ((Second , negsucc 0) ∷ []))
    ＝⟨ η/-identifies-related-points ≋ I ⟩
  η/ ≋ [] ∎
  where
  I : ((Second , pos 1) ∷ (Second , negsucc 0) ∷ []) ≈ []
  I Meter    = refl
  I Kilogram = refl
  I Second   = refl

不同單位確實有被等價類分開

different-units : (u₁ u₂ : Unit) → ¬ (u₁ ＝ u₂) → ¬ (((u₁ , pos 1) ∷ []) ≈ ((u₂ , pos 1) ∷ []))
different-units Meter    Meter    ne h = ne refl
different-units Meter    Kilogram ne h = pos-succ-not-zero 0 (h Meter)
different-units Meter    Second   ne h = pos-succ-not-zero 0 (h Meter)
different-units Kilogram Meter    ne h = pos-succ-not-zero 0 (h Kilogram)
different-units Kilogram Kilogram ne h = ne refl
different-units Kilogram Second   ne h = pos-succ-not-zero 0 (h Kilogram)
different-units Second   Meter    ne h = pos-succ-not-zero 0 (h Second)
different-units Second   Kilogram ne h = pos-succ-not-zero 0 (h Second)
different-units Second   Second   ne h = ne refl

不過這個方法雖然概念上很直觀，但就如同你直接看到的，寫起來非常複雜。

對 List 取 quotient [ag-YGG9]