  Proof assistants play a dual role as programming languages and logical
systems. As programming languages, proof assistants offer standard modularity
mechanisms such as first-class functions, type polymorphism and modules. As
logical systems, however, modularity is lacking, and understandably so:
incompatible reasoning principles -- such as univalence and uniqueness of
identity proofs -- can indirectly lead to logical inconsistency when used in a
given development, even when they appear to be confined to different modules.
The lack of logical modularity in proof assistants also hinders the adoption of
richer programming constructs, such as effects. We propose the multiverse, a
general type-theoretic approach to endow proof assistants with logical
modularity. The multiverse consists of multiple universe hierarchies that
statically describe the reasoning principles and effects available to define a
term at a given type. We identify sufficient conditions for this structuring to
modularly ensure that incompatible principles do not interfere, and to locally
restrict the power of dependent elimination when necessary. This extensible
approach generalizes the ad-hoc treatment of the sort of propositions in the
Coq proof assistant. We illustrate the power of the multiverse by describing
the inclusion of Coq-style propositions, the strict propositions of Gilbert et
al., the exceptional type theory of P\'edrot and Tabareau, and general
axiomatic extensions of the logic.

Logic in Computer Science;Programming Languages