Did Gödel possess a proof of the independence of $\mathsf{AC}$?

Question

We all know Gödel proved the consistency of the Axiom of Choice with $\mathsf{ZF}$ using his constructible universe, and Cohen proved the consistency of $\neg \mathsf{AC}$ using his new method of forcing some thirty years later. In the excellent book Zermelo's Axiom of Choice by G.H. Moore, there is the following footnote p.283 :

A tantalizing question is whether Gödel had previously found a proof for the independence of the Axiom. Speaking in 1966, on the occasion of Cohen's receipt of the Fields Medal for his independence proofs, Alonzo Church expressed one view : "Gödel [...] in 1942 found a proof of the independence of the axiom of constructibility in type theory. According to his own statement (in a private communication), he believed that this could be extended to an independent proof of the axiom of choice; but due to a shifting of his interests toward philosophy, he soon afterwards ceased to work in this area, without having settled its main problems. The partial result mentioned was never worked out in full detail or put into form for publication". Hao Wang expressed a second view in an article which Gödel approved for publication in 1976 or 1977 : "It was in 1943 when Gödel arrived at a proof of the independence of the axiom of choice in the framework of (finite) type theory. The idea of the proof makes it clear why the proof works. For that reason alone, it would be of interest to reconstruct the proof. It uses intensional considerations. The interpretation of the logical connectives is changed. A special topology has to be chosen. The method looked promising toward getting also the independence of $\mathsf{CH}$. But Gödel developed a distaste for the work. [...] He now regrets that he did not continue the work. If he had continued with it, he would probably have gotten the independence of $\mathsf{CH}$ by 1950, and the development of set theory would have progressed faster".

Moore then adds that John Addison told him in personal communication that Gödel said he didn't want to publish his proof by "fear of leading set-theoretic research in the wrong direction".

My main questions are the following :

1. Except for those quotes, is there any tangible trace of such a proof obtained by Gödel?
2. What does it mean to obtain the independence of $\mathsf{AC}$ in finite type theory? Does it imply in any way independence with $\mathsf{ZF}$? I know the independence of $\mathsf{AC}$ with $\mathsf{ZFA}$ had been obtained by Fraenkel-Mostowski, but at the time it wasn't known how to transfer this independence to $\mathsf{ZF}$.
3. Did anyone later work out the details of such an independence proof?
4. (Very speculative) If Gödel had indeed obtained such a proof and published it, would it really have advanced the development of set theory that much? We may have never gotten forcing from Cohen if the question of the independence of $\mathsf{CH}$ was already settled in the 50's.

Answer 1

Q1: Except for those quotes, is there any tangible trace of such a proof obtained by Gödel?

Gödel commented on his independence results in a letter dated June 30, 1967 to W. Rautenberg. In his reply (in German, translated here), Gödel confirmed what Church had stated:

In reply to your inquiry I would like to refer to the presentation of the facts that Professor Alonzo Church gave in his lecture at the last International Congress of Mathematicians. Mostowski's assertion _{[that Gödel, about 1940, had obtained most of Cohen's independence results]}is incorrect insofar as I was merely in possession of certain partial results, namely, of proofs for the independence of the axiom of constructibility and of the axiom of choice in type theory. Because of my highly incomplete records from that time, _{[entries in volumes 1 and 15 of his Arbeitshefte from Summer 1942]} I can only reconstruct the first of these two proofs without difficulty. My method had a very close connection with that recently developed by Dana Scott and had less connection with Cohen's method. I never obtained a proof for the independence of the continuum hypothesis from the axiom of choice, and I found it very doubtful that the method that I used would lead to such a result.