search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
447 stars 136 forks source link

Sites, sheaves and sheafification as a QIT #1031

Closed MatthiasHu closed 9 months ago

MatthiasHu commented 1 year ago

This PR provides a definition of a coverage on a category (turning it into a site) and formulates the sheaf condition (amalgamation property) for presheaves on such a site. Furthermore, the sheafification of a presheaf on a site is constructed by means of a quotient inductive type (QIT), and the appropriate universal property is shown.

MatthiasHu commented 9 months ago

@mzeuner I think I handled everything now!

mzeuner commented 9 months ago

I think the PR is ready to be merged @mortberg @felixwellen

felixwellen commented 9 months ago

Nice! Please rebase onto/merge master...

MatthiasHu commented 9 months ago

Note to my future self: it would probably have been smarter to split this PR into two (1. sites, 2. sheafification). :-)

felixwellen commented 9 months ago

Looks good to me (just skimming - two people already looked at it).