the time has come in the class i'm teaching about type theory where i go "so we're doing dependent types now. everything i have told you is either a lie or a massive oversimplification."