集合の要素と大域要素
圏論の記法
定義
任意の集合$ x （ 圏$ \mathbf{Set} における対象）について
要素$ \bar x \in x に対応する大域要素（写像）を
$ \bar x_♯\colon 1_\mathbf{Set} → x
$ \colon * \mapsto \bar x
と書くことにする
シャープ格上げの縦向きバージョン
性質
写像の適用
写像$ f\colon x→y について
$ (f(\bar x))_♯ = (\bar x;;f)_♯ = \bar x_♯ ;f
写像の図式順適用