「依存積型」と「依存和型」に関しては、もうサンザンだよー、あったく‥‥（昨日の記事「依存型と総称型の圏論的解釈」の冒頭を参照）ふんとに「依存ナントカ型」って紛らわしいよねぇ。それで、「依存ナントカ型」と言うのはやめます。 なんかまた間違える混…