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.
Henri Tuhola (Nov 24 2021 at 18:49): Henri Tuhola (Nov 24 2021 at 18:52):I wonder which texts to read in order to make this easier to understand. Maybe starting with sheaves.
Mike Shulman (Nov 25 2021 at 16:25):More recent papers along similar lines include Normalization by gluing for free λ-theories and Jon Sterling's thesis.
Henri Tuhola (Nov 25 2021 at 17:23):Equally difficult paper. I didn't find thesis though.
Nathanael Arkor (Nov 25 2021 at 20:59):Henri Tuhola said:
Equally difficult paper. I didn't find thesis though.
Here: First Steps in Synthetic Tait Computability.
Notification Bot (Nov 25 2021 at 21:00):This topic was moved here from #general > normalisation by evaluation and sheaves by Nathanael Arkor
Henri Tuhola (Nov 26 2021 at 05:20):https://okmij.org/ftp/tagless-final/NBE.html
Found this but first reading the thesis.
Henri Tuhola (Nov 26 2021 at 12:37):Got the same problem as the thesis gets too foreign language for me to understand.
Leopold Schlicht (Nov 26 2021 at 12:40):Maybe it helps to ask specific questions. :grinning_face_with_smiling_eyes:
Henri Tuhola (Nov 26 2021 at 12:57):How do I understand what a pullback is?
Henri Tuhola (Nov 26 2021 at 12:57):Or any other CT idea. How is this taught to people?
Henri Tuhola (Nov 26 2021 at 13:03):I'll read the thesis again. Maybe starting in middle next time.
Leopold Schlicht (Nov 26 2021 at 13:33):Henri Tuhola said:
Or any other CT idea. How is this taught to people?
One resource is the nLab: [[pullback]]
John Baez (Nov 26 2021 at 14:48):For pullbacks and pushouts and other limits and colimits you should start here:
Tai-Danae Bradley, Limits and Colimits, Part 1 (Introduction).
Tai-Danae Bradley, Limits and Colimits, Part 2 (Definitions).
Tai-Danae Bradley, Limits and Colimits, Part 2 (Examples).
John Baez (Nov 26 2021 at 14:50):If you find these helpful, you should read everything Bradley has written on her blog about category theory.
Henri Tuhola (Nov 26 2021 at 15:00):Didn't know mathema writings about CT. Thanks. I'll read these.
Henri Tuhola (Nov 26 2021 at 15:22):There's bit of same problem as before. I feel like I do remember these ideas. But they just do nothing in my mind.
Mike Shulman (Nov 26 2021 at 15:25):You certainly need a solid foundation in category theory before trying to read any of these papers about categorical normalization. Try some of the textbooks mentioned on the nLab. Probably go for one of the more recent ones, such as Leinster's.
John Baez (Nov 26 2021 at 15:36):Tom Leinster's book is a good intro to category theory. But if definitions like "pullback" don't make clear sense to you - if they're not intuitive - then I recommend Tai-Danae Bradley's blog and Fong and Spivak's book, together with their videos and my online lectures. These are easier than Leinster's book, so they could make a good warmup.
Fawzi Hreiki (Nov 26 2021 at 15:44):Emily Riehl’s article ‘A Survey of Categorical Concepts’ is a nice warmup for her textbook (which is also fantastic)
Henri Tuhola (Nov 26 2021 at 17:10):@John Baez is the register button no longer there? Thanks for the good resource though.
John Baez (Nov 27 2021 at 14:51):You can't register, but you can still read all of my "lectures" on the first four chapters of Seven Sketches, and read the students' discussions of these chapters, and answers to the homework problems.
Henri Tuhola (Nov 27 2021 at 15:30):Yup. I did it for the first chapter and it was more rewarding read that way.
John Baez (Nov 27 2021 at 15:41):Great!
Henri Tuhola (Nov 28 2021 at 17:53):Now I understand what a pullback is. Seven sketches book has an illustration on chapter 3.
John Baez (Nov 29 2021 at 02:05):Good!
Henri Tuhola (Dec 01 2021 at 11:59):I've been examining the old ML code with agda. I have trouble in giving the scope more types. Somehow the only way to go through is through the newer papers.
Henri Tuhola (Dec 01 2021 at 14:14):https://youtu.be/SuWY3xCktpE brought an insight into what a presheaf is. Pointing at sets is literally picking of some content or 'filling' for the graph.
Alex Gryzlov (Dec 01 2021 at 14:17):Speaking of type theory, Pierre-Marie Pedrot has a series of papers on viewing (pre)sheaves through type-theoretic lenses
Alex Gryzlov (Dec 01 2021 at 14:18):https://www.pédrot.fr/drafts/cbvpresheaf.pdf Pedrot, [2019] "Presheaves as an Purified Effectful Call-by-Value Language"
https://www.pédrot.fr/articles/markov.pdf Pedrot, [2020] "Russian Constructivism in a Prefascist Theory"
https://www.pédrot.fr/drafts/sheaftt.pdf Pedrot, [2021] "Debunking Sheaves"
Alex Gryzlov (Dec 01 2021 at 14:23):The last one is particularly hilarious :)
Astra Kolomatskaia (Dec 01 2021 at 18:09):Oh, hello! I've spent more than two months thinking about this exact paper and formalising it in Cubical Agda. (Here is my basically complete current draft: https://github.com/FrozenWinters/stlc/blob/main/README.md)
Astra Kolomatskaia (Dec 01 2021 at 18:11):I think that Thorsten's paper is vastly more comprehensible than Jon's paper. Thorsten actually defines the presheaf exponential and constructs the category of Twisted Glueings rather explicitly while Jon does neither of these things.
Mike Shulman (Dec 01 2021 at 18:11):It depends on your background.
Astra Kolomatskaia (Dec 01 2021 at 18:19):On a different note, I've been reading Jon's thesis and it's actually been explaining to me what I've been doing this whole time. Jon makes the distinction between Objective and Subjective metatheory. As Thorsten explains, STLC is the language of cartesian closed categories, so any presentation of the language, so long as it has the correct universal property, is a model of the language. Models can differ in lats of ways, and I personally tried at least five approaches to syntax while doing my project. Jon refers to theorems about a specific presentation of a language as a Subjective theorems, and theorems that are true of any model of syntax as Objective theorems.
One of Jon's key points is that normalisation is generally an objective property. Traditional Normalisation by Evaluation algorithms establish this fact subjectively, while the categorical glueing argument establishes this fact objectively.
Mike Shulman (Dec 01 2021 at 18:20):That's a nice way of talking about it, although it seems strange to me to use words like "syntax" and "language" for objective notions -- to me those words sound subjective.
Henri Tuhola (Dec 01 2021 at 18:22):This is great. I'm going to read through the whole formalization and see how much it opens up.
Henri Tuhola (Dec 01 2021 at 18:23):Also trying it out myself.
Henri Tuhola (Dec 01 2021 at 18:28):The distinction between objective and syntactic properties is early on in the thesis.
Astra Kolomatskaia (Dec 01 2021 at 18:30):That's true. Jon has a very advanced "space age" thesis relative to Thorsten's paper, but I value the latter as a great starting point (and it's helped me understand the thesis quite a bit).
Henri Tuhola (Dec 01 2021 at 18:36):How easy it is to understand depends directly to how much you understand category theory. I am motivated to read into it until I figure out how to make a normaliser for about anything.
Patrick Nicodemus (Dec 01 2021 at 22:11):Alex Gryzlov said:
The last one is particularly hilarious :)
This person sounds wearying to spend more than half an hour with
Reid Barton (Dec 01 2021 at 22:36):Alex Gryzlov said:
The last one is particularly hilarious :)
Lawvere-Tierney topologies also make sense on topoi that are not presheaf topoi, hence we can generalize the bold sentence on page 5 to:
Sheaves have nothing to do with sheaves.
Patrick Nicodemus (Dec 01 2021 at 22:41):Yes I was surprised he didn't simply follow the path to this logical conclusion. If sheaves have nothing to do with presheaves and nothing to do with geometry (Leinster) then why not say sheaves have nothing to do with sheaves.
Patrick Nicodemus (Dec 01 2021 at 22:47):Much like "Zorn's lemma has nothing to do with the axiom of choice" - Again, Leinster
Jon Sterling (Dec 03 2021 at 08:49):It is a shame that there are some very interesting and innovative ideas mixed into all the misconceptions and mistaken ideologies of Pierre-Marie's screeds...
Jon Sterling (Dec 03 2021 at 08:50):I say this with as much kindness as I can... I think Pierre-Marie has contributed and continues to contribute a lot of good ideas, and is definitely an interesting guy to discuss with who has a lot to offer. But I do not like these notes.
Jon Sterling (Dec 03 2021 at 08:52):One strength of PMP's note is that he points out that sheaves can be understood very simply from an internal perspective, though. Way too much is made in traditional sources of the explicit pointwise computation of sheafhood, which in practice is something that one rarely turns to.
Henri Tuhola (Dec 04 2021 at 18:52):There's a normalization algorithm in Aaron Stump verified functional programming. There soundness and completeness proofs themselves become the normalisation algorithm.
Henri Tuhola (Dec 04 2021 at 18:52):Located that just by browsing around for agda books.
Alex Gryzlov (Dec 04 2021 at 20:23):Henri Tuhola said:
There's a normalization algorithm in Aaron Stump verified functional programming. There soundness and completeness proofs themselves become the normalisation algorithm.
That's a result of C. Coquand, if I'm not mistaken.
Alex Gryzlov (Dec 04 2021 at 20:24):