PS

Relation lifting

圏論 定義 命題 Parametricity

Functorが絡んだときのparametricityの求め方。

以下、 \mathcal{Set} において･･･

Image

  • \mathsf{image}(a : A \to A') := \lbrace a(x) \mid x \in A \rbrace \subseteq A'

Relation

  • \mathcal{A} : A \Leftrightarrow A' \iff \mathcal{A} \subseteq A \times A'

Graph

  • \mathsf{graph}(a : A \to A') := \lbrace (x, a(x)) \mid x \in A \rbrace : A \Leftrightarrow A'

Relation lifting

Endofunctor:

  • F : \mathcal{Set} \to \mathcal{Set}

に対応する、relation間のmapping*1を

  • \mathcal{F}(\mathcal{A} : A \Leftrightarrow A') := \mathsf{image}\big( F\mathcal{A} \overset{F(\subseteq)}{\longrightarrow} F(A \times A') \overset{\langle F\pi _ A, F\pi _ {A'} \rangle}{\longrightarrow} FA \times FA' \big) : FA \Leftrightarrow FA'

と定義する。

命題

特に、関数:

  • a : A \to A'

に対応するrelation:

  • \mathcal{A} = \mathsf{graph}(a) : A \Leftrightarrow A'

について、

  • \mathcal{F}\mathcal{A} = \mathsf{graph}(Fa : FA \to FA')

証明

参考文献

*1:必ずしもfunctorialにはならないらしい。identityはpreserveする(と思う)

*2: \pi _ A \circ \subseteq はisoなのでimageは等しい