Two weeks ago a conference was held on precisely the topic
of your question, the Workshop on Set Theory and the
Philosophy of
Mathematics
at the University of Pennsylvania in Philadelphia. The
conference description was:
Hilbert, in his celebrated address to the Second International
Congress of Mathematicians held at Paris in 1900, expressed the
view that all mathematical problems are solvable by the application
of pure reason. At that time, he could not have anticipated the fate
that awaited the first two problems on his list of twenty-three,
namely, Cantor's Continuum Hypothesis and the problem of the consistency
of an axiom system adequate to develop real analysis. The Gödel
Incompleteness Theorems and the Gödel-Cohen demonstration of the
independence of CH from ZFC make clear that continued confidence in
the unrestricted scope of pure reason in application to mathematics
cannot be founded on trust in its power to squeeze the utmost from
settled axiomatic theories which are constitutive of their respective
domains. The goal of our Workshop is to consider the extent to which it
may be possible to frame new axioms for set theory that
both settle the Continuum Hypothesis and satisfy reasonable
standards of justification. The recent success of set
theorists in establishing deep connections between large
cardinal hypotheses and hypotheses of definable determinacy
suggests that it is possible to find rational justification
for new axioms that far outstrip the evident truths about
the cumulative hierarchy of sets, first codified by Zermelo
and later supplemented and refined by others, in their
power to settle questions about real analysis. The Workshop
will focus on both the exploration of promising
mathematical developments and on philosophical analysis of
the nature of rational justification in the context of set
theory.
Speakers included Hugh Woodin, Justin Moore, John Burgess,
Aki Kanamori, Tony Martin, Juliette Kennedy, Harvey
Friedman, Andreas Blass, Peter Koellner, John Steel, James
Cummings, Kai Hauser and myself. Bob Solovay also attended.
Several speakers have made their slides available on the
conference page, and I believe that they are organizing a
conference proceedings volume.
Without going into any details, let me say merely that in
my own talk (slides
here) I argued
against the position that there should be a unique theory
as in your question, by outlining the case for a multiverse
view in set theory, the view that we have multiple distinct
concepts of set, each giving rise to its own set-theoretic
universe. Thus, the concept of set has shattered into
myriad distinct set concepts, much as the ancient concepts
of geometry shattered with the discovery of non-euclidean
geometry and the rise of a modern geometrical perspective.
On the multiverse view, the CH question is a settled
question---we understand in a very deep way that the CH and
$\neg$CH are both dense in the multiverse, in the sense
that we can easily obtain either one in a forcing extension
of any given universe, while also controlling other
set-theoretic phenomenon. I also gave an argument for why
the traditionally proposed template for settling CH---where
one finds a new natural axiom that implies CH or that
implies $\neg$CH---is impossible.
Meanwhile, other speakers gave arguments closer to the
position that you seem to favor in your question. In
particular, Woodin described his vision for the Ultimate L,
and you can see his slides.
In as far as we regard forcing as forming internal sheaves, the question is asking how to say "internal category of sheaves" in homotopy type theory.
It is expected that this works in directed analogy with the situation in ordinary type theory by considering internal sites, except that there is a technical problem currently not fully solved: in homotoy type theory an internal category is necessarily an internal (infinity,1)-category and in order to say this one needs to be able to say "(semi-)simplicial object in the homotopy type theory". This might seem immediate, but is a little subtle, due to the infinite tower of higher coherences involved. For truncated internal categories one might proceed "by hand" as indicated here. A general formalization has recently been proposed by Voevodsky -- see the webpage UF-IAS-2012 -- Semi-simplicial types -- but this definition does not in fact at the moment work in homotopy type theory. (Last I heard was that Voevodsky had been thinking about changing homotopy type theory itself to make this work. But this is second-hand information only, we need to wait for one of the IAS-HoTT fellows to see this here and give us first-order news on this.)
However, that all said, there is something else which one can do and which does work: if an $\infty$-topos is equipped with a notion of (formally) étale morphisms, then one can speak about internal sheaves over the canonical internal site of any object without explicitly considering the internal site itself: the "petit (infintiy,1)-topos" of sheaves on a given object $X \in \mathbf{H}$ is the full sub-(oo,1)-category of the slice over $X$ on the (formally) étale maps
It may seem surprising on first sight, but this can be saiD in homotopy type theory and it can be said naturally and elegantly:
For this we simply add the axioms of differential cohesive homotopy type theory to plain homotopy type theory. This means that we declare there to be two adjoint triples of idempotent (co)monadic modalities called
shape modality $\dashv$ flat modality $\dashv$ sharp modality
and
reduction modality $\dashv$ infinitesimal shape modality $\dashv$ infinitesimal flat modality .
Using this we say: a function is formally étale if its naturality square of the unit of the "infinitesimal shape modality" is a homotopy pullback square. Then we have available in the homotopy type theory the sub-slice over any $X$ on those maps that are formally étale. This is internally the $\infty$-topos of $\infty$-stacks over $X$, hence the "forcing of $X$" in terms of the standard interpretation of forcing as passing to sheaves.
What I just indicated is discussed in detail in section 3.10.4 and 3.10.7 of the notes
Differential cohomology in a cohesive $\infty$-topos
( http://ncatlab.org/schreiber/show/differential+cohomology+in+a+cohesive+topos )
For more details on the above axioms of cohesive homotopy type theory see the first section of my article with Mike Shulman:
Quantum gauge field theory in Cohesive homotopy type theory
( http://ncatlab.org/schreiber/show/Quantum+gauge+field+theory+in+Cohesive+homotopy+type+theory )
Best Answer
Here are some resources:
HoTT.v.