English
Let Type u be the universe of types. The Grothendieck topology on Type u coincides with the canonical topology on Type u.
Русский
Пусть Type u — вселенная множеств. Гротендикова топология на Type u совпадает с канонической топологией на Type u.
LaTeX
$$$typesGrothendieckTopology = \operatorname{Sheaf.canonicalTopology}(\mathrm{Type}\,u)$$$
Lean4
theorem typesGrothendieckTopology_eq_canonical : typesGrothendieckTopology.{u} = Sheaf.canonicalTopology (Type u) :=
by
refine le_antisymm typesGrothendieckTopology.le_canonical (sInf_le ?_)
refine ⟨yoneda.obj (ULift Bool), ⟨_, rfl⟩, GrothendieckTopology.ext ?_⟩
funext α
ext S
refine ⟨fun hs x => ?_, fun hs β f => Presieve.isSheaf_yoneda' _ fun y => hs _⟩
by_contra hsx
have : (fun _ => ULift.up true) = fun _ => ULift.up false :=
(hs PUnit fun _ => x).isSeparatedFor.ext fun β f hf => funext fun y => hsx.elim <| S.2 hf fun _ => y
simp [funext_iff] at this
