PS

(Co)Ends for free

圏論 Haskell End

Free dinaturalityのもと、difunctor $S : \mathcal{C} ^ {\text{op}} \times \mathcal{C} \rightarrow \mathcal{Hask}$ について･･･

Ends for free

Limits for free - PSと同様にして、projection:

$\pi _ c : \forall _ d S(d, d) \rightarrow S(c, c)$
$\pi _ c(\sigma) = \sigma _ c$

は、 $S$ のending wedgeになる:

$\forall _ d S(d, d) \simeq \displaystyle\int _ d S(d, d)$

このending wedgeは、identity function:

$1 _ {\forall _ d S(d, d)} : \forall _ d S(d, d) \rightarrow \forall _ d S(d, d)$

と本質的に等しい。

Coends for free

Colimits for free - PSと同様にして、injection:

$i _ c : S(c, c) \rightarrow \exists _ d S(d, d)$
$i _ c(x) = (x, c)$

は、 $S$ のcoending cowedgeになる:

$\exists _ d S(d, d) \cong \displaystyle\int ^ d S(d, d)$

これはidentity function:

$1 _ {\exists _ d S(d, d)} : \exists _ d S(d, d) \rightarrow \exists _ d S(d, d)$

と本質的に等しい。