CoversTop in over-categories #
This file contains a transitivity lemma for GrothendieckTopology.CoversTop: if a family
X : I → C covers the top for J, and for each i a family Y i covers the top for the
induced topology on Over (X i), then the combined family covers the top for J.
theorem
CategoryTheory.GrothendieckTopology.CoversTop.over
{C : Type u_1}
[Category.{v_1, u_1} C]
{J : GrothendieckTopology C}
{I : Type u_2}
{X : I → C}
(hX : J.CoversTop X)
{I' : I → Type u}
{Y : (i : I) → I' i → Over (X i)}
(hY : ∀ (i : I), (J.over (X i)).CoversTop (Y i))
: