2

我想把我对幺半群的定义分成多个部分：

  • 幺半群的签名
  • 幺半群定律，作为关系
  • 此关系中元素的相等见证

我目前的想法是这样做：

data MonoidSig A : Type → Type₁ where
  ε₀   : MonoidSig A A
  _⋄₀_ : MonoidSig A (A → A → A)

RawMonoid : Type → Type₁
RawMonoid A = ∀ {B} → MonoidSig A B → B

module _ {A : Type} (rawMonoid : RawMonoid A) where
  private
    ε = rawMonoid ε₀
    _⋄_ = rawMonoid _⋄₀_

  data MonoidLaw : A → A → Type where
    unit-l : ∀ x → MonoidLaw (ε ⋄ x) x
    unit-r : ∀ x → MonoidLaw (x ⋄ ε) x
    assoc  : ∀ x y z → MonoidLaw ((x ⋄ y) ⋄ z) (x ⋄ (y ⋄ z))

Lawful : ∀ {A} (raw : RawMonoid A) → Set
Lawful raw = ∀ {x y} → MonoidLaw raw x y → x ≡ y

Monoid : (AIsSet : isSet A) → Type₁
Monoid {A = A} AIsSet = Σ[ raw ∈ RawMonoid A ] (Lawful raw)

现在，我想为自由幺半群创建一个数据类型，作为由幺半群法则商的原始语法的商类型。但我还没有想出如何摆脱RawFreeMonoid下面的定义，并以MonoidSig某种方式实现它：

open import Cubical.HITs.SetQuotients

data RawFreeMonoid A : Type where
  ⟨_⟩ : A → RawFreeMonoid A
  ε   : RawFreeMonoid A
  _⋄_ : RawFreeMonoid A → RawFreeMonoid A → RawFreeMonoid A

rawFreeMonoid : (A : Type) → RawMonoid (RawFreeMonoid A)
rawFreeMonoid A ε₀ = ε
rawFreeMonoid A _⋄₀_ = _⋄_

FreeMonoid : Type → Type
FreeMonoid A = RawFreeMonoid A / MonoidLaw (rawFreeMonoid A)

所以这是我的问题：有没有办法以FreeMonoid这种方式定义，而无需手动写出RawFreeMonoidandrawFreeMonoid定义？

4

1 回答 1

2

好问题！您可以按如下方式进行（我更喜欢使用实际记录类型而不是指示性编码）：

open import Cubical.Data.List

record Signature : Type₁ where
  field
    Sort   : Type₀
    Symbol : (domain : List Sort) → (codomain : Sort) → Type₀

data Vector {A : Type₀} (B : A → Type₀) : List A → Type₀ where
  []  : Vector B []
  _∷_ : {x : A} {xs : List A} → B x → Vector B xs → Vector B (x ∷ xs)

module _ (Σ : Signature) where
  open Signature Σ
  data Term : Sort → Type₀ where
    _·_ : {dom : List Sort} {cod : Sort} → (f : Symbol dom cod) → Vector Term dom → Term cod

对于任何给定的签名 Σ，Term Σ将是自由的 Σ 结构。更准确地说，对于任何类型s的 Σ，类型Term Σ s将是 sort 项的类型s。

幺半群的签名可以定义如下：

open import Cubical.Data.Unit

data MonoidSymbol : List Unit → Unit → Type₀ where
  ε₀ : MonoidSymbol [] tt
  ⋄₀ : MonoidSymbol (tt ∷ tt ∷ []) tt

monoidSignature : Signature
monoidSignature = record { Sort = Unit; Symbol = MonoidSymbol }

编辑回应评论：你是对的，Term monoidSignature是免费的原始幺半群，而不是免费的幺半群。我在这里提出了构建商的代码。我相信在这段代码中，法律以您想要的方式指定：

-- `Structure` is defined in the linked code.
module _ (A : Structure monoidSignature) where
  open Structure A

  ε   = op ε₀
  _⋄_ = op ⋄₀

  data MonoidLaw : Carrier tt → Carrier tt → Type₀ where
    unitₗ : (x : Carrier tt) → MonoidLaw (ε ⋄ x) x
    unitᵣ : (x : Carrier tt) → MonoidLaw (x ⋄ ε) x
    assoc : (x y z : Carrier tt) → MonoidLaw ((x ⋄ y) ⋄ z) (x ⋄ (y ⋄ z))
于 2020-06-07T10:54:40.013 回答