Могу ли я сделать необработанный тип данных из этого типа подписи? - PullRequest
Новая
       66

Могу ли я сделать необработанный тип данных из этого типа подписи?

0 голосов
/ 10 октября 2019

Я хотел бы разделить мое определение моноидов на несколько частей:

  • Подпись моноидов
  • Законы моноидов как отношение
  • Свидетели равенства для элементов, которые находятся в этом отношении

Моя текущая идея состоит в том, чтобы сделать это следующим образом: 

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 таким образом, без выписывания от руки определений RawFreeMonoid и rawFreeMonoid?

...