Show that the map from a pointed `k+1`-element type to the complement of the point is an equivalence

[fredrik-bakke]

The following claim is waiting to be formalized in univalent-combinatorics.complements-isolated-points:

• [ ] The map from a pointed k+1-element type to the complement of the point is an equivalence