昔デデキント切断による実数型を作れないか考えたことある。