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

假设我有一些代数结构的记录类型；例如对于幺半群:

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

最佳答案

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

该原型(prototype)的目的是找出需要(和可行)哪些功能，以指导元理论和“内部 Agda”实现的开发。

关于agda - 在不写出所有定律的情况下表示同态，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/58249413/