Hashes

Hashes are represented as bitstrings: 
Digest Hash : Type
Digest = ByteString
Hash   = ByteString
Digestable types are collected under a appropriate typeclass: 
record Digestable (A : Type) : Type where
  field digest     : A → Digest
        digest-inj : Injective≡ digest
We assume an injective hash function and ways to digest base types: 
record HashAssumptions : Type₁ where
  field
    -- how to digest base types
    instance
      Digestable-ℕ   : Digestable ℕ
      Digestable-ℕ×ℕ : Digestable (ℕ × ℕ)
      Digestable-H×ℕ : Digestable (Hash × ℕ)

    -- agreed-upon hash function (e.g. SHA256)
    hash     : Digest → Hash
    hash-inj : Injective≡ hash

  infix 100 _♯
  _♯ : ⦃ Digestable A ⦄ → A → Hash
  _♯ = hash ∘ digest

  ♯-inj : ⦃ _ : Digestable A ⦄ → Injective≡ {A = A} _♯
  ♯-inj = digest-inj ∘ hash-inj

Signatures

Let’s start with various aliases for bitstrings and key pairs: 
Key Signature PublicKey PrivateKey : Type
Key        = ByteString
Signature  = ByteString
PublicKey  = Key
PrivateKey = Key

record KeyPair : Type where
  constructor mk-keyPair
  field publicKey  : PublicKey
        privateKey : PrivateKey
open KeyPair public
We then assume that there is a way to sign (hashable) values, as well as the existence of a suitable signature verification algorithm (e.g. SHA256). 
record SignatureAssumptions : Type₁ where
  field
    verify-signature : PublicKey → Signature → Hash → Bool
    sign : ⦃ Digestable A ⦄ → Key → A → Signature