You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (May 30 2022 at 14:49):Thierry Coquand: Sheaf Cohomology in Univalent Type Theory
In the introduction of his book on Higher Topos Theory, Jacob Lurie motivates this theory by the fact that it allows an elegant and general treatment of sheaf cohomology. It was realised early on that these ideas could be expressed in the setting of univalent foundations/homotopy type theory (cf. the blog post of Mike Shulman on cohomology, 24 July 2013). I will try to explain recent insights which show that this can be done in a maybe surprisingly direct way. Furthermore, all this can be formulated in a constructive meta theory, avoiding the non effective notion of injective resolutions.
Zoom: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhTdGhvZ3pUdz09
YouTube: https://youtu.be/nN5IhhncUCk