Agdaでは、postulateで与えられた A : Set に対し、f : A -> Boolを定義した際、任意の t: A にたいし、 : Bool （ただし xがtに登場することを とここでは表記している）を定義することが出来ない。構成的型理論としては当たり前だけれど、やっぱり不便だ。

朝は雨、昼には止むが依然として湿度が高い。出勤して会議とコーディング。ひさびさにKtさんに質問、構成主義の不便さと、Agdaの"magic with"構文がAgdaに読んでもらえないケースの話について。再度コーディングしていたら、読書会の時間に間に合わなくなる。…