Представление гомоморфизмов без выписывания всех законов

Question

Предположим, у меня есть тип записи для некоторой алгебраической структуры; например, для моноидов:

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

Answer 1

В настоящее время нет. Но это то, о чем идет речь в продолжении недавней статьи "Функция разделения данных по желанию". В репозитории для этой работы вы найдете исходные коды для "прежнего пакета"; в сопроводительной документации используетсяMonoid как один из его примеров, а раздел 2.17 посвящен генерации гомоморфизмов.

Цель этого прототипа - выяснить, какие функции необходимы (и осуществимы), чтобы направлять разработку как метатеории, так и реализации "внутри Agda".