[math-fun] The other kind of codimension