Comment by andreabedini

Yes, that’s the whole point of dependent types: types can depend on (runtime) values.