表示同态而不写出所有定律

Question

假设我有一个代数结构的记录类型;例如，对于幺半群：

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

然后我可以手动为幺半群同态创建一个类型：

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

但是有没有办法在不详细说明同态定律的情况下定义Hom呢？因此，作为从见证人到N : Monoid B的某种映射M : Monoid A，但这对我来说没有多大意义，因为它将是一个"映射"，我们已经知道它应该将M映射到N......

Answer 1

目前没有。但这就是最近论文《随意解绑数据的功能》的后续内容。 在该工作的存储库中，您将找到"包成型者"的来源;随附的文档使用Monoid作为其示例之一，第 2.17 节是关于同态生成的。

这个原型的目的是弄清楚需要哪些功能(和可行(，以指导元理论和"内部Agda"实现的发展。