直観主義の命題って開集合だっけ閉集合だっけ→□がcomonadで開核もcomonadだから開集合だな、みたいな雑思考パターン