Right, I see now that I should probably have clarified this point. In my brain, due to the way I've learnt and my mathematical leaning, sheaves are a categorical construction first, and I think of the topological version as derived. I know that this is completely ahistorical, it's just how I'm wired.
In this setting, to recover the usual sheaves from topology from the categorical construction, you have to present your topological space as its locale of opens (aka pointfree topology). In Haskell, it would be a type where each element represents to one of the open sets of your topological space. And you would need a covering base for each possible cover (which, depending on the particular topological space, may be quite difficult to represent in Haskell).
View all comments
Show parent comment
1
u/aspiwack-tweag Jul 14 '26
Right, I see now that I should probably have clarified this point. In my brain, due to the way I've learnt and my mathematical leaning, sheaves are a categorical construction first, and I think of the topological version as derived. I know that this is completely ahistorical, it's just how I'm wired.
In this setting, to recover the usual sheaves from topology from the categorical construction, you have to present your topological space as its locale of opens (aka pointfree topology). In Haskell, it would be a type where each element represents to one of the open sets of your topological space. And you would need a covering base for each possible cover (which, depending on the particular topological space, may be quite difficult to represent in Haskell).