Open claims about 2-element types #743
Description
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