agda - 在不写出所有定律的情况下表示同态

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 而不 阐明同态定律？所以作为从见证 M : Monoid A 到 N : Monoid B 的某种映射，但这对我来说没有多大意义，因为它是一个“映射”，我们已经知道它应该将 M 映射到 N...

Answer 1

目前没有。但这就是最近论文的后续内容 A feature to unbundle data at will是关于。在 the repo对于这项工作，您会找到“package former”的来源； accompanying documentation使用 Monoid 作为其示例之一，2.17 节是关于同态生成的。

这个原型(prototype)的目的是找出需要(和可行)的特性，以指导元理论和“Agda 内部”实现的开发。