Representing homomorphisms without writing all laws out

Question

Suppose I have a record type for some algebraic structure; e.g. for monoids:

{-# OPTIONS --cubical #-}

module _ where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything hiding (assoc)

record Monoid {ℓ} (A : Type ℓ) : Type ℓ where
  field
    set : isSet A

    _⋄_ : A → A → A
    e : A

    eˡ : ∀ x → e ⋄ x ≡ x
    eʳ : ∀ x → x ⋄ e ≡ x
    assoc : ∀ x y z → (x ⋄ y) ⋄ z ≡ x ⋄ (y ⋄ z)

Then I can manually create a type for monoid homomorphisms:

record Hom {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} (M : Monoid A) (N : Monoid B) : Type (ℓ-max ℓ ℓ′) where
  open Monoid M renaming (_⋄_ to _⊕_)
  open Monoid N renaming (_⋄_ to _⊗_; e to ε)
  field
    map : A → B
    map-unit : map e ≡ ε
    map-op : ∀ x y → map (x ⊕ y) ≡ map x ⊗ map y

But is there a way to define Hom without spelling out the homomorphism laws? So as some kind of mapping from the witness M : Monoid A to N : Monoid B, but that doesn't make much sense to me because it'd be a "mapping" where we already know that it should map M to N...

Answer 1

There currently isn't. But that's what the follow up to the recent paper A feature to unbundle data at will is about. In the repo for that work, you'll find the sources for 'package former'; the accompanying documentation uses Monoid as one of its examples, and section 2.17 is all about homomorphism generation.

The aim of this prototype is to figure out what features are needed (and feasible), to guide the development of both the meta-theory and an 'inside Agda' implementation.