PS

Colimits for free

圏論 Limit Haskell

以下、Limits for free - PSのdual。

Cocones for free

Functor F : \mathcal{J} \rightarrow \mathcal{Hask} のcoproduct:

  • \exists F \approx \bigcup _ {a} \lbrace (x, a) | x \in Fa \rbrace

について、function:

  • r : c \leftarrow \exists F

を F のcocone for freeと勝手に呼ぶことにする。
これは、以下のcategoryにより F のcoconeと本質的に等しい。

Cocone category for free

  • f : c \leftarrow c', f \circ r' = r

なる f をcocone for free間のmorphismとするcategory:

  • \mathcal{CoconeF}(F)

を作れる。これは、

  • (c \leftarrow \exists F) \cong \forall _ a (c \leftarrow Fa)

とfree naturalityにより、cocone category \mathcal{Cocone}(F) とisomorphic。

Colimits for free

Free naturalityにより、Colimits in sets - PSと同様にして、injection:

  • i _ a : \exists F \leftarrow Fa
  • i _ a(x) = (x, a)

は F のcolimiting coconeになる:

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

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

また、明らかに、identity function:

  • 1 _ {\exists F} : \exists F \rightarrow \exists F

は、colimiting cocone for free(initial cocone for free)になる。

これらは本質的に等しい。