Sheaves and Lean

X → ℝ
functions glue uniquely

A presheaf F is a rule that assigns

such that 

def presheaf (X : Top) := opens(X)ᵒᵖ ⥤ Type

class category (obj : Type u) : Type (max u (v+1)) :=

(hom      : obj → obj → Type v)
(infixr ` ⟶ `:10 := hom)
(id       : Π X : obj, X ⟶ X)
(notation `𝟙` := id)
(comp     : Π {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z))
(infixr ` ≫ `:80 := comp)
(id_comp' : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
            . obviously)
(comp_id' : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
            . obviously)
(assoc'   : ∀ {W X Y Z : obj}
            (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
            (f ≫ g) ≫ h = f ≫ (g ≫ h)
            . obviously)
structure functor (C : Type u₁) [category.{v₁} C]
                  (D : Type u₂) [category.{v₂} D] :
  Type (max u₁ v₁ u₂ v₂) :=
(obj       : C → D)
(map       : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
(map_id'   : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
             map (f ≫ g) = (map f) ≫ (map g) . obviously)

instance types : large_category (Type u) :=
{ hom     := λ a b, (a → b),
  id      := λ a, id,
  comp    := λ _ _ _ f g, g ∘ f }

variables {C : Type u₁} [𝒞 : category.{v₁} C]
include 𝒞

def yoneda : C ⥤ ((Cᵒᵖ) ⥤ (Type v₁)) := 
{ obj := λ X,
  { obj := λ Y : C, Y ⟶ X,
    map := λ Y Y' f g, f ≫ g,
    map_comp' :=
    begin
      intros X_1 Y Z f g,
      ext1, dsimp at *,
      erw [category.assoc]
    end,
    map_id' :=
    begin
      intros X_1,
      ext1, dsimp at *,
      erw [category.id_comp]
    end },
map := λ X X' f, { app := λ Y g, g ≫ f } }

def yoneda_2 : C ⥤ ((Cᵒᵖ) ⥤ (Type v₁)) := 
{ obj := λ X,
  { obj := λ Y : C, Y ⟶ X,
    map := λ Y Y' f g, f ≫ g },
  map := λ X X' f, { app := λ Y g, g ≫ f } }

def yoneda_3 : C ⥤ ((Cᵒᵖ) ⥤ (Type v₁)) := ƛ X, ƛ Y : C, Y ⟶ X.

So, what is a sheaf?

Let U_i ⊆ X be open sets that cover U ⊆ X.

Consider the following set

F'(U) = { s ∈ Π_i F(U_i) | r(s_i) = r(s_j), ∀ i,j }

There is a canonical map F(U) → F'(U)

A presheaf F is called a sheaf if this canonical map is bijective for every U ⊆ X and every cover of U.

sheaves of (commutative) groups/rings
topologies on categories 
def covering_family (U : X) : Type u := set (over.{u} U)

structure coverage :=
(covers   : Π (U : X), set (covering_family U))
(property : ∀ {U V : X} (g : V ⟶ U),
            ∀ f ∈ covers U, ∃ h ∈ covers V,
            ∀ Vj ∈ (h : set _), ∃ (Ui ∈ f),
            nonempty $ ((over.map g).obj Vj) ⟶ Ui)

class site (X : Type u) extends category.{u} X :=
(coverage : coverage X)

def sheaf (X : Type u) [𝒳 : site X] :=
{ F : presheaf X // nonempty (site.sheaf_condition F) }
https://github.com/leanprover-community/mathlib/tree/sheaf-2