diff --git a/Mathlib.lean b/Mathlib.lean
index 5caec29a98a6a1..deabf36a17a478 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2361,11 +2361,13 @@ import Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
 import Mathlib.CategoryTheory.Sites.EpiMono
 import Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
 import Mathlib.CategoryTheory.Sites.Equivalence
+import Mathlib.CategoryTheory.Sites.GlobalSections
 import Mathlib.CategoryTheory.Sites.Grothendieck
 import Mathlib.CategoryTheory.Sites.IsSheafFor
 import Mathlib.CategoryTheory.Sites.IsSheafOneHypercover
 import Mathlib.CategoryTheory.Sites.LeftExact
 import Mathlib.CategoryTheory.Sites.Limits
+import Mathlib.CategoryTheory.Sites.LocalSite
 import Mathlib.CategoryTheory.Sites.Localization
 import Mathlib.CategoryTheory.Sites.LocallyBijective
 import Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
diff --git a/Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean
index b21f86509e1a5d..698b248848e7fe 100644
--- a/Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean
+++ b/Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean
@@ -5,6 +5,7 @@ Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
 import Mathlib.CategoryTheory.Limits.Shapes.Products
+import Mathlib.CategoryTheory.Limits.Shapes.Terminal
 
 /-!
 # (Co)products in functor categories
@@ -45,6 +46,15 @@ alias piObjIso_inv_comp_pi := piObjIso_inv_comp_π
 
 end Product
 
+section Terminal
+
+/-- Evaluating the terminal functor yields the terminal object. -/
+noncomputable def terminalObjIso [HasTerminal C] (d : D) : (⊤_ (D ⥤ C)).obj d ≅ ⊤_ C :=
+  limitObjIsoLimitCompEvaluation _ d ≪≫ HasLimit.isoOfNatIso
+    ((Discrete.compNatIsoDiscrete _ _).trans <| eqToIso <| congrArg _ <| funext fun x ↦ nomatch x)
+
+end Terminal
+
 section Coproduct
 
 variable [HasColimitsOfShape (Discrete α) C]
diff --git a/Mathlib/CategoryTheory/Limits/Types.lean b/Mathlib/CategoryTheory/Limits/Types.lean
index 963e0660f85ee0..d5d519fc78b6ad 100644
--- a/Mathlib/CategoryTheory/Limits/Types.lean
+++ b/Mathlib/CategoryTheory/Limits/Types.lean
@@ -214,6 +214,12 @@ theorem limitEquivSections_symm_apply (x : F.sections) (j : J) :
     limit.π F j ((limitEquivSections F).symm x) = (x : ∀ j, F.obj j) j :=
   isLimitEquivSections_symm_apply _ _ _
 
+/-- The limit of a functor `F : J ⥤ Type _` is naturally isomorphic to `F.sections`. -/
+noncomputable def limNatIsoSectionsFunctor :
+    (lim : (J ⥤ Type max u v) ⥤ _) ≅ Functor.sectionsFunctor _ :=
+  NatIso.ofComponents (fun _ ↦ (limitEquivSections _).toIso)
+    fun f ↦ funext fun x ↦ Subtype.ext <| funext fun _ ↦ congrFun (limMap_π f _) x
+
 -- Porting note: `limitEquivSections_symm_apply'` was removed because the linter
 --   complains it is unnecessary
 --@[simp]
diff --git a/Mathlib/CategoryTheory/Sites/GlobalSections.lean b/Mathlib/CategoryTheory/Sites/GlobalSections.lean
new file mode 100644
index 00000000000000..d509452e03a14d
--- /dev/null
+++ b/Mathlib/CategoryTheory/Sites/GlobalSections.lean
@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2025 Ben Eltschig. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ben Eltschig
+-/
+import Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
+import Mathlib.CategoryTheory.Sites.ConstantSheaf
+
+/-!
+# Global sections of sheaves
+In this file we define a global sections functor `Sheaf.Γ : Sheaf J A ⥤ A` and show that it
+is isomorphic to several other constructions when they exist, most notably evaluation of sheaves
+on a terminal object and `Functor.sectionsFunctor`.
+
+## Main definitions / results
+* `Sheaf.Γ J A`: the global sections functor `Sheaf J A ⥤ A`, defined as taking each sheaf to
+  the limit of its underlying presheaf in `A`.
+* `constantSheafΓAdj J A`: the adjunction between the constant sheaf functor and `Sheaf.Γ J A`.
+* `Sheaf.ΓNatIsoSheafSections J A hT`: on sites with a terminal object `T`, `Sheaf.Γ J A` is
+  isomorphic to the functor evaluating sheaves at `T`.
+* `Sheaf.ΓNatIsoSectionsFunctor J`: for sheaves of types, `Sheaf.Γ J A` is isomorphic to the
+  functor taking each sheaf to the type of sections of its underlying presheaf in the sense of
+  `Functor.sections`.
+* `Sheaf.ΓNatIsoCoyonedaObj J`: for sheaves of types, `Sheaf.Γ J A` is isomorphic to the
+  coyoneda embedding of the terminal sheaf, i.e. the functor sending each sheaf `F` to the type
+  of morphisms from the terminal sheaf to `F`.
+-/
+
+universe u v w u₂ v₂
+
+open CategoryTheory Limits Sheaf Opposite GrothendieckTopology
+
+namespace CategoryTheory
+
+variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
+  (A : Type u₂) [Category.{v₂} A]
+
+/-- The global sections functor `Γ`, taking sheaves valued in `A` to its global sections in `A`.
+It is given here as a limit instead of evaluation on a terminal object of `C`; this has the
+advantage of not requiring `C` to have a terminal object, but the disadvantage of requiring `A`
+to have limits of shape `Cᵒᵖ`. -/
+noncomputable def Sheaf.Γ [HasLimitsOfShape Cᵒᵖ A] : Sheaf J A ⥤ A :=
+  sheafToPresheaf J A ⋙ lim
+
+/-- The constant sheaf functor is left-adjoint to the global sections functor when both exist. -/
+noncomputable def constantSheafΓAdj [HasWeakSheafify J A] [HasLimitsOfShape Cᵒᵖ A] :
+    constantSheaf J A ⊣ Γ J A :=
+  constLimAdj.comp (sheafificationAdjunction J A)
+
+instance [HasWeakSheafify J A] [HasLimitsOfShape Cᵒᵖ A] : (constantSheaf J A).IsLeftAdjoint :=
+  ⟨Γ J A, ⟨constantSheafΓAdj J A⟩⟩
+
+instance [HasWeakSheafify J A] [HasLimitsOfShape Cᵒᵖ A] : (Γ J A).IsRightAdjoint :=
+  ⟨constantSheaf J A, ⟨constantSheafΓAdj J A⟩⟩
+
+/-- For functors `F : C ⥤ Type _`, `F.sections` is naturally isomorphic to the type `⊤_ _ ⟶ F`
+of natural transformations from the terminal functor to `F`. -/
+noncomputable def sectionsFunctorNatIsoCoyoneda :
+    Functor.sectionsFunctor.{v,max u w} C ≅ coyoneda.obj (op (⊤_ _)) :=
+  let _ : ∀ X, Unique ((⊤_ C ⥤ Type max u w).obj X) := fun X ↦ (terminalObjIso X).toEquiv.unique
+  NatIso.ofComponents fun F ↦ {
+      hom s := { app X := fun _ ↦ s.1 X }
+      inv s := ⟨fun X ↦ s.app X default, fun f ↦
+        (congrFun (s.naturality f).symm _).trans <| congrArg (s.app _) <| Unique.eq_default _⟩
+      inv_hom_id := funext fun s ↦ by
+        dsimp; ext X x; simp [Unique.eq_default x]
+  }
+
+/-- When `C` has a terminal object, the global sections functor is isomorphic to the functor
+of sections on that object. -/
+noncomputable def Sheaf.ΓNatIsoSheafSections [HasLimitsOfShape Cᵒᵖ A] {T : C}
+    (hT : IsTerminal T) : Γ J A ≅ (sheafSections J A).obj (op T) := by
+  refine (isoWhiskerLeft _ ?_).trans <| (sheafSectionsNatIsoEvaluation J A).symm
+  refine @asIso _ _ _ _ { app := fun F ↦ limit.π _ _ } ?_
+  have hT' := initialOpOfTerminal hT
+  exact (NatTrans.isIso_iff_isIso_app _).2 <| fun F ↦ isIso_π_of_isInitial hT' F
+
+/-- For sheaves of types, the global sections functor is isomorphic to the sections functor
+on presheaves. -/
+noncomputable def Sheaf.ΓNatIsoSectionsFunctor :
+    Γ J (Type max u w) ≅ sheafToPresheaf J _ ⋙ Functor.sectionsFunctor _ :=
+  isoWhiskerLeft _ <| Types.limNatIsoSectionsFunctor
+
+/-- For sheaves of types, the global sections functor is isomorphic to the covariant hom
+functor of the terminal sheaf. -/
+noncomputable def Sheaf.ΓNatIsoCoyonedaObj :
+    Γ J (Type max u w) ≅ coyoneda.obj (op (⊤_ _)) := by
+  refine (ΓNatIsoSectionsFunctor J).trans ?_
+  refine (isoWhiskerLeft _ sectionsFunctorNatIsoCoyoneda).trans ?_
+  let e : (⊤_ Sheaf J _).val ≅ ⊤_ Cᵒᵖ ⥤ Type max u w :=
+    (terminalIsoIsTerminal (terminalIsTerminal.isTerminalObj (sheafToPresheaf J _) _)).symm
+  refine (isoWhiskerLeft _ <| coyoneda.mapIso e.op).trans ?_
+  exact NatIso.ofComponents fun _ ↦ Sheaf.homEquiv.toIso.symm
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
new file mode 100644
index 00000000000000..878b031a5d45ae
--- /dev/null
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2025 Ben Eltschig. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ben Eltschig
+-/
+import Mathlib.CategoryTheory.Adjunction.Triple
+import Mathlib.CategoryTheory.Sites.GlobalSections
+
+/-!
+# Local sites
+A site (C,J) is called local if it has a terminal object whose only covering sieve is trivial -
+this makes it possible to define codiscrete sheaves on it, giving its sheaf topos the structure
+of a local topos. This makes them an important stepping stone to cohesive sites.
+
+See https://ncatlab.org/nlab/show/local+site.
+
+## Main definitions / results
+* `LocalSite J`: typeclass stating that (C,J) is a local site.
+* `Sheaf.codisc`: the codiscrete functor `Type w ⥤ Sheaf J (Type max v w)` defined on any
+  local site.
+* `Sheaf.ΓCodiscAdj`: the adjunction between the global sections functor `Γ` and `Sheaf.codisc`.
+* `Sheaf.fullyFaithfulCodisc`: `Sheaf.codisc` is fully faithful.
+* `fullyFaithfulConstantSheaf`: on local sites, the constant sheaf functor is fully faithful.
+All together this shows that for local sites `Sheaf J (Type max u v w)` forms a local topos, but
+since we don't yet have local topoi this can't be stated yet.
+-/
+
+universe u v w
+
+open CategoryTheory Limits Sheaf Opposite GrothendieckTopology
+
+namespace CategoryTheory
+
+variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
+
+/-- A local site is a site that has a terminal object with only a single covering sieve. -/
+class LocalSite extends HasTerminal C where
+  /-- The only covering sieve of the terminal object is the trivial sieve. -/
+  eq_top_of_mem : ∀ S ∈ J (⊤_ C), S = ⊤
+
+/-- On a local site, every covering sieve contains every morphism from the terminal object. -/
+lemma LocalSite.from_terminal_mem_of_mem [LocalSite J] {X : C} (f : ⊤_ C ⟶ X) {S : Sieve X}
+    (hS : S ∈ J X) : S.arrows f :=
+  (S.mem_iff_pullback_eq_top f).2 <| LocalSite.eq_top_of_mem _ <| J.pullback_stable f hS
+
+/-- Every category with a terminal object becomes a local site with the trivial topology. -/
+instance {C : Type u} [Category.{v} C] [HasTerminal C] : LocalSite (trivial C) where
+  eq_top_of_mem _ := trivial_covering.1
+
+/-- The functor that sends any set `A` to the functor `Cᵒᵖ → Type _` that sends any `X : C`
+to the set of all functions `A → (⊤_ C ⟶ X)`. This can be defined on any site with a terminal
+object, but has values in sheaves in the case of local sites. -/
+noncomputable def Presheaf.codisc {C : Type u} [Category.{v} C] [HasTerminal C] :
+    Type w ⥤ (Cᵒᵖ ⥤ Type max v w) :=
+  uliftFunctor ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj
+    (coyoneda.obj (op (⊤_ C)) ⋙ uliftFunctor).op
+
+/-- On local sites, `Presheaf.codisc` actually takes values in sheaves. -/
+lemma Presheaf.codisc_isSheaf [LocalSite J] (X : Type w) : IsSheaf J (codisc.obj X) := by
+  refine (isSheaf_iff_isSheaf_of_type J _).2 fun Y S hS f hf ↦ ?_
+  refine ⟨fun g ↦ f g.down (LocalSite.from_terminal_mem_of_mem J g.down hS) ⟨𝟙 _⟩, ?_, ?_⟩
+  · intro Z g hg
+    exact funext fun (x : ULift (_ ⟶ _)) ↦
+      (congrFun (f.comp_of_compatible S hf hg x.down) _).trans (congrArg (f g hg) <| by simp)
+  · intro g hg
+    exact funext fun h : ULift (⊤_ C ⟶ Y) ↦ Eq.trans (by simp [Presheaf.codisc]) <|
+      congrFun (hg h.down ((LocalSite.from_terminal_mem_of_mem J h.down hS))) _
+
+/-- The right adjoint to the global sections functor that exists over any local site.
+Takes a type `X` to the sheaf that sends each `Y : C` to the type of functions `Y → X`. -/
+noncomputable def Sheaf.codisc [LocalSite J] :
+    Type w ⥤ Sheaf J (Type (max v w)) where
+  obj X := ⟨Presheaf.codisc.obj X, Presheaf.codisc_isSheaf J X⟩
+  map f := ⟨Presheaf.codisc.map f⟩
+  map_id _ := rfl
+  map_comp _ _ := rfl
+
+/-- On local sites, the global sections functor `Γ` is left-adjoint to the codiscrete functor. -/
+noncomputable def Sheaf.ΓCodiscAdj [LocalSite J] : Γ J (Type max u v w) ⊣ codisc J := by
+  refine Adjunction.ofNatIsoLeft ?_ (ΓNatIsoSheafSections J _ terminalIsTerminal).symm
+  exact Adjunction.mkOfUnitCounit {
+    unit := {
+      app X := ⟨{
+        app Y (x : X.val.obj Y) y := ⟨X.val.map (op y.down) x⟩
+        naturality Y Z f := by
+          ext (x : X.val.obj Y); dsimp [codisc, Presheaf.codisc]; ext z
+          exact (FunctorToTypes.map_comp_apply X.val _ _ x).symm
+      }⟩
+      naturality X Y f := by
+        ext Z (x : X.val.obj Z); dsimp [codisc, Presheaf.codisc]; ext z
+        exact congrFun (f.val.naturality _).symm x
+    }
+    counit := { app X := fun f : ULift (_ ⟶ _) → _ ↦ (f default).down }
+    left_triangle := by
+      ext X (x : X.val.obj _)
+      dsimp; convert congrFun (X.val.map_id _) x; exact Subsingleton.elim _ _
+    right_triangle := by
+      ext X Y (f : _ → _); dsimp [codisc, Presheaf.codisc]; ext y
+      dsimp; congr; convert Category.id_comp _; exact Subsingleton.elim _ _
+  }
+
+instance [LocalSite J] : (Γ J (Type max u v w)).IsLeftAdjoint :=
+  ⟨codisc J, ⟨ΓCodiscAdj J⟩⟩
+
+instance [LocalSite J] : (codisc.{u,v,max u v w} J).IsRightAdjoint :=
+  ⟨Γ J _, ⟨ΓCodiscAdj J⟩⟩
+
+/-- The global sections of the codiscrete sheaf on a type are naturally isomorphic to that type. -/
+noncomputable def Sheaf.codiscΓNatIsoId [LocalSite J] :
+    codisc J ⋙ Γ J _ ≅ 𝟭 (Type max u v w) := by
+  refine (isoWhiskerLeft _ (ΓNatIsoSheafSections J _ terminalIsTerminal)).trans ?_
+  exact (NatIso.ofComponents (fun X ↦ {
+    hom x := fun _ ↦ ⟨x⟩
+    inv f := (f (default : ULift (⊤_ C ⟶ ⊤_ C))).down
+    inv_hom_id := by
+      dsimp [codisc, Presheaf.codisc]; ext; dsimp
+      congr; exact Subsingleton.elim _ _
+  })).symm
+
+/-- `Sheaf.codisc` is fully faithful. -/
+noncomputable def Sheaf.fullyFaithfulCodisc [LocalSite J] :
+    (codisc.{u,v,max u v w} J).FullyFaithful :=
+  (ΓCodiscAdj J).fullyFaithfulROfCompIsoId (codiscΓNatIsoId J)
+
+instance [LocalSite J] : (codisc.{u,v,max u v w} J).Full :=
+  (fullyFaithfulCodisc J).full
+
+instance [LocalSite J] : (codisc.{u,v,max u v w} J).Faithful :=
+  (fullyFaithfulCodisc J).faithful
+
+/-- On local sites, the constant sheaf functor is fully faithful. -/
+noncomputable def fullyFaithfulConstantSheaf [HasWeakSheafify J (Type max u v w)] [LocalSite J] :
+    (constantSheaf J (Type max u v w)).FullyFaithful :=
+  ((constantSheafΓAdj J _).fullyFaithfulEquiv (Sheaf.ΓCodiscAdj J)).symm <|
+    Sheaf.fullyFaithfulCodisc J
+
+instance [HasWeakSheafify J (Type max u v w)] [LocalSite J] :
+    (constantSheaf J (Type max u v w)).Full :=
+  (fullyFaithfulConstantSheaf J).full
+
+instance [HasWeakSheafify J (Type max u v w)] [LocalSite J] :
+    (constantSheaf J (Type max u v w)).Faithful :=
+  (fullyFaithfulConstantSheaf J).faithful
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Sites/Sheaf.lean b/Mathlib/CategoryTheory/Sites/Sheaf.lean
index 3e940253f47311..9a83646359695a 100644
--- a/Mathlib/CategoryTheory/Sites/Sheaf.lean
+++ b/Mathlib/CategoryTheory/Sites/Sheaf.lean
@@ -345,6 +345,11 @@ def sheafToPresheaf : Sheaf J A ⥤ Cᵒᵖ ⥤ A where
 /-- The sections of a sheaf (i.e. evaluation as a presheaf on `C`). -/
 abbrev sheafSections : Cᵒᵖ ⥤ Sheaf J A ⥤ A := (sheafToPresheaf J A).flip
 
+/-- The sheaf sections functor on `X` is given by evaluation of presheaves on `X`. -/
+def sheafSectionsNatIsoEvaluation {X : C} :
+    (sheafSections J A).obj (op X) ≅ sheafToPresheaf J A ⋙ (evaluation _ _).obj (op X) :=
+  NatIso.ofComponents fun _ ↦ eqToIso rfl
+
 /-- The functor `Sheaf J A ⥤ Cᵒᵖ ⥤ A` is fully faithful. -/
 @[simps]
 def fullyFaithfulSheafToPresheaf : (sheafToPresheaf J A).FullyFaithful where