![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
michiexileI just lay myself down to sleep, so that I'll be fresh and amazing for my job interview tomorrow.
And took with me, as a last thing to read, Tom Leinster's 2-page paper “Sheaves do not belong to algebraic geometry”.
And now I'm back out of bed, in front of my computer again. That punchline is amazing. Inspiring. Dangerous even. The paper makes me think about how these constructions would play out in type theory — especially since the sheafification observation is “really” (in some sense) about final monad algebras (or initial comonad coalgebras), and thus hooks in neatly with Lambek's Lemma and with how Haskell does type definitions.
And the construction of sheaves and their equivalences to étale spaces is SO much clearer in Leinster's categorical language than most treatments I've read so far.
Dammit! I don't have time to sit down and port this paper to Haskell! I have sleeping to do!!
And took with me, as a last thing to read, Tom Leinster's 2-page paper “Sheaves do not belong to algebraic geometry”.
And now I'm back out of bed, in front of my computer again. That punchline is amazing. Inspiring. Dangerous even. The paper makes me think about how these constructions would play out in type theory — especially since the sheafification observation is “really” (in some sense) about final monad algebras (or initial comonad coalgebras), and thus hooks in neatly with Lambek's Lemma and with how Haskell does type definitions.
And the construction of sheaves and their equivalences to étale spaces is SO much clearer in Leinster's categorical language than most treatments I've read so far.
Dammit! I don't have time to sit down and port this paper to Haskell! I have sleeping to do!!
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2011-01-11 07:02 am (UTC)