Can I make a raw datatype from this kind of signature type?

Question

I'd like to split up my definition of monoids into multiple parts:

• The signature of monoids
• The monoid laws, as a relation
• Witnesses of equality for elements that are in this relation

My current idea is to do it like the following:

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)

Now, I'd like to make a datatype for free monoids as a quotient type of raw syntax quotiented by the monoid laws. But I haven't figured out how to get rid of the RawFreeMonoid definition below, and make it from MonoidSig somehow:

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)

So that is my question: is there a way to define FreeMonoid in this way, without writing out by hand the RawFreeMonoid and rawFreeMonoid definitions?

Answer 1

Nice question! You can do it as follows (where I prefer to use an actual record type instead of an impredicative encoding):

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

For any given signature Σ, Term Σ will then be the free Σ-structure. More precisely, for any sort s of Σ, the type Term Σ s will be the type of terms of sort s.

The signature for monoids can be defined as follows:

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 }

Edit in response to the comment: You are right, Term monoidSignature is the free raw monoid, not the free monoid. I put up code for constructing the quotient here. I believe that in this code, the laws are specified in the way you want:

-- `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))