{-# 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
不過這個方法雖然概念上很直觀，但就如同你直接看到的，寫起來非常複雜。