On: In Further Praise of Dependent Types

[icen]

You can specify the 2-vectors on the unit circle as "{ (x, y) : x, y in R | x^2 + y^2 - 1 < 0.000001 }" instead.