diff options
author | Gregor Kleen <gkleen@yggdrasil.li> | 2017-11-14 10:12:08 +0100 |
---|---|---|
committer | Gregor Kleen <gkleen@yggdrasil.li> | 2017-11-14 10:12:08 +0100 |
commit | 95e42853b901d0f1d6cdbbfd9d50521fd0e38068 (patch) | |
tree | dd014786b16f490adaac3122ba6282e33d62510b /edit-lens/src/Control/Lens/Edit.lhs | |
parent | ad4b28878104d82d26d65d110f082c7d1c20c617 (diff) | |
download | incremental-dfsts-95e42853b901d0f1d6cdbbfd9d50521fd0e38068.tar incremental-dfsts-95e42853b901d0f1d6cdbbfd9d50521fd0e38068.tar.gz incremental-dfsts-95e42853b901d0f1d6cdbbfd9d50521fd0e38068.tar.bz2 incremental-dfsts-95e42853b901d0f1d6cdbbfd9d50521fd0e38068.tar.xz incremental-dfsts-95e42853b901d0f1d6cdbbfd9d50521fd0e38068.zip |
Cat-T corrections
Diffstat (limited to 'edit-lens/src/Control/Lens/Edit.lhs')
-rw-r--r-- | edit-lens/src/Control/Lens/Edit.lhs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs index 973f409..29b34ce 100644 --- a/edit-lens/src/Control/Lens/Edit.lhs +++ b/edit-lens/src/Control/Lens/Edit.lhs | |||
@@ -23,7 +23,7 @@ module Control.Lens.Edit | |||
23 | \end{code} | 23 | \end{code} |
24 | 24 | ||
25 | \begin{defn}[Moduln] | 25 | \begin{defn}[Moduln] |
26 | Ein Modul $M$ ist eine \emph{partielle Monoidwirkung} zusammen mit einem initialen Element (bzgl. der Monoidwirkung) auf dem Träger, d.h. $M = (\Dom M, \partial M, \init_M)$ ist ein Tupel aus einer Trägermenge $\Dom M$, einem Monoid $\partial M$ zusammen mit mit einer partiellen Funktion $\cdot \colon \Dom M \times \partial M \to \Dom$, die \emph{kompatibel} ist mit der Monoid-Struktur: | 26 | Ein Modul $M$ ist eine \emph{partielle Monoidwirkung} zusammen mit einem schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (bzgl. der Monoidwirkung) auf dem Träger, d.h. $M = (\Dom M, \partial M, \init_M)$ ist ein Tupel aus einer Trägermenge $\Dom M$, einem Monoid $\partial M$ zusammen mit mit einer partiellen Funktion $\cdot \colon \Dom M \times \partial M \to \Dom$, die \emph{kompatibel} ist mit der Monoid-Struktur: |
27 | 27 | ||
28 | \begin{itemize} | 28 | \begin{itemize} |
29 | \item $\forall m \in \Dom M \colon m \cdot 1_{\partial M} = m$ | 29 | \item $\forall m \in \Dom M \colon m \cdot 1_{\partial M} = m$ |
@@ -32,7 +32,7 @@ Ein Modul $M$ ist eine \emph{partielle Monoidwirkung} zusammen mit einem initial | |||
32 | 32 | ||
33 | und einem Element $\init_M \in \Dom M$, sodass gilt: | 33 | und einem Element $\init_M \in \Dom M$, sodass gilt: |
34 | 34 | ||
35 | $$ \forall m \in \Dom M \ \exists \partial m \in \partial M \colon m = \init_M \cdot m^\prime $$ | 35 | $$ \forall m \in \Dom M \ \exists \partial m \in \partial M \colon m = \init_M \cdot \partial m$$ |
36 | 36 | ||
37 | Wir führen außerdem eine Abbildung $(\init_M \cdot)^{-1} \colon \Dom M \to \partial m$ ein, die ein $m$ auf ein arbiträr gewähltes $\partial m$ abbildet für das $\init_M \cdot \partial m = m$ gilt. | 37 | Wir führen außerdem eine Abbildung $(\init_M \cdot)^{-1} \colon \Dom M \to \partial m$ ein, die ein $m$ auf ein arbiträr gewähltes $\partial m$ abbildet für das $\init_M \cdot \partial m = m$ gilt. |
38 | 38 | ||
@@ -56,7 +56,7 @@ class Monoid m => Module m where | |||
56 | \end{code} | 56 | \end{code} |
57 | \end{defn} | 57 | \end{defn} |
58 | 58 | ||
59 | Wir weichen von der originalen Definition von Moduln aus \cite{hofmann2012edit} darin ab, dass wir für das ausgezeichnete Element $\init_X$ des Trägers explizit (und konstruktiv) fordern, dass es ein initiales Element bzgl. der Monoidwirkung sei. | 59 | Wir weichen von der originalen Definition von Moduln aus \cite{hofmann2012edit} darin ab, dass wir für das ausgezeichnete Element $\init_X$ des Trägers explizit (und konstruktiv) fordern, dass es ein schwach-initiales Element bzgl. der Monoidwirkung sei. |
60 | 60 | ||
61 | \begin{comment} | 61 | \begin{comment} |
62 | \begin{defn}[Modulhomomorphismen] | 62 | \begin{defn}[Modulhomomorphismen] |