Reflective global subuniverses

[fredrik-bakke]

• Defines
  • Extensions of types in (global) subuniverses
  • Universal property of localizations at global subuniverses
  • Localizations at global subuniverses
  • Reflective global subuniverses
  • Functoriality of localizations
• Proves
  • Essential uniqueness of localizations at global subuniverses
  • Closure of localizations under dependent products, exponentials, retracts, pullbacks, products, identity types, equivalence types
  • Computation of cartesian products of localizations
  • Dependent precomposition equivalence for localizations
  • Closure of null types under dependent sums

[fredrik-bakke]

This work is cut short again because I need to prioritize other work, but it should be easy enough to pick up where this PR leaves off, for instance defining Σ-closed reflective global universes. In particular, it should be simple enough to show that reflective global subuniverses are in correspondence with orthogonal factorization systems using the infrastructure in orthogonal-factorization-systems.orthogonal-maps.