mbps https://blog.hatena.ne.jp/mbps/ PS https://mbps.hatenablog.com/ 圏論 Haskell Free theorem ある種の体系では、naturalityが常に成立するという(ことを含む)定理。 このnaturalityをfree naturalityと勝手に呼ぶことにする。 命題 Functor について、product: に関してfreely naturalならば、coproduct: に関してもfreely natural。 証明 まず、 次に、 に関するfree naturalityにより、 ここで、 と定義すると、 しかも、これは についてnaturalとなる。 系 へのinjection: はfreely naturalとなり、Colimits in sets - PS… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmbps.hatenablog.com%2Fentry%2F2014%2F04%2F06%2F140430" title="Free theorem vs. existential - PS" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> http://chart.apis.google.com/chart?cht=tx&chl=%20%5Ccoprod%5Climits_a%20F%28a%29%20%3D%20%5Cbigcup_%7Bc%7D%20%5Cbig%7B%20%28x%2C%5C%20c%29%5C%20%7C%5C%20%20x%20%5Cin%20F%28c%29%20%5Cbig%7D%20 Hatena Blog https://hatena.blog 2014-04-06 14:04:30 rich https://mbps.hatenablog.com/entry/2014/04/06/140430 1.0 100%