My suggestion has quite some overlap with other comments and also @gowers answer:

Let $A$, $B$ be two sets. An **explicit bijection** between $A$ and $B$ is a deterministic algorithm taking elements of $A$ as input and for which outputs are elements of $B$, such that an analysis of the algorithm yield its bijectivity.

Several notes:

In most cases I have been looking at, the sets $A$ and $B$ were finite.

A typical way of satisfying this criterion is to provide two deterministic algorithms $A \to B$ and $B \to A$ and showing that they are inverses of each other. Or showing that both are injective. I would also call this "explicit" though one might need to slightly reword to include this situation.

I did not include anything about complexity of the algorithm because I do not think its actual computation time is relevant for it being "explicit".

I have often seen the following relaxation, namely that one knows already that $|A| = |B|$, and only deduces injectivity or surjectivity from the algorithm. The problem with this relaxation is that it would allow just listing the elements of both sets...

My suggestion has quite some overlap with other comments and also @gowers answer:

Let $A$, $B$ be two sets. An **explicit bijection** between $A$ and $B$ is a deterministic algorithm taking elements of $A$ as input and for which outputs are elements of $B$, such that an analysis of the algorithm yield its bijectivity.

Several notes:

In most cases I have been looking at, the sets $A$ and $B$ were finite.

A typical way of satisfying this criterion is to provide two deterministic algorithms $A \to B$ and $B \to A$ and showing that they are inverses of each other. Or showing that both are injective. I would also call this "explicit" though one might need to slightly reword to include this situation.

I did not include anything about complexity of the algorithm because I do not think its actual computation time is relevant for it being "explicit".

I have often seen the following relaxation, namely that one knows already that $|A| = |B|$, and only deduces injectivity or surjectivity from the algorithm.

My suggestion has quite some overlap with other comments and also @gowers answer:

Let $A$, $B$ be two sets. An **explicit bijection** between $A$ and $B$ is a deterministic algorithm taking elements of $A$ as input and for which outputs are elements of $B$, such that an analysis of the algorithm yield its bijectivity.

Several notes:

In most cases I have been looking at, the sets $A$ and $B$ were finite.

A typical way of satisfying this criterion is to provide two deterministic algorithms $A \to B$ and $B \to A$ and showing that they are inverses of each other. Or showing that both are injective. I would also call this "explicit" though one might need to slightly reword to include this situation.

I did not include anything about complexity of the algorithm because I do not think its actual computation time is relevant for it being "explicit".

I have often seen the following relaxation, namely that one knows already that $|A| = |B|$, and only deduces injectivity or surjectivity from the algorithm. The problem with this relaxation is that it would allow just listing the elements of both sets...