Cohesive sites #
Cohesive sites are sites with a number of useful properties that make their sheaf topos into a cohesive topos. See https://ncatlab.org/nlab/show/cohesive+site.
Every cohesive site is in particular local and locally connected, and every cosifted category with a terminal object that admits morphisms to every object is cohesive when equipped with the trivial topology.
TODO: generalise universe levels from max u v
to max u v w
again once that is possible.
A cohesive site is a cosifted locally connected site with a terminal object that admits morphisms to every other object. This guarantees that the sheaf topos is a cohesive topos.
For every object
X : C
there is at least one morphism from the terminal object toX
.
Instances
Every cohesive site is in particular a local site.
Every cosifted category with a terminal object that admits morphisms to every other object becomes a cohesive site when equipped with the trivial topology.
The cohesive structure of the sheaf topos on a cohesive site.
Equations
- One or more equations did not get rendered due to their size.
In sheaf topoi on cohesive sites, pieces have points in the sense that the components of
the canonical points-to-pieces transformation Γ ⟶ π₀
are epic.