antisubalgebra

constructive mathematics, realizability, computability propositions as types, proofs as programs, computational trinitarianism In constructive mathematics, we often do algebra by equipping an algebra with a tight apartness (and requiring the algebraic operations to be strongly extensional), in the sense of ring with tight apartness. In this context, it is convenient to replace subalgebras with anti-subalgebras, which classically are simply the complements of subalgebras. Let us work in the...