{-# OPTIONS --safe --without-K --no-exact-split #-} open import MLTT.Spartan hiding (_+_) open import UF.FunExt open import Integers.Type open import Integers.Addition open import Integers.Negation module ag-FKSF (fe : Fun-Ext) where data Unit : 𝓤₀ ̇ where Meter Kilogram Second : Unit
這裏把組合單位定義成一個函數 u：今天問
u Meter 就會知道公尺這個單位的次方是多少
UL : (X : 𝓤 ̇ ) → 𝓤 ̇ UL X = X → ℤ Units : 𝓤₀ ̇ Units = UL Unit
這個定義的好處之一是沒有單位的定義非常簡單：
ε-unit : Units ε-unit _ = pos 0
單位相乘只需要把自己的指數相加即可
*-unit : Units → Units → Units *-unit us₁ us₂ u = us₁ u + us₂ u
要取單位的乘法反元素可以定義成加法反元素
⁻¹-unit : Units → Units ⁻¹-unit us u = - us u
也就是說，我們根本就是借用了 ℤ
的代數來用，從而大幅簡化了定義。我們可以構造一些範例來看看
1m : Units 1m Meter = pos 1 1m _ = pos 0 1s : Units 1s Second = pos 1 1s _ = pos 0 m³ : Units m³ Meter = pos 3 m³ _ = pos 0 1/s : Units 1/s = ⁻¹-unit 1s
證明這確實有用
cancel-pointwise : *-unit 1s 1/s ＝ ε-unit cancel-pointwise = dfunext fe I where I : (u : Unit) → *-unit 1s 1/s u ＝ ε-unit u I Meter = refl I Kilogram = refl I Second = refl 1m³s : Units 1m³s Meter = pos 3 1m³s Second = pos 1 1m³s _ = pos 0 m³-×̇-1s : *-unit m³ 1s ＝ 1m³s m³-×̇-1s = dfunext fe I where I : (u : Unit) → *-unit m³ 1s u ＝ 1m³s u I Meter = refl I Kilogram = refl I Second = refl
這個方案的好處是他構造寫起來最直覺，在概念上很漂亮（對函數詢問特定單位的指數次方是多少），但證明的複雜性跟 quotient 版本相當。