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

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

3 голосов
/ 05 октября 2019

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

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

1 Ответ

3 голосов
/ 06 октября 2019

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

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

...