対
word(ss,s)! …【\(\langle {\sf X} , {\sf Y} \rangle\)】対の定義はされません。次のものは対の成分を取り出します。
word(s,s) … \({\rfloor}\) \({\lfloor}\)
\({\rfloor.}\)【\({\rfloor} \langle x , y \rangle = x\)】
\({\lfloor.}\)【\({\lfloor} \langle x , y \rangle = y\)】
\(\text{%0}\)【\(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\)】◀ \({\rfloor.}\)\({\lfloor.}\)
直積、関係
word(cc,c) … \(\times\)def …【\({\sf C} \times {\sf D}\)】≃【\(\{ \langle {\sf x} , {\sf y} \rangle \mid {\sf x} \in {\sf C} , {\sf y} \in {\sf D} \}\)】
word(ss,s) … \(\times\)
\(\times.\)【\(X \times Y = X \times Y\)】
\(\text{Set}^2\)【\(\widehat{\times} \text{Set} = \{ x \mid x = \langle {\rfloor} x , {\lfloor} x \rangle \} \)】◀ \({\rfloor.}\)\({\lfloor.}\)
対の集まりは関係とよばれます。
word(,c) … \(\text{Rel}\)
def …【\(\text{Rel}\)】≃【\(\{ {\sf R} \mid {\sf R} \subset \widehat{\times} \text{Set} \} \)】
abbr …【\(\langle {\sf p} \rangle\)】≈【\(\{ \langle {\sf x} , {\sf y} \rangle \mid {\sf x} \, {\sf p} \, {\sf y} \}\)】
word(ss,p)と関係は等価です。\({\sf X} {\sf p} {\sf Y} \Longleftrightarrow \langle {\sf X} , {\sf Y} \rangle \in \langle {\sf p} \rangle\)
写像
word(c,p)F … \(\text{Map}\)def …【\(\text{Map}\)】≃【\(\{ {\sf R} \in \text{Rel} \mid \forall {\sf x} ! {\sf y} \langle {\sf x} , {\sf y} \rangle \in {\sf R} \}\)】
word(vs,c)R … \(\lambda\)
def …【\(\lambda {\sf x} \, {\sf X}\)】≃【\(\{ \langle {\sf x} , {\sf X} \rangle \mid {\sf x} \in \text{Set} \}\)】
word(s,s)と写像は等価です。\({\sf f} {\sf X} = {\sf Y} \Longleftrightarrow \langle {\sf X} , {\sf Y} \rangle \in \lambda {\sf x} \, {\sf f} {\sf x}\)
abbr …【\( \lambda {\sf x} {\sf A} . {\sf X} \)】≈【\(\{ \langle {\sf x} , {\sf X} \rangle \mid {\sf x} {\sf A} \}\)】
lmd はその前が { で { } 内に . を含めば補助単語です。
word(,c)F … \(\text{id}\)
def …【\(\text{id}\)】≃【\(\lambda {\sf x} \, {\sf x}\)】
\(\text{Id0}\)【\(\text{id} = \langle = \rangle\)】
定義域、値域
word(c,c)F … \(\text{dom}\) \(\text{rng}\)def …【\(\text{dom} ( {\sf R} )\)】≃【\(\{ {\sf x} \mid \exists {\sf y} \, \langle {\sf x} , {\sf y} \rangle \in {\sf R} \} \)】
def …【\(\text{rng} ( {\sf R} )\)】≃【\(\{ {\sf y} \mid \exists {\sf x} \, \langle {\sf x} , {\sf y} \rangle \in {\sf R} \} \)】
word(s,s)F … \(\text{dom}\) \(\text{rng}\)
\(\text{dom.}\)【\(\text{dom} ( R ) = \text{dom} ( R )\)】
\(\text{rng.}\)【\(\text{rng} ( R ) = \text{rng} ( R )\)】
成分の入れ替え
word(s,s) … \(^\leftrightarrow\)\(\text{sw.}\)【\(\langle x , y \rangle ^\leftrightarrow = \langle y , x \rangle\)】
word(c,c) … \(^\leftrightarrow\)
def …【\({\sf R} ^\leftrightarrow\)】≃【\(\{ {\sf p} ^\leftrightarrow \mid {\sf p} \in {\sf R} \}\)】
word(s,s) … \(^\leftrightarrow\)
\(\text{Psw.}\)【\({\sf R} ^\leftrightarrow = {\sf R} ^\leftrightarrow\)】