3

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

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

4

1 回答 1

4

目前没有。但这就是最近论文A feature to unbundle data at will的后续内容。在该工作的 repo中，您会找到“package forms”的来源；随附的文档用作Monoid其示例之一，第 2.17 节是关于同态生成的全部内容。

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

于 2019-10-06T12:20:59.837 回答