Generalization of Lawvere's fixed point for a bijection between $A$ and $(A\to B)\to B$ At the end of his paper about the set semantics of System F, Reynolds produces two sets $A,B$ and a bijection between $A$ and $(A\to B)\to B$. He concludes "since $(A\to B)\to B$ and $A$ are well-known to have different cardinalities, we have a contradiction". This last statement is not constructive.
We can finish Reynolds' proof with classical logic as follows. From the bijection between $(A\to B)\to B$ and $A$, deduce a surjection $A \twoheadrightarrow (A\to B)$. By Lawvere's fixed point theorem, any function $f:B\to B$ then has a fixed point. By hypothesis, $B$ has at least two different elements $x,y$. By the excluded middle principle, an arbitrary element of $B$ is either equal to $x$, or different. We then have a function $f:B\to B$ such as $f(x)=y$ and $f(z)=x$, for all $z$ different from $x$. This $f$ has no fixed point, which is our contradiction.
Constructively we have to stop at the Lawvere step, which is interesting already : any function $f:B\to B$ has a fixed point. However, the definition of the surjection $A \twoheadrightarrow (A\to B)$ does not seem constructive either (as far as I have tried). Is there a generalization of Lawvere's fixed point theorem when there is a bijection between $A$ and $(A\to B)\to B$ ? What can we constructively deduce about $B$ in that case ? I would like to show that $B$ is as close as possible to a singleton, which is called proof irrelevance in type theory.
 A: The first step of your reasoning here is faulty. We can't get a surjection from $A$ onto $A → B$ from Reynolds' bijection. At least, it would be big news, because by the rest of your argument, it would mean that System F is not consistent, which in turn would mean either that some widely believed/imitated proofs are actually faulty, or something like ZF had proved a contradiction.
Your Lawvere argument is why "negative" inductive types are problematic to have in a type theory. They allow a $T$ such that $T \cong A^T$, which quickly leads to looping terms in $A$ via a translation of Lawvere's argument. However, System F does not let you define these "negative" types. It only has fixed points of "positive" operations like $A^{A^-}$. That is positive due to being, "double negative," but it is still positive.
The reasoning behind Reynolds' last step is that there is no bijection $A → Ω^{Ω^A}$, where $Ω$ is the set of truth values. This holds even constructively. The classical aspect is taking $2$, the booleans, to be the set of truth values. This is a definable type in System F, so in a classical set theoretic semantics Reynolds' type would need to be interepreted as a fixed point of the double power set operator, which doesn't exist.
However, constructively, $2^A$ is not the power set of $A$, but the decidable subsets of $A$, and there can be fixed points of $2^{2^-}$. The obvious counterpoint to the Reynolds paper is "Polymorphism is Set Theoretic Constructively." But for instance this article might be a little simpler to think about as an introduction, and leads to the idea that you can have a situation where $ℕ \cong 2^{2^ℕ}$ constructively (also, check the comments for a link to a paper on this being the case for classical topological spaces).
