search

isovector / reasonablypolymorphic.com

⏳ my math blog
http://reasonablypolymorphic.com
BSD 3-Clause "New" or "Revised" License
23 stars 11 forks source link

blog/sheafs/index #36

Open utterances-bot opened 1 year ago

utterances-bot commented 1 year ago

Review: A Very Elementary Introduction to Sheaves :: Reasonably Polymorphic

https://reasonablypolymorphic.com/blog/sheafs/index.html

williamdemeo commented 1 year ago

Just started reading this post, and already finding it quite compelling, but I had to pause to comment on your beautiful presentation. I love that the whole thing is a literate Agda file and the code is pretty-printed with hyperlinks to the source. That's just awesome! I had to work very hard to achieve a similar effect when documenting my Agda library (ualib.org), but I think you do a better job. You even have the correct typesetting of symbols that appear in the paragraphs discussing the code... wow! I wonder if you would be willing to describe your workflow. Perhaps you would even be generous enough to write a blog post explaining how you create such amazing posts. Your whole website is awesome, by the way, so if you care to share some tips and tools you use to create it, I (and I suspect many others) would be very grateful! Thank you for your wonderful site.

williamdemeo commented 1 year ago

You write, "and two cases to satisfy the preorder laws." I suspect you initially had an ex<-trans constructor as well, and then discovered that you didn't need it...?

isovector commented 1 year ago

Hi William, thanks for the kind words! This site is generated via https://github.com/isovector/blagda, which is a blogging platform I slapped together based on the source code of the https://1lab.dev/. You're free to try to suit it to your purposes, and I'm happy to answer any technical questions you might come across.

On January 4, 2023 8:08:02 PM PST, William DeMeo @.***> wrote:

Just started reading this post, and already finding it quite compelling, but I had to pause to comment on your beautiful presentation. I love that the whole thing is a literate Agda file and the code is pretty-printed with hyperlinks to the source. That's just awesome! I had to work very hard to achieve a similar effect when documenting my Agda library (ualib.org), but I think you do a better job. You even have the correct typesetting of symbols that appear in the paragraphs discussing the code... wow! I wonder if you would be willing to describe your workflow. Perhaps you would even be generous enough to write a blog post explaining how you create such amazing posts. Your whole website is awesome, by the way, so if you care to share some tips and tools you use to create it, I (and I suspect many others) would be very grateful! Thank you for your wonderful site.

-- Reply to this email directly or view it on GitHub: https://github.com/isovector/reasonablypolymorphic.com/issues/36#issuecomment-1371759859 You are receiving this because you are subscribed to this thread.

Message ID: @.***>