Transporting families that cover the terminal object

Covering families on arbitrary sites can be transported through equivalences whose forward functors preserve covers. This is site-theoretic infrastructure and does not require sheaves or a geometric realization of either site.

theorem CategoryTheory.GrothendieckTopology.CoversTop.map_equivalence {C D : Type u} [Category.{u, u} C] [Category.{u, u} D] {J : GrothendieckTopology C} {K : GrothendieckTopology D} {I : Type u_1} {U : I → C} (hU : J.CoversTop U) (e : C ≌ D) : CoverPreserving J K e.functor → K.CoversTop fun (i : I) => e.functor.obj (U i)

An equivalence whose forward functor preserves covers sends a family covering the terminal object to a family covering the terminal object.