Spahn setoid

References

The formalization of Bishop set is reviewed for instance in section 3 of