```
X
→
ℝ
```

A *presheaf* `F`

is a rule that assigns

- to every open
`U ⊆ X`

a set`F(U)`

`-- functions`

- to every inclusion of opens
`U ⊆ V`

a map`r_UV : F(V) → F(U)`

`-- restriction`

such that

- for every open
`U ⊆ X`

,

the map`r_UU`

is`id`

on`F(U)`

- and if
`U ⊆ V ⊆ W`

,

then`r_UV ∘ r_VW = r_UW`

.

```
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.
```

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`

.

```
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) }
```