diff --git a/Cubical/Categories/Site/Cover.agda b/Cubical/Categories/Site/Cover.agda
new file mode 100644
index 0000000000..ae6c7ea719
--- /dev/null
+++ b/Cubical/Categories/Site/Cover.agda
@@ -0,0 +1,44 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Cover where
+
+-- A cover of an object is just a family of arrows into that object.
+-- This notion is used in the definition of a coverage.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.HITs.PropositionalTruncation
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Constructions.Slice
+
+
+module _
+  {ℓ ℓ' : Level}
+  (C : Category ℓ ℓ')
+  where
+
+  open Category
+
+  Cover : (ℓpat : Level) → ob C → Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓpat))
+  Cover ℓpat c = TypeWithStr ℓpat λ patches → patches → ob (SliceCat C c)
+
+module _
+  {ℓ ℓ' : Level}
+  {C : Category ℓ ℓ'}
+  where
+
+  open Category
+
+  -- Extracting the members (patches) from a cover.
+  module _
+    {ℓpat : Level}
+    {c : ob C}
+    (cov : Cover C ℓpat c)
+    (patch : ⟨ cov ⟩)
+    where
+
+    patchObj : ob C
+    patchObj = S-ob (str cov patch)
+
+    patchArr : C [ patchObj , c ]
+    patchArr = S-arr (str cov patch)
diff --git a/Cubical/Categories/Site/Coverage.agda b/Cubical/Categories/Site/Coverage.agda
new file mode 100644
index 0000000000..5e581ef2bf
--- /dev/null
+++ b/Cubical/Categories/Site/Coverage.agda
@@ -0,0 +1,43 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Coverage where
+
+-- Definition of a coverage on a category, also called a Grothendieck topology.
+-- A coverage on a category turns it into a site
+-- and enables us to formulate a sheaf condition.
+
+-- We stay close to the definitions given in the nLab and the Elephant:
+-- * https://ncatlab.org/nlab/show/coverage
+-- * Peter Johnstone, "Sketches of an Elephant" (Definition C2.1.1)
+
+-- While the covers are just families of arrows,
+-- we use the notion of sieves to express the "pullback stability" property of the coverage.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Site.Cover
+open import Cubical.Categories.Site.Sieve
+
+module _
+  {ℓ ℓ' : Level}
+  (C : Category ℓ ℓ')
+  where
+
+  open Category C
+
+  record Coverage (ℓcov ℓpat : Level) : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-suc (ℓ-max ℓcov ℓpat)))) where
+    no-eta-equality
+    field
+      covers : (c : ob) → TypeWithStr ℓcov λ Cov → Cov → (Cover C ℓpat c)
+      pullbackStability :
+        {c : ob} →
+        (cov : ⟨ covers c ⟩) →
+        {d : ob} →
+        (f : Hom[ d , c ]) →
+        ∃[ cov' ∈ ⟨ covers d ⟩ ]
+          coverRefinesSieve
+            (str (covers d) cov')
+            (pulledBackSieve f (generatedSieve (str (covers c) cov)))
diff --git a/Cubical/Categories/Site/Sheaf.agda b/Cubical/Categories/Site/Sheaf.agda
new file mode 100644
index 0000000000..c1fa5b53ac
--- /dev/null
+++ b/Cubical/Categories/Site/Sheaf.agda
@@ -0,0 +1,138 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sheaf where
+
+-- Definition of sheaves on a site.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function using (_∘_)
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Functions.Embedding
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Site.Cover
+open import Cubical.Categories.Site.Sieve
+open import Cubical.Categories.Site.Coverage
+open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Constructions.FullSubcategory
+
+module _
+  {ℓ ℓ' : Level}
+  {C : Category ℓ ℓ'}
+  {ℓP : Level}
+  (P : Presheaf C ℓP)
+  where
+
+  open Category C hiding (_∘_)
+
+  module _
+    {c : ob}
+    {ℓ'' : Level}
+    (cov : Cover C ℓ'' c)
+    where
+
+    FamilyOnCover : Type (ℓ-max ℓP ℓ'')
+    FamilyOnCover = (i : ⟨ cov ⟩) → ⟨ P ⟅ patchObj cov i ⟆ ⟩
+
+    isCompatibleFamily : FamilyOnCover → Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓP) ℓ'')
+    isCompatibleFamily fam =
+      (i : ⟨ cov ⟩) →
+      (j : ⟨ cov ⟩) →
+      (d : ob) →
+      (f : Hom[ d , patchObj cov i ]) →
+      (g : Hom[ d , patchObj cov j ]) →
+      f ⋆ patchArr cov i ≡ g ⋆ patchArr cov j →
+      (P ⟪ f ⟫) (fam i) ≡ (P ⟪ g ⟫) (fam j)
+
+    isPropIsCompatibleFamily : (fam : FamilyOnCover) → isProp (isCompatibleFamily fam)
+    isPropIsCompatibleFamily fam =
+      isPropΠ6 λ _ _ d _ _ _ → str (P ⟅ d ⟆) _ _
+
+    CompatibleFamily : Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓP) ℓ'')
+    CompatibleFamily = Σ FamilyOnCover isCompatibleFamily
+
+    isSetCompatibleFamily : isSet CompatibleFamily
+    isSetCompatibleFamily =
+      isSetΣSndProp
+        (isSetΠ (λ i → str (P ⟅ patchObj cov i ⟆)))
+        isPropIsCompatibleFamily
+
+    elementToCompatibleFamily : ⟨ P ⟅ c ⟆ ⟩ → CompatibleFamily
+    elementToCompatibleFamily x =
+      (λ i → (P ⟪ patchArr cov i ⟫) x) ,
+      λ i j d f g eq → cong (λ f → f x) (
+        P ⟪ f ⟫ ∘ P ⟪ patchArr cov i ⟫  ≡⟨ sym (F-seq (patchArr cov i) f ) ⟩
+        P ⟪ f ⋆ patchArr cov i ⟫        ≡⟨ cong (P ⟪_⟫) eq ⟩
+        P ⟪ g ⋆ patchArr cov j ⟫        ≡⟨ F-seq (patchArr cov j) g ⟩
+        P ⟪ g ⟫ ∘ P ⟪ patchArr cov j ⟫  ∎ )
+      where
+      open Functor P
+
+    hasAmalgamationPropertyForCover : Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓP) ℓ'')
+    hasAmalgamationPropertyForCover =
+      isEquiv elementToCompatibleFamily
+
+    isPropHasAmalgamationPropertyForCover : isProp hasAmalgamationPropertyForCover
+    isPropHasAmalgamationPropertyForCover =
+      isPropIsEquiv _
+
+module _
+  {ℓ ℓ' ℓcov ℓpat : Level}
+  {C : Category ℓ ℓ'}
+  (J : Coverage C ℓcov ℓpat)
+  {ℓP : Level}
+  (P : Presheaf C ℓP)
+  where
+
+  open Coverage J
+
+  isSeparated : Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓcov) ℓpat) ℓP)
+  isSeparated =
+    (c : _) →
+    (cov : ⟨ covers c ⟩) →
+    (x : ⟨ P ⟅ c ⟆ ⟩) →
+    (y : ⟨ P ⟅ c ⟆ ⟩) →
+    ( (patch : _) →
+      let f = patchArr (str (covers c) cov) patch
+      in (P ⟪ f ⟫) x ≡ (P ⟪ f ⟫) y ) →
+    x ≡ y
+
+  isPropIsSeparated : isProp isSeparated
+  isPropIsSeparated = isPropΠ5 (λ c _ _ _ _ → str (P ⟅ c ⟆) _ _)
+
+  isSheaf : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) ℓP)
+  isSheaf =
+    (c : _) →
+    (cov : ⟨ covers c ⟩) →
+    hasAmalgamationPropertyForCover P (str (covers c) cov)
+
+  isPropIsSheaf : isProp isSheaf
+  isPropIsSheaf = isPropΠ2 λ c cov → isPropHasAmalgamationPropertyForCover P (str (covers c) cov)
+
+  isSheaf→isSeparated : isSheaf → isSeparated
+  isSheaf→isSeparated isSheafP c cov x y locallyEqual =
+    isEmbedding→Inj (isEquiv→isEmbedding (isSheafP c cov)) x y
+      (Σ≡Prop
+        (isPropIsCompatibleFamily {C = C} P _)
+        (funExt locallyEqual))
+
+module _
+  {ℓ ℓ' ℓcov ℓpat : Level}
+  {C : Category ℓ ℓ'}
+  (J : Coverage C ℓcov ℓpat)
+  (ℓF : Level)
+  where
+
+  Sheaf : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) (ℓ-suc ℓF))
+  Sheaf = Σ[ P ∈ Presheaf C ℓF ] isSheaf J P
+
+  SheafCategory :
+    Category
+      (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) (ℓ-suc ℓF))
+      (ℓ-max (ℓ-max ℓ ℓ') ℓF)
+  SheafCategory = FullSubcategory (PresheafCategory C ℓF) (isSheaf J)
diff --git a/Cubical/Categories/Site/Sheafification.agda b/Cubical/Categories/Site/Sheafification.agda
new file mode 100644
index 0000000000..43862edcad
--- /dev/null
+++ b/Cubical/Categories/Site/Sheafification.agda
@@ -0,0 +1,6 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sheafification where
+
+open import Cubical.Categories.Site.Sheafification.Base public
+open import Cubical.Categories.Site.Sheafification.ElimProp public
+open import Cubical.Categories.Site.Sheafification.UniversalProperty public
diff --git a/Cubical/Categories/Site/Sheafification/Base.agda b/Cubical/Categories/Site/Sheafification/Base.agda
new file mode 100644
index 0000000000..1f78c48c07
--- /dev/null
+++ b/Cubical/Categories/Site/Sheafification/Base.agda
@@ -0,0 +1,126 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sheafification.Base where
+
+-- Construction of the sheafification of a presheaf on a site
+-- using a quotient inductive type (QIT).
+
+-- This is inspired by the construction of the sheafification (for finite coverings) in:
+-- * E. Palmgren, S.J. Vickers, "Partial Horn logic and cartesian categories"
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Function using (_∘_)
+
+open import Cubical.HITs.PropositionalTruncation using (∣_∣₁)
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Functions.Surjection
+open import Cubical.Functions.Embedding
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Functor
+
+open import Cubical.Categories.Site.Cover
+open import Cubical.Categories.Site.Coverage
+open import Cubical.Categories.Site.Sheaf
+
+
+module Sheafification
+  {ℓ ℓ' ℓcov ℓpat : Level}
+  {C : Category ℓ ℓ'}
+  (J : Coverage C ℓcov ℓpat)
+  {ℓP : Level}
+  (P : Presheaf C ℓP)
+  where
+
+  open Category C hiding (_∘_)
+  open Coverage J
+
+  data ⟨sheafification⟅_⟆⟩ : ob → Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓcov (ℓ-max ℓpat ℓP)))) where
+
+    trunc : {c : ob} → isSet ⟨sheafification⟅ c ⟆⟩
+
+    restrict : {c d : ob} → (f : Hom[ d , c ]) → ⟨sheafification⟅ c ⟆⟩ → ⟨sheafification⟅ d ⟆⟩
+
+    restrictId :
+      {c : ob} →
+      (x : ⟨sheafification⟅ c ⟆⟩) →
+      restrict id x ≡ x
+    restrictRestrict :
+      {c d e : ob} →
+      (f : Hom[ d , c ]) →
+      (g : Hom[ e , d ]) →
+      (x : ⟨sheafification⟅ c ⟆⟩) →
+      restrict (g ⋆ f) x ≡ restrict g (restrict f x)
+
+    η⟦⟧ : {c : ob} → (x : ⟨ P ⟅ c ⟆ ⟩) → ⟨sheafification⟅ c ⟆⟩
+
+    ηNatural :
+      {c d : ob} →
+      (f : Hom[ d , c ]) →
+      (x : ⟨ P ⟅ c ⟆ ⟩) →
+      η⟦⟧ ((P ⟪ f ⟫) x) ≡ restrict f (η⟦⟧ x)
+
+    sep :
+      {c : ob} →
+      (cover : ⟨ covers c ⟩) →
+      let cov = str (covers c) cover in
+      (x y : ⟨sheafification⟅ c ⟆⟩) →
+      (x~y :
+        (patch : ⟨ cov ⟩) →
+        restrict (patchArr cov patch) x ≡ restrict (patchArr cov patch) y) →
+      x ≡ y
+
+    amalgamate :
+      let
+      -- Is there any way to make this definition now and reuse it later?
+      sheafification : Presheaf C _
+      sheafification = record
+        { F-ob = λ c → ⟨sheafification⟅ c ⟆⟩ , trunc
+        ; F-hom = restrict
+        ; F-id = funExt restrictId
+        ; F-seq = λ f g → funExt (restrictRestrict f g)
+        }
+      in
+      {c : ob} →
+      (cover : ⟨ covers c ⟩) →
+      let cov = str (covers c) cover in
+      (fam : CompatibleFamily sheafification cov) →
+      ⟨sheafification⟅ c ⟆⟩
+    restrictAmalgamate :
+      let
+      sheafification : Presheaf C _
+      sheafification = record
+        { F-ob = λ c → ⟨sheafification⟅ c ⟆⟩ , trunc
+        ; F-hom = restrict
+        ; F-id = funExt restrictId
+        ; F-seq = λ f g → funExt (restrictRestrict f g)
+        }
+      in
+      {c : ob} →
+      (cover : ⟨ covers c ⟩) →
+      let cov = str (covers c) cover in
+      (fam : CompatibleFamily sheafification cov) →
+      (patch : ⟨ cov ⟩) →
+      restrict (patchArr cov patch) (amalgamate cover fam) ≡ fst fam patch
+
+  sheafification : Presheaf C (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) ℓP)
+  Functor.F-ob sheafification c = ⟨sheafification⟅ c ⟆⟩ , trunc
+  Functor.F-hom sheafification = restrict
+  Functor.F-id sheafification = funExt restrictId
+  Functor.F-seq sheafification f g = funExt (restrictRestrict f g)
+
+  isSheafSheafification : isSheaf J sheafification
+  isSheafSheafification c cover = isEmbedding×isSurjection→isEquiv
+    ( injEmbedding
+        (isSetCompatibleFamily sheafification cov)
+        (λ {x} {y} x~y → sep cover x y (funExt⁻ (cong fst x~y)))
+    , λ fam →
+        ∣ amalgamate cover fam
+        , Σ≡Prop
+            (isPropIsCompatibleFamily sheafification cov)
+            (funExt (restrictAmalgamate cover fam)) ∣₁ )
+    where
+    cov = str (covers c) cover
diff --git a/Cubical/Categories/Site/Sheafification/ElimProp.agda b/Cubical/Categories/Site/Sheafification/ElimProp.agda
new file mode 100644
index 0000000000..0e5dd855ac
--- /dev/null
+++ b/Cubical/Categories/Site/Sheafification/ElimProp.agda
@@ -0,0 +1,208 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sheafification.ElimProp where
+
+-- An elimination operator from the QIT definition of sheafification
+-- into a dependent proposition.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.HLevels
+
+import Cubical.HITs.PropositionalTruncation as PT
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Functor
+
+open import Cubical.Categories.Site.Cover
+open import Cubical.Categories.Site.Coverage
+open import Cubical.Categories.Site.Sheaf
+
+open import Cubical.Categories.Site.Sheafification.Base
+
+
+module _
+  {ℓ ℓ' ℓcov ℓpat : Level}
+  {C : Category ℓ ℓ'}
+  (J : Coverage C ℓcov ℓpat)
+  {ℓP : Level}
+  (P : Presheaf C ℓP)
+  where
+
+  open Category C
+  open Coverage J
+  open Sheafification J P
+
+  -- We name the (potential) assumptions on 'B' here to avoid repetition.
+  module ElimPropAssumptions
+    {ℓB : Level}
+    (B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type ℓB)
+    where
+
+    isPropValued =
+      {c : ob} →
+      {x : ⟨ sheafification ⟅ c ⟆ ⟩} →
+      isProp (B x)
+
+    Onη =
+      {c : ob} →
+      (x : ⟨ P ⟅ c ⟆ ⟩) →
+      B (η⟦⟧ x)
+
+    -- This way to say that 'B' respects the 'amalgamate' point constructor
+    -- should usually be more convenient to prove.
+    isLocal =
+      {c : ob} →
+      (x : ⟨ sheafification ⟅ c ⟆ ⟩) →
+      (cover : ⟨ covers c ⟩) →
+      let cov = str (covers c) cover in
+      ((patch : ⟨ cov ⟩) → B (restrict (patchArr cov patch) x)) →
+      B x
+
+    -- This assumption will turn out to be unnecessary.
+    isMonotonous =
+      {c d : ob} →
+      (f : Hom[ d , c ]) →
+      (x : ⟨ sheafification ⟅ c ⟆ ⟩) →
+      B x → B (restrict f x)
+
+  open ElimPropAssumptions
+
+  -- A fist version of elimProp that uses the isMonotonous assumption.
+  module ElimPropWithMonotonous
+    {ℓB : Level}
+    {B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type ℓB}
+    (isPropValuedB : isPropValued B)
+    (onηB : Onη B)
+    (isLocalB : isLocal B)
+    (isMonotonousB : isMonotonous B)
+    where
+
+    -- We have to transform the 'isLocal' assumption into the actual statement
+    -- that 'B' respects 'amalgamate'.
+    amalgamatePreservesB :
+      {c : ob} →
+      (cover : ⟨ covers c ⟩) →
+      let cov = str (covers c) cover in
+      (fam : CompatibleFamily sheafification cov) →
+      ((patch : ⟨ cov ⟩) → B (fst fam patch)) →
+      B (amalgamate cover fam)
+    amalgamatePreservesB cover fam famB =
+      isLocalB
+        (amalgamate cover fam)
+        cover
+        λ patch → subst B (sym (restrictAmalgamate cover fam patch)) (famB patch)
+
+    -- A helper to deal with the path constructor cases.
+    mkPathP :
+      {c : ob} →
+      {x0 x1 : ⟨ sheafification ⟅ c ⟆ ⟩} →
+      (p : x0 ≡ x1) →
+      (b0 : B (x0)) →
+      (b1 : B (x1)) →
+      PathP (λ i → B (p i)) b0 b1
+    mkPathP p = isProp→PathP (λ i → isPropValuedB)
+
+    elimProp : {c : ob} → (x : ⟨ sheafification ⟅ c ⟆ ⟩) → B x
+    elimProp (trunc x y p q i j) =
+      isOfHLevel→isOfHLevelDep 2 (λ _ → isProp→isSet isPropValuedB)
+        (elimProp x)
+        (elimProp y)
+        (cong elimProp p)
+        (cong elimProp q)
+        (trunc x y p q)
+        i
+        j
+    elimProp (restrict f x) =
+      isMonotonousB f x (elimProp x)
+    elimProp (restrictId x i) =
+      mkPathP
+        (restrictId x)
+        (isMonotonousB id x (elimProp x))
+        (elimProp x)
+        i
+    elimProp (restrictRestrict f g x i) =
+      mkPathP (restrictRestrict f g x)
+        (isMonotonousB (g ⋆ f) x (elimProp x))
+        (isMonotonousB g (restrict f x) (isMonotonousB f x (elimProp x)))
+        i
+    elimProp (η⟦⟧ x) =
+      onηB x
+    elimProp (ηNatural f x i) =
+      mkPathP (ηNatural f x)
+        (onηB ((P ⟪ f ⟫) x))
+        (isMonotonousB f (η⟦⟧ x) (onηB x))
+        i
+    elimProp (sep cover x y x~y i) =
+      mkPathP (sep cover x y x~y)
+        (elimProp x)
+        (elimProp y)
+        i
+    elimProp (amalgamate cover fam) =
+      amalgamatePreservesB cover fam λ patch → elimProp (fst fam patch)
+    elimProp (restrictAmalgamate cover fam patch i) =
+      let cov = str (covers _) cover in
+      mkPathP (restrictAmalgamate cover fam patch)
+        (isMonotonousB (patchArr cov patch) (amalgamate cover fam)
+          (amalgamatePreservesB cover fam (λ patch' → elimProp (fst fam patch'))))
+        (elimProp (fst fam patch))
+        i
+
+  -- Now we drop the 'isMonotonous' assumption and prove the stronger version of 'elimProp'.
+  module _
+    {ℓB : Level}
+    {B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type ℓB}
+    (isPropValuedB : isPropValued B)
+    (onηB : Onη B)
+    (isLocalB : isLocal B)
+    where
+
+    -- Idea: strengthen the inductive hypothesis to "every restriction of x satisfies 'B'"
+    private
+      B' : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type (ℓ-max (ℓ-max ℓ ℓ') ℓB)
+      B' x = {d : ob} → (f : Hom[ d , _ ]) → B (restrict f x)
+
+      isPropValuedB' : isPropValued B'
+      isPropValuedB' = isPropImplicitΠ λ _ → isPropΠ λ _ → isPropValuedB
+
+      onηB' : Onη B'
+      onηB' x f = subst B (ηNatural f x) (onηB ((P ⟪ f ⟫) x))
+
+      isLocalB' : isLocal B'
+      isLocalB' x cover B'fam f =
+        PT.rec
+          isPropValuedB
+          (λ (cover' , refines) →
+            isLocalB (restrict f x) cover' λ patch' →
+              PT.rec
+                isPropValuedB
+                (λ (patch , g , p'⋆f≡g⋆p) →
+                  let
+                    p = patchArr (str (covers _) cover) patch
+                    p' = patchArr (str (covers _) cover') patch'
+                  in
+                  subst B
+                    ( restrict g (restrict p x)   ≡⟨ sym (restrictRestrict _ _ _) ⟩
+                      restrict (g ⋆ p) x          ≡⟨ cong (λ f → restrict f x) (sym p'⋆f≡g⋆p) ⟩
+                      restrict (p' ⋆ f) x         ≡⟨ restrictRestrict _ _ _ ⟩
+                      restrict p' (restrict f x)  ∎ )
+                    (B'fam patch g))
+                (refines patch'))
+          (pullbackStability cover f)
+
+      isMonotonousB' : isMonotonous B'
+      isMonotonousB' f x B'x g = subst B (restrictRestrict _ _ _) (B'x (g ⋆ f))
+
+      elimPropInduction :
+        {c : ob} →
+        (x : ⟨ sheafification ⟅ c ⟆ ⟩) →
+        B' x
+      elimPropInduction =
+        ElimPropWithMonotonous.elimProp {B = B'}
+          isPropValuedB'
+          onηB'
+          isLocalB'
+          isMonotonousB'
+
+    elimProp : {c : ob} → (x : ⟨ sheafification ⟅ c ⟆ ⟩) → B x
+    elimProp x = subst B (restrictId _) (elimPropInduction x id)
diff --git a/Cubical/Categories/Site/Sheafification/UniversalProperty.agda b/Cubical/Categories/Site/Sheafification/UniversalProperty.agda
new file mode 100644
index 0000000000..8fd6714028
--- /dev/null
+++ b/Cubical/Categories/Site/Sheafification/UniversalProperty.agda
@@ -0,0 +1,188 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sheafification.UniversalProperty where
+
+-- We prove the universal property of the sheafification,
+-- exhibiting it as a left adjoint to the forgetful functor.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Function using (_$_; _∘_)
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Functor
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Constructions.FullSubcategory
+
+open import Cubical.Categories.Site.Cover
+open import Cubical.Categories.Site.Coverage
+open import Cubical.Categories.Site.Sheaf
+
+open import Cubical.Categories.Site.Sheafification.Base
+open import Cubical.Categories.Site.Sheafification.ElimProp
+
+
+module UniversalProperty
+  {ℓ ℓ' ℓcov ℓpat : Level}
+  {C : Category ℓ ℓ'}
+  (J : Coverage C ℓcov ℓpat)
+  where
+
+  -- We assume 'P' to have the following universe level in order to ensure that
+  -- the sheafification does not raise the universe level.
+  -- This is unfortunately necessary as long as we want to use the general
+  -- definition of natural transformations for the maps between presheaves.
+  -- (Other than that, the sheafification construction should enjoy the expected
+  -- universal property also for 'P' of arbitrary universe level.)
+  ℓP = ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓcov ℓpat))
+
+  module _
+    (P : Presheaf C ℓP)
+    where
+
+    open Category C hiding (_∘_)
+
+    private
+      C^ = PresheafCategory C ℓP
+      module C^ = Category C^
+
+    open Coverage J
+    open Sheafification J P
+    open NatTrans
+    open Functor
+
+    η : P ⇒ sheafification
+    N-ob η c = η⟦⟧
+    N-hom η f = funExt (ηNatural f)
+
+    module InducedMap
+      (G : Presheaf C ℓP)
+      (isSheafG : isSheaf J G)
+      (α : P ⇒ G)
+      where
+
+{-
+           η
+        P --> sheafification
+         \    .
+          \   . inducedMap
+         α \  .
+            ∨ ∨
+              G
+-}
+
+      private
+
+        ν : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → ⟨ G ⟅ c ⟆ ⟩
+
+        ν (trunc x y p q i j) = str (G ⟅ _ ⟆) _ _ (cong ν p) (cong ν q) i j
+        ν (restrict f x) = (G ⟪ f ⟫) (ν x)
+        ν (restrictId x i) = funExt⁻ (F-id G) (ν x) i
+        ν (restrictRestrict {c} {d} {e} f g x i) = funExt⁻ (F-seq G f g) (ν x) i
+        ν (η⟦⟧ x) = (α ⟦ _ ⟧) x
+        ν (ηNatural f x i) = funExt⁻ (N-hom α f) x i
+
+        ν (sep cover x y x~y i) =
+          isSheaf→isSeparated J G isSheafG _ cover
+            (ν x)
+            (ν y)
+            (λ patch → cong ν (x~y patch))
+            i
+          where
+          cov = str (covers _) cover
+
+        ν (amalgamate cover (fam , compat)) =
+          fst (fst (equiv-proof (isSheafG _ cover) fam'))
+          where
+          cov = str (covers _) cover
+          -- We have to push forward 'fam' along the natural transformation 'ν' that we are just defining.
+          fam' : CompatibleFamily G cov
+          fam' =
+            (λ i → ν (fam i)) ,
+            λ i j d f g diamond → cong ν (compat i j d f g diamond)
+
+        ν (restrictAmalgamate cover (fam , compat) patch i) =
+          fst (snd (fst (equiv-proof (isSheafG _ cover) fam')) i) patch
+          where
+          cov = str (covers _) cover
+          fam' : CompatibleFamily G cov
+          fam' =
+            (λ i → ν (fam i)) ,
+            λ i j d f g diamond → cong ν (compat i j d f g diamond)
+
+      inducedMap : sheafification ⇒ G
+      N-ob inducedMap c = ν
+      N-hom inducedMap f = refl
+
+      inducedMapFits : η C^.⋆ inducedMap ≡ α
+      inducedMapFits = makeNatTransPath refl
+
+      module _
+        (β : sheafification ⇒ G)
+        (βFits : η C^.⋆ β ≡ α)
+        where
+
+        open ElimPropAssumptions J P
+
+        private
+          B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type _
+          B x = (β ⟦ _ ⟧) x ≡ ν x
+
+          isPropValuedB : isPropValued B
+          isPropValuedB = str (G ⟅ _ ⟆) _ _
+
+          onηB : Onη B
+          onηB = funExt⁻ (funExt⁻ (cong N-ob βFits) _)
+
+          isLocalB : isLocal B
+          isLocalB x cover locallyAgree =
+            isSheaf→isSeparated J G isSheafG _ cover
+              ((β ⟦ _ ⟧) x)
+              (ν x)
+              λ patch →
+                let f = patchArr (str (covers _) cover) patch in
+                (G ⟪ f ⟫) ((β ⟦ _ ⟧) x)                 ≡⟨ sym (cong (_$ x) (N-hom β f)) ⟩
+                ((β ⟦ _ ⟧) ((sheafification ⟪ f ⟫) x))  ≡⟨ locallyAgree patch ⟩
+                (G ⟪ f ⟫) (ν x)                         ∎
+
+        uniqueness : β ≡ inducedMap
+        uniqueness = makeNatTransPath (funExt λ _ → funExt (
+          elimProp J P {B = B} isPropValuedB onηB isLocalB))
+
+        -- This alternative proof does not use the 'pullbackStability' of the coverage.
+        module _ where private
+
+          isMonotonousB : isMonotonous B
+          isMonotonousB f x βx≡νx =
+            (β ⟦ _ ⟧) (restrict f x)  ≡⟨ cong (_$ x) (N-hom β f) ⟩
+            (G ⟪ f ⟫) ((β ⟦ _ ⟧) x)   ≡⟨ cong (G ⟪ f ⟫) βx≡νx ⟩
+            (G ⟪ f ⟫) (ν x)           ∎
+
+          uniqueness' : β ≡ inducedMap
+          uniqueness' = makeNatTransPath (funExt λ _ → funExt (
+            ElimPropWithMonotonous.elimProp J P
+              {B = B}
+              isPropValuedB
+              onηB
+              isLocalB
+              isMonotonousB))
+
+    sheafificationIsUniversal :
+      isUniversal
+        (SheafCategory J ℓP ^op)
+        ((C^ [ P ,-]) ∘F FullInclusion C^ (isSheaf J))
+        (sheafification , isSheafSheafification)
+        η
+    sheafificationIsUniversal (G , isSheafG) = record
+      { equiv-proof = λ α →
+          let open InducedMap G isSheafG α in
+            (inducedMap , inducedMapFits)
+          , λ (β , βFits) →
+              Σ≡Prop
+                (λ _ → C^.isSetHom _ _)
+                (sym (uniqueness β βFits))
+      }
diff --git a/Cubical/Categories/Site/Sieve.agda b/Cubical/Categories/Site/Sieve.agda
new file mode 100644
index 0000000000..183b6240f4
--- /dev/null
+++ b/Cubical/Categories/Site/Sieve.agda
@@ -0,0 +1,124 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sieve where
+
+-- Definition of sieves on an object
+-- and the sieve generated by a cover.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+
+open import Cubical.HITs.PropositionalTruncation as PT
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Site.Cover
+
+module _
+  {ℓ ℓ' : Level}
+  (C : Category ℓ ℓ')
+  where
+
+  open Category C
+
+  record Sieve (ℓsie : Level) (c : ob) : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-suc ℓsie))) where
+    no-eta-equality
+    field
+      passes : {d : ob} → Hom[ d , c ] → Type ℓsie
+      isPropPasses : {d : ob} → (f : Hom[ d , c ]) → isProp (passes f)
+      closedUnderPrecomposition :
+        {d' d : ob} (p : Hom[ d' , d ]) (f : Hom[ d , c ]) →
+        passes f → passes (p ⋆ f)
+
+
+module _
+  {ℓ ℓ' : Level}
+  {C : Category ℓ ℓ'}
+  where
+
+  open Category C hiding (_∘_)
+  open Sieve
+
+  sieveRefinesSieve :
+    {ℓS' ℓS : Level} →
+    {c : ob} →
+    Sieve C ℓS' c →
+    Sieve C ℓS c →
+    Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓS') ℓS)
+  sieveRefinesSieve S' S =
+    (d : ob) →
+    (f : Hom[ d , _ ]) →
+    passes S' f → passes S f
+
+  isPropSieveRefinesSieve :
+    {ℓS' ℓS : Level} →
+    {c : ob} →
+    (S : Sieve C ℓS' c) →
+    (S' : Sieve C ℓS c) →
+    isProp (sieveRefinesSieve S S')
+  isPropSieveRefinesSieve S S' =
+    isPropΠ3 (λ d f _ → isPropPasses S' f)
+
+  generatedSieve : {ℓ : Level} {c : ob} → Cover C ℓ c → Sieve C (ℓ-max ℓ' ℓ) c
+  passes (generatedSieve cov) f =
+    ∃[ i ∈ ⟨ cov ⟩ ] Σ[ h ∈ Hom[ _ , _ ] ] f ≡ h ⋆ patchArr cov i
+  isPropPasses (generatedSieve cov) f = isPropPropTrunc
+  closedUnderPrecomposition (generatedSieve cov) p f =
+    PT.rec isPropPropTrunc λ (i , h , f≡hi) →
+      ∣   i
+        , (p ⋆ h)
+        , ( (p ⋆ f)                     ≡⟨ cong (p ⋆_) f≡hi ⟩
+            (p ⋆ (h ⋆ patchArr cov i))  ≡⟨ sym (⋆Assoc p h (patchArr cov i)) ⟩
+            ((p ⋆ h) ⋆ patchArr cov i)  ∎ )
+      ∣₁
+
+  coverRefinesSieve :
+    {ℓcov ℓsie : Level}
+    {c : ob} →
+    Cover C ℓcov c →
+    Sieve C ℓsie c →
+    Type (ℓ-max ℓcov ℓsie)
+  coverRefinesSieve cov S =
+    (i : _) → passes S (patchArr cov i)
+
+  isPropCoverRefinesSieve :
+    {ℓcov ℓsie : Level}
+    {c : ob} →
+    (cov : Cover C ℓcov c) →
+    (S : Sieve C ℓsie c) →
+    isProp (coverRefinesSieve cov S)
+  isPropCoverRefinesSieve _ S = isPropΠ (λ _ → isPropPasses S _)
+
+  coverRefinesGeneratedSieve :
+    {ℓ : Level} →
+    {c : ob} →
+    {cov : Cover C ℓ c} →
+    coverRefinesSieve cov (generatedSieve cov)
+  coverRefinesGeneratedSieve i = ∣ i , id , sym (⋆IdL _) ∣₁
+
+  -- The universal property of generatedSieve
+  generatedSieveIsUniversal :
+    {ℓcov ℓsie : Level} →
+    {c : ob} →
+    (cov : Cover C ℓcov c) →
+    (S : Sieve C ℓsie c) →
+    coverRefinesSieve cov S →
+    sieveRefinesSieve (generatedSieve cov) S
+  generatedSieveIsUniversal cov S cov≤S d f =
+    PT.rec (isPropPasses S f) (λ (i , g , eq) →
+      subst (passes S) (sym eq)
+        (closedUnderPrecomposition S g (patchArr cov i) (cov≤S i)) )
+
+  pulledBackSieve :
+    {ℓsie : Level} →
+    {c d : ob} →
+    (Hom[ c , d ]) →
+    Sieve C ℓsie d →
+    Sieve C ℓsie c
+  passes (pulledBackSieve f S) g = passes S (g ⋆ f)
+  isPropPasses (pulledBackSieve f S) g = isPropPasses S _
+  closedUnderPrecomposition (pulledBackSieve f S) p g pass =
+    subst (passes S) (sym (⋆Assoc p g f))
+      (closedUnderPrecomposition S p (g ⋆ f) pass)