open import Cat.CartesianClosed.Instances.PSh
open import Cat.Thin.Instances.Sub
open import Cat.Instances.Functor
open import Cat.Instances.Slice
open import Cat.Functor.Everything
open import Cat.Diagram.Everything
open import Cat.Prelude
import Cat.Reasoning as Cat

open import Topoi.Reasoning
open import Topoi.Base

module wip.site where

open /-Hom
open /-Obj

module _ {o ℓ} (C : Precategory o ℓ) (fc : Finitely-complete C) where
  private
    module C = Cat C
    module Sub O = Cat (Subobj C O)

    _∩_ : ∀ {X} → Sub.Ob X → Sub.Ob X → Sub.Ob X
    _∩_ a b = subobj-products C {A = a} {b}
      (fc .Finitely-complete.pullbacks _ _) .Product.apex

  record Topology : Type (o ⊔ ℓ) where
    field
      closure : ∀ {X} → Sub.Ob X → Sub.Ob X
      monotonic : ∀ {X} (s : Sub.Ob X) → Sub.Hom X s (closure s)
      idempotent : ∀ {X} (s : Sub.Ob X) → Sub.Hom X (closure (closure s)) (closure s)
      stable
        : ∀ {X} (s t : Sub.Ob X)
        → Sub.Hom X (closure (s ∩ t)) (closure s ∩ closure t)

    dense : ∀ {X} → Sub.Ob X → Type _
    dense s = Sub._≅_ _ (closure s) s

    local : C.Ob → Type _
    local O =
      ∀ {m : Sub.Ob O}
      → dense m
      → is-equiv {A = C.Hom O _} ((m .object .map C.∘_))

module _ {ℓ} {C : Precategory ℓ ℓ} where
  private
    fc : Finitely-complete (PSh ℓ C)
    fc = with-pullbacks _ (PSh-terminal {C = C}) (PSh-pullbacks {C = C})

  module _ (tp : Topology (PSh ℓ C) fc) where
    module tp = Topology tp

    Sheaves : Precategory _ _
    Sheaves = Restrict {C = PSh ℓ C} tp.local

    incl : Functor Sheaves (PSh ℓ C)
    incl = Forget-full-subcat

    incl-ff : is-fully-faithful incl
    incl-ff = id-equiv

    open Functor

    -- Sheafification : Functor (PSh ℓ C) Sheaves
    -- Sheafification .F₀ pre .object = {!   !}
    -- Sheafification .F₀ pre .witness = {!   !}
    -- Sheafification .F₁ = {!   !}
    -- Sheafification .F-id = {!   !}
    -- Sheafification .F-∘ = {!   !}