search

agda / cubical

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

Comparison lemma for distributive lattice #1013

Closed mzeuner closed 1 year ago

mzeuner commented 1 year ago

If B is a basis of a distributive lattice L, then the categories of sheaves on B and sheaves on L are equivalent.

mzeuner commented 1 year ago

Implemented all the requested changes from @mortberg . The notation should be more consistent now. Anything else that should be fixed/changed?

mortberg commented 1 year ago

Looks good to me! Merging