> Point is that the above is a constructive definition, not just a
> postulate. I am also fine with |Define $\catx{K}$ to be s.t.|.

OK, I see your point. Define is maybe more clear here.