# Sheafification of `Type`

valued presheaves #

We construct the sheafification of a `Type`

valued presheaf,
as the subsheaf of dependent functions into the stalks
consisting of functions which are locally germs.

We show that the stalks of the sheafification are isomorphic to the original stalks,
via `stalkToFiber`

which evaluates a germ of a dependent function at a point.

We construct a morphism `toSheafify`

from a presheaf to (the underlying presheaf of)
its sheafification, given by sending a section to its collection of germs.

## Future work #

Show that the map induced on stalks by `toSheafify`

is the inverse of `stalkToFiber`

.

Show sheafification is a functor from presheaves to sheaves,
and that it is the left adjoint of the forgetful functor,
following

The prelocal predicate on functions into the stalks, asserting that the function is equal to a germ.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The local predicate on functions into the stalks, asserting that the function is locally equal to a germ.

## Equations

## Instances For

The sheafification of a `Type`

valued presheaf, defined as the functions into the stalks which
are locally equal to germs.

## Equations

## Instances For

The morphism from a presheaf to its sheafification, sending each section to its germs. (This forms the unit of the adjunction.)

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The natural morphism from the stalk of the sheafification to the original stalk.
In `sheafifyStalkIso`

we show this is an isomorphism.

## Equations

## Instances For

The isomorphism between a stalk of the sheafification and the original stalk.