我可以从这种签名类型制作原始数据类型吗？

Question

我想将对等分体的定义分成多个部分：

• monoid的签名
• 有关等分法则
• 具有这种关系的元素的平等见证

我目前的想法是像下面这样：

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)

现在，我想为免费的monoid创建一个数据类型，作为由monoid定律所引用的原始语法的商类型。但是我还没有弄清楚如何摆脱下面的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，而无需手工写出RawFreeMonoid和rawFreeMonoid定义？

Answer 1

很好的问题！您可以按以下方式进行操作（我更喜欢使用实际记录类型而不是强制性编码）：

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将是种类s的项的类型。
monoid的签名可以定义如下：
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是免费的原始monoid，而不是免费的monoid。我放置了用于构造商here的代码。我相信在此代码中，将以您想要的方式指定法律：
-- `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))