Skip to content

Draft: Binary coproducts

Daniel Gratzer requested to merge hott/hott-set-theory:coproduct into master

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..

Merge request reports