    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of digits and digit expansions
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Data.Digit using (digitChars; Digit; showDigit; toDigits)
    import Data.Char.Properties as Char
    open import Data.Nat.Base using (ℕ)
    open import Data.Nat.Properties using (_≤?_)
    open import Data.Fin.Properties using (inject≤-injective)
    open import Data.Product.Base using (_,_; proj₁)
    open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
    import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Unique
    open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)
    open import Relation.Nullary.Decidable.Core using (True; from-yes; ¬?)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
    open import Function.Base using (_∘_)

    module Data.Digit.Properties where

    digitCharsUnique : Unique digitChars
    digitCharsUnique = from-yes (allPairs? (λ x y → ¬? (x Char.≟ y)) digitChars)

    module _ (base : ℕ) where
      module _ {base≥2 base≥2′ : True (2 ≤? base)} where
        toDigits-injective : ∀ n m → proj₁ (toDigits base {base≥2} n) ≡ proj₁ (toDigits base {base≥2′} m) → n ≡ m
        toDigits-injective n m eq with toDigits base {base≥2} n | toDigits base {base≥2′} m
        toDigits-injective ._ ._ refl | _ , refl | ._ , refl = refl

      module _ {base≤16 base≤16′ : True (base ≤? 16)} where
        showDigit-injective : (n m : Digit base) → showDigit {base} {base≤16} n ≡ showDigit {base} {base≤16′} m → n ≡ m
        showDigit-injective n m = inject≤-injective _ _ n m ∘ Unique.lookup-injective digitCharsUnique _ _