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

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

Answer 1

目前没有。但这就是最近论文 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 使用 Monoid 作为示例之一的后续内容，而第 2.17 节是关于同态生成的。

此原型的目的是找出需要（和可行）的特征，以指导元理论和 'inside Agda' 实现的发展。

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

Representing homomorphisms without writing all laws out

agda

homomorphism

cubical-type-theory

homotopy-type-theory