Commit 2026-03-16 11:24 15a45ed1

refactor(CategoryTheory/Sites): remove universe parameter from Functor.IsContinuous (#36459) The current definition of Functor.IsContinuous depends on a universe parameter t and says that F : C ⥤ D is continuous if precomposing with F.op preserves being a sheaf for presheaves with values in Type t. We show SGA 4 III 1.5, which says that if t is large enough such that both C and D are t-small, then being continuous for t implies being continuous for any universe t'. Using this, we drop the parameter from the definition and show it implies the old one.