nLab A-set

Definition

An affine set or antithesis set or $\mathcal{A}$-set is a setoid $(A, \sim)$ with an irreflexive symmetric relation $\nsim$ such that the equivalence relation satisfies the principle of substitution for the irreflexive symmetric relation in both variables: for all $x$, $y$, and $z$ in $A$,

$$(x \sim y) \to ((x \nsim z) \to (y \nsim z)) \quad \mathrm{and} \quad (x \sim y) \to ((z \nsim x) \to (z \nsim y))$$

In addition,

• An $\mathcal{A}$-set is strong if $\nsim$ is an apartness relation.

• An $\mathcal{A}$-set is affirmative if $\neg (x \sim y)$ implies $x \nsim y$.

• An $\mathcal{A}$-set is refutative if $\neg (x \nsim y)$ implies $x \sim y$.

• An $\mathcal{A}$-set is stable if it is both affirmative and refutative.

• An $\mathcal{A}$-set is decidable if $x \sim y$ or $x \nsim y$.

Thus, every setoid is an affirmative $\mathcal{A}$-set.

In dependent type theory, an $\mathcal{A}$-set is a univalent $\mathcal{A}$-set if the canonical inductively defined function $\mathrm{idtosim}(x, y)$ from $x =_A y$ to $x \sim y$ is an equivalence of types for all $x$ and $y$ in $A$. This means that univalent $\mathcal{A}$-sets are the same as h-sets equipped with an irreflexive symmetric relation, since the principle of substitution is automatically satisfied via transport across the type families $(-) \nsim z$ and $z \nsim (-)$ for all $z$ in $A$.

Using the type of affine propositions

An affine proposition $P$ is interpreted as a pair $(P^+, P^-)$ of propositions in intuitionistic logic which are mutually exclusive in that $\neg (P^+ \wedge P^-)$ holds. Thus, we can define the type of affine propositions as the type

$$\Omega_\pm \coloneqq \sum_{P^+:\Omega} \sum_{P^-:\Omega} \neg (P^+ \wedge P^-) =_\Omega \top$$

where $\Omega$ is the type of all propositions. We denote the two projection functions of the above type as $(-)^+:\Omega_\pm \to \Omega$ and $(-)^-:\Omega_\pm \to \Omega$. In addition, we usually suppress the witness that $\neg (P^+ \wedge P^-)$ and denote elements of $\Omega_\pm$ as pairs $(P^+, P^-)$. The logical operations for the affine logic can be defined on $\Omega_\pm$ as demonstrated here. We denote affine truth by $1:\Omega_\pm$ and affine falsehood by $0:\Omega_\pm$, to contrast with intuitionistic truth $\top:\Omega$ and falsehood $\bot:\Omega$

An $\mathcal{A}$-set is a type $A$ with an affine equivalence relation, a function $\mathrm{Eq}:A \times A \to \Omega_\pm$ with witnesses that

• for all $x:A$, $\mathrm{Eq}(x, x)$

$$\mathrm{refl}_\mathrm{Eq}:\prod_{x:A} \mathrm{Eq}(x, x) =_{\Omega_\pm} 1$$

• for all $x:A$ and $y:A$, $\mathrm{Eq}(x, y)$ implies $\mathrm{Eq}(y, x)$

$$\mathrm{sym}_\mathrm{Eq}:\prod_{x:A} \prod_{y:A} \mathrm{Eq}(x, y) \multimap \mathrm{Eq}(y, x) =_{\Omega_\pm} 1$$

• for all $x:A$, $y:A$, and $z:A$, $\mathrm{Eq}(x, y)$ multiplicatively and $\mathrm{Eq}(y, z)$ implies $\mathrm{Eq}(x, z)$

$$\mathrm{trans}_\mathrm{Eq}^{\boxtimes}:\prod_{x:A} \prod_{y:A} \prod_{z:A} \mathrm{Eq}(x, y) \boxtimes \mathrm{Eq}(y, z) \multimap \mathrm{Eq}(x, z) =_{\Omega_\pm} 1$$

An $\mathcal{A}$-set is

• strong if for all $x:A$, $y:A$, and $z:A$, $\mathrm{Eq}(x, y)$ additively and $\mathrm{Eq}(y, z)$ implies $\mathrm{Eq}(x, z)$

$$\mathrm{trans}_\mathrm{Eq}^{\sqcap}:\prod_{x:A} \prod_{y:A} \prod_{z:A} \mathrm{Eq}(x, y) \sqcap \mathrm{Eq}(y, z) \multimap \mathrm{Eq}(x, z) =_{\Omega_\pm} 1$$

• affirmative if for all $x:A$ and $y:A$, $\mathrm{Eq}(x, y)$ is affirmative

$$\mathrm{aff}_\mathrm{Eq}:\prod_{x:A} \prod_{y:A} \mathrm{Eq}(x, y) =_{\Omega_\pm} !\mathrm{Eq}(x, y)$$

• refutative if for all $x:A$ and $y:A$, $\mathrm{Eq}(x, y)$ is refutative

$$\mathrm{ref}_\mathrm{Eq}:\prod_{x:A} \prod_{y:A} \mathrm{Eq}(x, y) =_{\Omega_\pm} ?\mathrm{Eq}(x, y)$$

• stable if for all $x:A$ and $y:A$, $\mathrm{Eq}(x, y)$ is stable

$$\mathrm{stab}_\mathrm{Eq}:\prod_{x:A} \prod_{y:A} !\mathrm{Eq}(x, y) =_{\Omega_\pm} ?\mathrm{Eq}(x, y)$$

• decidable if for all $x:A$ and $y:A$, $\mathrm{Eq}(x, y)$ is decidable

$$\mathrm{dec}_\mathrm{Eq}:\prod_{x:A} \prod_{y:A} \mathrm{Eq}(x, y) \sqcup \mathrm{Eq}(x, y)^\bot =_{\Omega_\pm} 1$$

An $\mathcal{A}$-set is a univalent $\mathcal{A}$-set if the canonical inductively defined function $\mathrm{idtoeq}^+(x, y)$ from $x =_A y$ to $\mathrm{El}(\mathrm{Eq}(x, y)^+)$ is an equivalence of types for all $x$ and $y$ in $A$. Univalent $\mathcal{A}$-sets are just h-sets with an irreflexive symmetric relation.

Examples

Every type is an affirmative $\mathcal{A}$-set with the equivalence relation given by the propositional truncation of the identity type and the irreflexive symmetric relation given by the negation of the equivalence relation.

• A-monoid

• A-group

• A-ring

In ring theory

Every nontrivial commutative ring $R$ is an $\mathcal{A}$-set with the equivalence relation given by equality and the irreflexive symmetric relation given by $(y - x)$ being an invertible element. In addition,

• $R$ is a strong $\mathcal{A}$-set if and only if $R$ is a local ring,

• $R$ is a strong affirmative $\mathcal{A}$-set if and only if $R$ is a Kock field,

• $R$ is a strong refutative $\mathcal{A}$-set if and only if $R$ is a Heyting field

• $R$ is a strong decidable $\mathcal{A}$-set if and only if $R$ is a discrete field

More generally, let $R$ be a nontrivial commutative ring and let $M$ be a multiplicative subset of $R$ such that $-1 \in M$ and $\neg (0 \in M)$. Then $R$ is an $\mathcal{A}$-set with the equivalence relation given by equality and the irreflexive symmetric relation given by $(y - x) \in M$.

Related concepts

• setoid

• irreflexive symmetric relation

• antithesis interpretation

• antithesis partial order

• A-function

• cartesian product of A-sets

• tensor product of A-sets

References

• Michael Shulman, Affine logic for constructive mathematics. Bulletin of Symbolic Logic, Volume 28, Issue 3, September 2022. pp. 327 - 386 (doi:10.1017/bsl.2022.28, arXiv:1805.07518)