Target: apartness algebras and their antisubalgebras

[djspacewhale]

For roughly the same reason as topologists like, say, Hausdorff groups, constructive algebraists like working with gadgets where the underlying set has a tight apartness relation. Examples in nature include RR^n and profinite groups such as Cantor space. As discussed at the nlab page on antisubalgebras, the more useful notion in such contexts is of an "antisubalgebra" rather than a subalgebra, again for roughly the same reason as topologists like closed subalgebras.

(Note 1: such work is only relevant to set-level algebra, as types with a tight relation are automatically sets; constructive higher algebra promises to be much trickier and likely out of the range of current technology without rapid progress in modal lands.)

This is potentially a lot of routine work but good ethical practice, then, to define the apartness-versions of groups, rings, modules, etc along with their antisubalgebras. Such work would be useful for investigating and formalizing further constructive algebra and promises to be a good onboarder for the budding constructive algebraist.