表題の事実は、長／ジェイコブスの以下の論文の p.11 Proposition 3.10 として記述されています。 Title: Disintegration and Bayesian Inversion via String Diagrams Authors: Kenta Cho, Bart Jacobs Submitted: 29 Aug 2017 (v1), 8 Feb 2019 (v3) Pages…

デカルト閉圏では、単純型理論とラムダ計算が気持ちよく出来ます。が、実用上、もう少し広い範囲の型 -- 依存型と再帰的型も扱えたほうがいいですね。依存型と再帰的型も扱えて、手で触れる感じ（あくまで“感じ”）の圏を考えましょう。内容： 実用上必要そう…