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.

[fredrik-bakke]

(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.)

Is there an established higher version of tight apartness relations? I.e. tight apartness for 1-types or even untruncated types?

[djspacewhale]

If there is I'm not familiar with it. It should be a useful theory however for e.g. deloopings of apartness groups.