Open claims about `2`-element types

[fredrik-bakke]

The following claims are waiting to be formalized in univalent-combinatorics.2-element-types:

• [ ] A map between 2-element types is an equivalence if and only if its image is the full subtype of the codomain
• [ ] A map between 2-element types is not an equivalence if and only if its image is a singleton subtype of the codomain
• [ ] Any map between 2-element types that is not an equivalence is constant
• [ ] Any map between 2-element types is either an equivalence or it is constant