おーそうだったのかぁ、と思いつつ、ふと疑問が。…（Xは任意の型） はどうなるのでしょう？
状況からして、直積、直和があってそれぞれに単位元1、0があるような圏を考える訳ですよね。
こっからは当て推量ですけど、strictな言語なら となって欲しいと思うので、直感的には
(
は同型）となりそうな気がするんだけれど、これってつまり、distributive law が成り立つと言う状況で。
でも、確かこないだの圏論勉強会で「MLのようなstrictな言語の圏ではdistributive lawは成り立たない」みたいな話をしてた気が*1。…あや？違うのかなぁ。謎。
※いつものごとく豪快に勘違いをしている可能性大アリなので、そんときゃ許してくださいませ。
*1:うろ覚えなので正確さを欠いているかもしれません。というか多分不正確。
