English
Global sections of a sheaf of types correspond to morphisms from a terminal constant sheaf; explicitly, ΓObjEquivHom provides the equivalence.
Русский
Глобальные секции шейфа типа соответствуют морфизмам из терминального константного шейфа; ΓObjEquivHom задаёт эквивалентность.
LaTeX
$$$\Gamma J (Type w) \;\simeq\; ((\text{constantSheaf } J (Type w)).\mathrm{obj} X \to F)$$$
Lean4
/-- Global sections of a sheaf of types `F` correspond to morphisms from a terminal sheaf to `F`.
We use the constant sheaf on a singleton type as a specific choice of terminal sheaf here. -/
noncomputable def ΓObjEquivHom [HasWeakSheafify J (Type w)] [HasGlobalSectionsFunctor J (Type w)] (F : Sheaf J (Type w))
(X : Type w) [Unique X] : (Γ J (Type w)).obj F ≃ ((constantSheaf J (Type w)).obj X ⟶ F) :=
(Equiv.funUnique X _).symm.trans ((constantSheafΓAdj J (Type w)).homEquiv _ _).symm
