「型理論のコロン、ターンスタイル、カンマ」への追記ですが別記事にします。ターンスタイルをオーバーロードすることの弊害は、（ターンスタイルに限らないけど）ターンスタイルが表す複数の意味がゴッチャになりがちなことです。もちろん、区別できる人は…

昨日の記事「記号のグリフと使用場面・使用意図： 型理論、圏論、集合論、論理など」より： なんでそこまでコロンとターンスタイルにこだわるのか？ 僕にはちょっと意味不明です。...[snip]...僕の個人的感想としては、型理論独自の記法をやめて、圏論と集合…