Определение группы, полугруппы, моноида ...

[Geen]

iifat в сообщении #1281708 писал(а):

зачем в понятие группы включается множество?

А вот зачем, кстати?

[arseniiv]

(Кстати о единице моноида в сигнатуре и вне её)

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

$$\Sigma(A:\mathcal U)\; A\times A\to A,$$

его элементы — всевозможные пары из некоторого типа из вселенной $\mathcal U$ и бинарной операции на нём.

Тип полугрупп можно записать как

$$\Sigma(A:\mathcal U)\; \Sigma({\circ}:A\times A\to A)\; \mathsf{assoc}(A,{\circ}),$$

где

$$\mathsf{assoc}(A,{\circ})\equiv\Pi(a,b,c:A)\; a\circ(b\circ c) = (a\circ b)\circ c$$

— тип всевозможных доказательств ассоциативности $\circ$ (функций, для любой тройки элементов $A$ предъявляющих свидетельство равенства $a\circ(b\circ c)$ и $(a\circ b)\circ c$). Сам тип полугрупп состоит из троек (тип, операция, свидетельство ассоциативности).

И тип моноидов можно представить как

$$\Sigma(A:\mathcal U)\; \Sigma({\circ}:A\times A\to A)\; \mathsf{assoc}(A,{\circ})\times\mathsf{hasNeutral}(A,{\circ}),$$

где $\mathsf{hasNeutral}(A,{\circ})$ — тип доказательств того, что у $\circ$ есть нейтральный элемент. Переводя соответствующую аксиому побуквенно, получим

$$\mathsf{hasNeutral}(A,{\circ})\equiv\Sigma(e:A)\; \Pi(a:A)\; (a\circ e = a)\times(e\circ a = a).$$

Элементы этого типа — пары из элемента $e:A$ и свидетельства того, что это действительно нейтральный элемент (в виде функции, для каждого $a:A$ выдающей пару из свидетельств равенств $a\circ e$ и $e\circ a$ самому $a$). Так что, внимание, с одной стороны у нас аксиома с $\exists$, а с другой — единица в сигнатуре (она входит в этот большой кортеж, который является элементом описанного типа моноидов)!

(Для наглядности можно даже взять изоморфный этому тип

$$\Sigma(A:\mathcal U)\; \Sigma({\circ}:A\times A\to A)\; \Sigma(e:A)\; \mathsf{assoc}(A,{\circ})\times\mathsf{isNeutral}(A,{\circ},e),$$

части кортежа-элемента которого просто немного переставлены; $\mathsf{isNeutral}(A,{\circ},e)\equiv \Pi(a:A)\; (a\circ e = a)\times(e\circ a = a)$.)