PS

Free theorem vs. existential

圏論 Haskell

Free theorem

ある種の体系では、naturalityが常に成立するという(ことを含む)定理。
このnaturalityをfree naturalityと勝手に呼ぶことにする。

命題

Functor $F : \mathcal{J} \rightarrow \mathcal{Hask}$ について、product:

$\forall F \approx \lbrace (\sigma _ a) _ {a \in \mathcal{J} } \mid {} ^ {\forall} a,\ \sigma _ a \in Fa \rbrace$

に関してfreely naturalならば、coproduct:

$\exists F \approx \bigcup\limits _ {a} \lbrace (x, a) \mid x \in Fa \rbrace$

に関してもfreely natural。

証明

まず、

$\forall _ a (Fa \rightarrow b) \cong (\exists F \rightarrow b)$

次に、 $\forall$ に関するfree naturalityにより、

${} ^ {\forall} c \in \mathcal{Hask}, c \cong \forall _ b \big( (c \rightarrow b) \rightarrow b \big)$

ここで、

$\Diamond F = \forall _ b \big(\forall _ a (Fa \rightarrow b) \rightarrow b \big)$

と定義すると、

- $\cong \forall _ b \big( (\exists F \rightarrow b) \rightarrow b \big)$
- $\cong \Diamond F$

しかも、これは $F$ についてnaturalとなる。

系

$\exists F$ へのinjection:

$i _ a : Fa \rightarrow \exists F$
$i _ a(x) = (x, a)$

はfreely naturalとなり、Colimits in sets - PSと同様にすると、 colimiting coconeになる。

$\exists F \cong \text{colim } F$

しかも、これは $F$ についてnaturalとなる。

参考文献