Limits for free

以下、category $\mathcal{J}$ と $\mathcal{Hask}$ (的なもの) にて、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$

について、function:

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

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

を作れる。これは、

とfree naturalityにより、cone category $\mathcal{Cone}(F)$ とisomorphic。

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

は $F$ のlimiting coneになる:

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

また、明らかに、identity function:

は、limiting cone for free(terminal cone for free)になる。

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