Codomain as part of the definition of a function

TL;DR I don't think you need one to describe a function, but I think you need a codomain to define a function.

(The original iteration)

However, in set theory, the definition of function as a binary relation (i.e. a subset 𝑅 of $𝐴×𝐵$) does not include its codomain

Sure it does, you just did it: it's $B$. You can't specify ordered pairs without mentioning $B$. What does $(a,b)$ even mean if you don't know what set $b$ is from? (Edit: Of course you can build an ordered pair with two arbitrary sets. What I wanted to express, but failed to make clear, is that to use comprehension to select ordered pairs it would be necessary to mention $B$. The discussion is in the commentary to Arthur's comment below.)

It's not entirely unnatural to discern based on codomains

Also, $(𝑎,𝑏)$ does mean something if, for example, we change $𝐵$ to a larger set, and this does not affect $𝑅$.

This is part of the "is the codomain a part of the function?" question. I would say it is not so clear that it "does not affect $R$."

In Mac Lane's formulation of category theory, for example, each arrow has two associated objects of categories: the domain, and the codomain. This definition allows two technically different arrows which otherwise might be "the same function" to have different codomains, one properly containing the other.

Now look what happens when we define extensions of functions: say that we have a function $R\subseteq A\times B$ and a function $S\subseteq C\times D$ where $A\subseteq C$ and $B\subseteq D$. We say that $S$ extends $R$ if $R(a)=S(a)$ for every $a\in A$.

Of course, if $A=C$ the "bigger codomain" is just a special case of extension. From this viewpoint one can avoid confusing $R$ with its extension $S$, although for all intents and purposes we usually think of them as being the same thing "with different codomain."

While Mac Lane's formulation of category theory is largely independent of set theory, I think the mindset above is a thing in set theory too.

Regarding Arthur's comment:

A set $𝑅$ of ordered pairs where each element of 𝐴 appears exactly once as the first element of a pair" avoids the mention of anything like a codomain.

I will concede that this is a description of a function, but I would argue it does not allow one to define a function. (I'm operating under ZF only.)

Think about what it would take to try to define a function using this description. You have in hand, we suppose, the sets that will be elements of the domain and the sets that will be their images. For each assignment $a\mapsto b$, you can form $\{\{a\},\{a,b\}\}$ using the axiom of pairing, no problem.

But now you need something to pull all of these into a single set that is your set of ordered pairs. But how does one do that? I do not believe the axiom of comprehension can handle this$^\ast$. As the wiki notes, "the axiom schema of specification can only construct subsets". I think attempting to pull all the pairs into a single set would amount to using unrestricted comprehension, which is of course not safe.

A thought experiment

What I'm trying to get at is that to realize functions as sets, picking a codomain seems as necessary as specifying a domain.

How about we double-down on the logic that the codomain can be done away with completely with this thought experiment: if one believes that a function doesn't need a codomain, should we also believe that a partial function don't need a domain specified either? It's just "a set of ordered pairs, period." Is the domain not meaningful because we can extend it at will?

$^\ast$ (With a finite domain, you might be able to combine pairing, powerset and union to assemble them into a set, but of course I want to discuss infinite domains too.)