Draft: Binary coproducts

This shows that V0 has all binary coproducts. It also shows indirectly that V0 is closed under booleans. Closes issue issue #9

Currently this has way too many commits in it..