I think it was "value judgement" (dependent types allow dispatching over a value in the type system)