5 代数の最初の例

5.1 アロー関数

word(vs,(s,s))F … \(\mathsf{fn}\)
abbr … \(\lceil x \mapsto X \rfloor\) ≈ \(\mathsf{fn} ( x , X )\)
cvt … \(\lceil x \mapsto X \rfloor ( t )\) ≃ substitution(\(X\), \(x\) ↦ \(t\))

\(\mapsto\) の前のv-Formを \(\bullet\) に替えられます。その際 \(\bullet \mapsto\) は略されます。
例　 \(\lceil \bullet + a \rfloor\) ≈ \(\lceil x \mapsto x + a \rfloor\)
\([ \mathbin{p} ] :\mathsf{R} \Longleftrightarrow \lceil \bullet \rfloor \stackrel{\star}{\mathbin{p}} \lceil \bullet \rfloor\) \(\blacktriangleleft\) O

5.2 1項関数の性質

word+(s[s,s],p)R … \(:\underline{1}\)  \(:\mathsf{i}\)
lower … \(( X , [\mathbin{{\sf f}}] ) :\underline{1}\) ≃ \(\forall x \in X . \mathbin{{\sf f}} x \in X\)
lower … \(( X , [\mathbin{{\sf f}}] ) :\mathsf{i}\) ≃ \(\forall x \in X . \mathbin{{\sf f}} ( \mathbin{{\sf f}} x ) = x\)
\(( X , [ {f} ] ) :\underline{1} \Longleftrightarrow \stackrel{\text{^}}{{f}} X \subset X\) \(\blacktriangleleft\) O
\(( X , [ \lceil \bullet \rfloor ] ) :\underline{1}\mathsf{i}\) \(\blacktriangleleft\) O

5.3 2項関数の性質

word+(s[ss,s],p)R … \(:\underline{2}\)  \(:\mathsf{C}\)  \(:\mathsf{A}\)  \(:\mathsf{I}\)
lower … \(( X , [\mathbin{{\sf f}}] ) :\underline{2}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y \in X\)
lower … \(( X , [\mathbin{{\sf f}}] ) :\mathsf{C}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y = y \mathbin{{\sf f}} x\)
lower … \(( X , [\mathbin{{\sf f}}] ) :\mathsf{A}\) ≃ \(\forall x , y , z \in X . x \mathbin{{\sf f}} \, ( y \mathbin{{\sf f}} z ) = ( x \mathbin{{\sf f}} y ) \mathbin{{\sf f}} z\)
lower … \(( X , [\mathbin{{\sf f}}] ) :\mathsf{I}\) ≃ \(\forall x \in X . x \mathbin{{\sf f}} x = x\)
\(( X , [ \mathbin{f} ] ) :\underline{2} \Longleftrightarrow X \stackrel{\text{^^}}{\mathbin{f}} X \subset X\) \(\blacktriangleleft\) O

word+(s[ss,s],c) … \(\text{unit}\)
lower … \(\text{unit} ( X , [\mathbin{{\sf f}}] )\) ≃ \(\{ e \mid \forall x \in X . e \mathbin{{\sf f}} x = x = x \mathbin{{\sf f}} e \}\)

5.4 べき集合

word(s,s) … \(\wp\)
℘. … \(\wp X = \{ A \mid A \subset X \}\)
wp0 … \(\wp \emptyset = \{ \emptyset \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
wp1 … \(\wp \{ x \} = \{ \emptyset , \{ x \} \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

\(( \wp X , [\cup] ) :\underline{2}\mathsf{C}\mathsf{A}\mathsf{I}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(( \wp X , [\cap] ) :\underline{2}\mathsf{C}\mathsf{A}\mathsf{I}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(\emptyset \in \text{unit} ( \wp X , [\cup] )\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(X \in \text{unit} ( \wp X , [\cap] )\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(( \wp X , [ \lceil X \mathop\setminus \bullet \rfloor ] ) :\underline{1}\mathsf{i}\) \(\blacktriangleleft\) \(\mathbb{W}.\)