Sets の Completeness できた

集合と射の圏 Sets が Limit を持つっていう奴なんですが、なかなかできなくて。Product と Equalizer は割とはやく片付いたんだが。

6月ぐらいに Stack overflow に投げて諦めてたんですが、

　　8月に解答が付いていた

のに10月になってから気がつきました。

やっぱり、Heterogenous Equality を使うんだが、λ式を避けるとできるらしい。

そこから、また少しすったもんだはしたんですが、結果的には Heterogenous Equality の Functional Extensionallity と Irrelevance を書いてやるとできました。

3月ぐらいから、はまっていたので、ちょっとうれしいです。

https://stackoverflow.com/questions/44456608/two-fields-record-congruence-in-agda