{-# 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 
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 ) ∷ [])

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

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

這裏證明了純量 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 ) ∷ []) ++ ((Second , negsucc ) ∷ []))
    ＝⟨ η/-identifies-related-points ≋ I ⟩
  η/ ≋ [] ∎
  where
  I : ((Second , pos ) ∷ (Second , negsucc ) ∷ []) ≈ []
  I Meter    = refl
  I Kilogram = refl
  I Second   = refl

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

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

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

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan hiding (_+_)
open import MLTT.Maybe
open import MGS.MLTT using (has-decidable-equality)
open import Integers.Type
open import Integers.Addition

module ag-SPBG where

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 裡面的單位只有一種正確排列方式，我們可以幫單位附上順序，這個順序其實並不重要，只是需要有一個來確保 List 只有一種排列方法，從而去除因為排列順序不同而無法被定義等價認出來的不同表達方式（[A, B] 跟 [B, A] 兩種構造）

_<Unit_ : Unit → Unit → 𝓤₀ ̇
Meter    <Unit Meter    = 𝟘
Meter    <Unit Kilogram = 𝟙
Meter    <Unit Second   = 𝟙
Kilogram <Unit Meter    = 𝟘
Kilogram <Unit Kilogram = 𝟘
Kilogram <Unit Second   = 𝟙
Second   <Unit _        = 𝟘

<Unit-trans : (u v w : Unit) → u <Unit v → v <Unit w → u <Unit w
<Unit-trans Meter    Kilogram Second   _ _ = ⋆
<Unit-trans Meter    Kilogram Kilogram _ ()
<Unit-trans Meter    Kilogram Meter    _ ()
<Unit-trans Meter    Second   _        _ ()
<Unit-trans Kilogram Second   _        _ ()
<Unit-trans Meter    Meter    _        () _
<Unit-trans Kilogram Meter    _        () _
<Unit-trans Kilogram Kilogram _        () _
<Unit-trans Second   _        _        () _

data Tri (u v : Unit) : 𝓤₀ ̇ where
  is-< : u <Unit v → Tri u v
  is-≡ : u ＝ v → Tri u v
  is-> : v <Unit u → Tri u v

tri : (u v : Unit) → Tri u v
tri Meter    Meter    = is-≡ refl
tri Meter    Kilogram = is-< ⋆
tri Meter    Second   = is-< ⋆
tri Kilogram Meter    = is-> ⋆
tri Kilogram Kilogram = is-≡ refl
tri Kilogram Second   = is-< ⋆
tri Second   Meter    = is-> ⋆
tri Second   Kilogram = is-> ⋆
tri Second   Second   = is-≡ refl

單位定了順序之後，這裏規定 List 中的單位必須按照特定順序排列，確保每個組合單位的表示形式只有一種

data _<?_ : Maybe Unit → Unit → 𝓤₀ ̇ where
  no-bd : ∀ {u} → Nothing <? u
  bd    : ∀ {v u} → v <Unit u → Just v <? u

接著在 cons 中我們規定 ¬ (n ＝ pos 0) 因此不會出現 3 s⁰ 這種可以直接寫成 3 的情況

data UL (lb : Maybe Unit) : 𝓤₀ ̇ where
  []   : UL lb
  cons : (u : Unit) → lb <? u
       → (n : ℤ) → ¬ (n ＝ pos )
       → UL (Just u)
       → UL lb

Units : 𝓤₀ ̇
Units = UL Nothing

<?-trans : ∀ {lb u v} → lb <? u → u <Unit v → lb <? v
<?-trans no-bd      _   = no-bd
<?-trans (bd w<u)   u<v = bd (<Unit-trans _ _ _ w<u u<v)

weaken : ∀ {lb u} → lb <? u → UL (Just u) → UL lb
weaken bd' []                          = []
weaken bd' (cons v (bd u<v) n nz rest) = cons v (<?-trans bd' u<v) n nz rest

insert : ∀ {lb} (u : Unit) → lb <? u → (n : ℤ) → ¬ (n ＝ pos )
         → UL lb → UL lb
insert u ord n nz []                          = cons u ord n nz []
insert u ord n nz (cons v ord' m nz' rest)   with tri u v
... | is-< u<v     = cons u ord n nz (cons v (bd u<v) m nz' rest)
... | is-> v<u     = cons v ord' m nz' (insert u (bd v<u) n nz rest)
... | is-≡ refl    with ℤ-is-discrete (n + m) (pos )
...   | inl _      = weaken ord rest
...   | inr nz-sum = cons u ord (n + m) nz-sum rest

*-unit : ∀ {lb} → UL lb → Units → Units
*-unit []                   ys = ys
*-unit (cons u _ n nz rest) ys = insert u no-bd n nz (*-unit rest ys)

構造一些案例來看看這種實現

1m : Units
1m = cons Meter no-bd (pos ) (λ ()) []

1s : Units
1s = cons Second no-bd (pos ) (λ ()) []

1/s : Units
1/s = cons Second no-bd (negsucc ) (λ ()) []

對消就會得到純量

cancel : *-unit 1s 1/s ＝ []
cancel = refl

另外也嘗試證明比較複雜的案例

m³ : Units
m³ = cons Meter no-bd (pos ) (λ ()) []

1m³s : Units
1m³s =
  cons Meter no-bd (pos ) (λ ())
    (cons Second (bd ⋆) (pos ) (λ ()) [])

m³-×̇-1s : *-unit m³ 1s ＝ 1m³s
m³-×̇-1s = refl

這個方法的缺點是我們被迫仔細的構造構造子，構造複雜也難用，並創造了一個內容無關緊要的 strict order 與大量的輔助函數來處理這些問題。但比起另外兩個方案，這個方案並不需要 function extensionality，並且證明可以仰賴定義等價。

{-# 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 

單位相乘只需要把自己的指數相加即可

*-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 
1m _ = pos 

1s : Units
1s Second = pos 
1s _ = pos 

m³ : Units
m³ Meter = pos 
m³ _ = pos 

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 
1m³s Second = pos 
1m³s _ = pos 

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 版本相當。

對所有我們能夠想到儲存方式，但表示方式具有歧意的狀況，都可以用類似的方案解決。但方案三這種直接去找理想的 model 的做法不一定能成功，混用三種方案也是有可能的，熟悉理論的多種模型會對避免粗暴的使用方案一有很大的幫助。