« Home

單位乘法通用化 [ag-4AP1]

用 Agda 實現單位正確的算術 的 *-unit 其實可以進一步通用化，我們只關心拿來當單位的類型是不是有可判定的相等，所以程式可以寫成

{-# OPTIONS --safe --without-K #-}
module ag-4AP1 where

open import MLTT.Spartan hiding (_+_)
open import MLTT.List
open import MGS.MLTT using (has-decidable-equality)
open import Integers.Type
open import Integers.Addition
open import ag-OW40

generalized-_-unit : {A : 𝓤 ̇ }
  → has-decidable-equality A
  → List (A × ℤ) → List (A × ℤ) → List (A × ℤ)
generalized-_-unit {_}{A} dec us₁ us₂ = foldr step us₁ us₂
  where
  step : A × ℤ → List (A × ℤ) → List (A × ℤ)
  step (u , n) [] = (u , n) ∷ []
  step (u , n) ((v , m) ∷ xs) with dec u v
  ... | inr _ = (v , m) ∷ step (u , n) xs
  ... | inl _ with ℤ-≟ (n + m) (pos 0)
  ...   | inl _ = xs
  ...   | inr _ = (u , n + m) ∷ xs