- setoids
- e-categories
- pullbacks
- presheaves
- basis for a Grothendieck topology
- sheaves, in terms of covers
- sheaf semantics
timjb / constructive-sheaf-semantics Goto Github PK
View Code? Open in Web Editor NEWThis project forked from jonsterling/constructive-sheaf-semantics
I'm putting Palmgren's Constructive Sheaf Semantics into Agda. Defines sheaves via Grothendieck pretopologies.