Comment by jounker

Doesn’t this break down with dependent type systems?