Read-back: arrow_theorem

Setup. Fix two arbitrary types: a type $A$ of alternatives and a type $\iota$ of voters. Three typeclass hypotheses are assumed:

• $A$ is finite (Fintype A);
• $\iota$ is finite (Fintype ι);
• $\iota$ is nonempty (Nonempty ι).

There is one explicit cardinality hypothesis: $|A| > 2$, i.e. there are strictly more than two alternatives (so at least $3$; combined with finiteness, $3 \le |A| < \infty$). No decidability assumption is used by the theorem (a DecidableEq ι hypothesis appears in the surrounding definition file, but only after the definitions this theorem uses, and the theorem statement itself does not carry it).

Throughout, a profile is any family $P = (P_i)_{i \in \iota}$ where each $P_i$ is a binary relation on $A$ (an arbitrary function $A \to A \to \mathrm{Prop}$; no properties are built into the type). The predicate "$P$ is a preference profile" means: for every voter $i$, the relation $P_i$ is a strict total order on $A$ in Mathlib's sense (IsStrictTotalOrder), i.e. $P_i$ is

• trichotomous: for all $a, b \in A$, $P_i\,a\,b$ or $a = b$ or $P_i\,b\,a$;
• irreflexive: for no $a$ does $P_i\,a\,a$ hold;
• transitive.

The object $F$. Let $F$ be any function taking a family of binary relations on $A$ (one per voter — not necessarily a preference profile; $F$ is total on all such families) and returning a single binary relation on $A$. Three hypotheses are assumed about $F$:

1. $F$ is a social welfare function (IsSWF F): for every preference profile $P$ (every $P_i$ a strict total order), the output relation $F(P)$ is itself a strict total order on $A$. Nothing is assumed about the value of $F$ on families that are not preference profiles.

2. Unanimity, in the constant-profile form (SWFUnanimity F): for every single relation $r$ on $A$ that is a strict total order, and for all $a, b \in A$,

That is: on a profile in which every voter holds the identical order $r$, the social order coincides exactly (as a biconditional on every ordered pair, including pairs with $a = b$) with $r$. This is the only form of unanimity assumed — it constrains $F$ only on constant profiles. It is not the Pareto condition: no assumption is made that unanimous agreement on a single pair $(a,b)$ within a non-constant profile forces $F(P)\,a\,b$.

3. Independence of irrelevant alternatives (SWFIIA F): for all preference profiles $P$ and $Q$ (both consisting of strict total orders) and all $a, b \in A$: if every voter $i$ satisfies $P_i\,a\,b \iff Q_i\,a\,b$ (agreement is required only on the single ordered pair $(a,b)$, not explicitly on $(b,a)$), then

Conclusion. There exists a voter $i \in \iota$ (plain existence — no uniqueness is claimed) who is a dictator in the following strong sense (SWFDictator F i): for every preference profile $P$ (every coordinate a strict total order) and all $a, b \in A$,

That is, on every preference profile the social order returned by $F$ is identical, pair by pair, to voter $i$'s own order — not merely that $i$'s strict preferences are respected in one direction, but a full biconditional on every ordered pair.

Edge cases made explicit.

• The hypotheses are non-vacuous only when strict total orders on $A$ exist and $\iota$ is inhabited; both are guaranteed here ($A$ finite hence linearly orderable, $\iota$ assumed nonempty). If $\iota$ were empty the conclusion $\exists i$ would be false, so Nonempty ι is load-bearing.
• With $|A| > 2$ the two-alternative case (where majority rule famously satisfies the analogous conditions) is excluded, as are $|A| \in \{0, 1\}$.
• All biconditionals quantify over all ordered pairs, including diagonal pairs $a = b$ (where irreflexivity forces both sides false) and both orientations $(a,b)$, $(b,a)$.
• $F$'s behavior on families that fail to be preference profiles is completely unconstrained by every hypothesis and by the conclusion.