Category and homotopy theoretic methods in set theory I am looking for applications of category theory and homotopy theory in set theory and particularly in cardinal arithmetics. "Applications" in the broad sense of the word --- this would include theorems, definitions, questions, points of view (and papers) in set theory that could be motivated or understood with help of category theory and homotopy theory. I am aware of some applications of set theory in category theory, e.g. large cardinal axioms (Vopenka principle) are used to construct localisations in homotopy theory, but this is not what I am asking for. However, I would be interested to hear if Vopenka principle is equivalent to a statement in category or homotopy theory.
The reason for the question is that I am trying to better understand this sketch of an attempt to understand an invariant in PCF theory in terms of homotopy theory. I am most interested in applications to cardinal arithmetic.
 A: You could look at algebraic set theory. For a general outline of how set theory, categories and type theory interact, see Steve Awodey's "From sets, to types, to categories, to sets". I don't know about direct connections between set theory and homotopy theory, but there is certainly a rich connection between type theory and homotopy theory, for example:

*

*https://arxiv.org/abs/0906.4521v1

*https://arxiv.org/abs/1007.4638

*https://arxiv.org/abs/0803.4349
Also possibly relevant is:

*

*https://arxiv.org/abs/0711.1529
Let me also mention that Vladimir Voevodsky has taken interest in connections between homotopy theory and foundations, see his page.
But I should say that all this (recent!) work is just laying the ground for what you seem to be asking for, namely further insights about set theory by means of category theory.
A: Peter Freyd wrote a paper, "The Axiom of Choice," in which he used topos-theoretic methods to prove that the axiom of choice is independent of (classical) Zermelo-Fraenkel set theory.  Unlike earlier topos-versions of set-theoretic independence proofs, Freyd's construction does not merely provide a category-theoretic view of a model that had already been considered by set theorists.  His models can be obtained by set-theoretic forcing methods (by another result of Freyd, in "All topoi are localic"), but those particular forcing constructions had not been considered until Andre Scedrov and I analyzed them (in "Freyd's models for the independence of the axiom of choice").  So I think it's fair to say that these models were a contribution from category theory to set theory.  
A: There is an interaction between category theory and set theory. In 1965, one year after Cohen's proof of the independence of the continuum hypothesis, Vopenka gave a proof using sheaf theory, see

*

*Kenneth Kunen, "[Omnibus Review]", The Journal of Symbolic Logic, 34 Issue 3 (1969) pp. 515 - 516, DOI: https://doi.org/10.2307/2270953
This is nowadays systematized in the topos theoretic interpretation of set theory, for which you should look up MacLane/Moerdijk, as Dylan Wilson pointed out. The authors give a proof of the independence of the continuum hypothesis.
Marta Bunge has given a topos theoretic proof of the independence of the Suslin hypothesis from ZFC in:

*

*Marta Bunge, Topos Theory and Souslin's Hypothesis. J.Pure & Applied Algebra 4 (1974) 159-187, https://doi.org/10.1016/0022-4049(74)90020-6.

As for the reformulation of Vopenka's principle: It is equivalent to the statement that a locally presentable category can not have a large full discrete subcategory. This, and more, is nicely explained in Adamek/Rosicky's Locally Presentable and Accessible Categories
On the other hand I know of no worked out connection between homotopy theory and set theory, just the indirect one via type theory mentioned by Andrej.
