The Multiverse: Logical Modularity for Proof Assistants. - Kenji Maillard; Nicolas Margulies; Matthieu Sozeau; Nicolas Tabareau; Éric Tanter (CoRR, 2021)