The statement "The monotonicity of B means that ..." is not precise enough. (For example, the identity mapping, the mapping defined by B(V) = V for any V, is monotone, but iteration of it does not converge to the set of SPE payoff profiles.)
Other (minor) comments I typed yesterday but which disappeared:
In Step 2, (1 - delta) is missing in the IC constraints.
In Step 2, the last two two elements in b should be the right hand side of the second inequality in 3). Delete the ) after underline_w_i there.
The pictures would look better if drawn with equal aspect ratio.
Maybe better to connect the vertices in the pictures of the payoff profile sets.
max_x c^T x should be min_x c^T x: in the code, the linear program is set up as a minimization problem.
This pull request is work in progress. It is jointly being finished with https://github.com/QuantEcon/Games.jl/pull/19.
There are several comments from @oyamad on this gist. I will include them below for completeness.