5 ms·

An introduction to topos theory (2011) [pdf]

60 points by poetically 5y ago

auggierose 5y ago
That's incomplete, at least 8.4 and 8.5 are missing. Given that is from 2011, it will probably not be updated...
- echopurity 5y ago
  HN just upvotes category theory to feel smart.
klodolph 5y ago
Oh, neat! I knew that topoi were an alternative mathematical foundation, but this is the first time I've seen it explained in a way that I could understand. I've tried attacking the explanations on Wikipedia but my head just started spinning around each time I did it. I made it to page 8 here before I got a bit bogged down and would need to take a pad of paper out to keep following. I do enjoy this dense yet accessible style of mathematics text, it reminds my of the notes I would get from the most seasoned professors in the mathematics department... you know, the ones that have been around forever and care about teaching.
Syzygies 5y ago
Proof assistants such as Lean are inching their way into the mainstream. Ideas from topos theory, higher category theory, and homotopy theory are all running together: https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/ I'd argue that any new programming language should be designed with an awareness of the languages of formal proof. Otherwise one is barking up the wrong tree. Samuel Eilenberg, perhaps the most influential mathematician to pass through Columbia's math department doors, was in his later years a pioneer of topos theory. Colleagues viewed this with respect and puzzlement; no one else had much of a clue what topos theory even was. As a kid, I saw a photo of Eilenberg "working", deep in afternoon thought while reclining in his apartment, in a Time/Life book on mathematics. I thought, "What a great job!" Years later, he called to hire me. Early on the job, I was out drinking with friends after midnight, way downtown, when a fellow postdoc spotted Sammy at the bar. "What if he sees us!?" Huh, he's here too. We moved across the street to a quieter bar, then I saw him looking for a cab, and invited him to join the four of us. We were out together past dawn, and he beat me into the department that day, as chair. He was seventy.
- spekcular 5y ago
  Wait, what? Lean doesn't used any ideas from "topos theory, higher category theory, and homotopy theory." It uses pretty vanilla type theory. The HoTT people sometimes express annoyance at the "impurity" of their approach, in fact. Also, it's not so clear that Eilenberg is "most influential mathematician to pass through Columbia's math department doors" when people like Okounkov are there. I don't necessarily disagree, but it's a highly contestable claim.
  - deleted 5y ago
    [deleted]
  - bionhoward 5y ago
    It’s a good claim. Topos theory is a statement about type systems, right?
  - Syzygies 5y ago
    Lean is getting the most math buzz of late. The HoTT people instead use Coq, which has to be adapted to their purpose. The differences could be its own thread. I love how you allow that dependent types are now "vanilla"; perhaps more people will migrate from Haskell to Idris. The HoTT book is the trippiest read. I said "perhaps", and what's an opinion worth if it's not obviously an opinion? Eilenberg has category theory and homological algebra to his credit, those are entire subjects that have shaped the last seventy years of mathematics. I'm happy to throw him into the debate.
    - zozbot234 5y ago
      AIUI, it is possible to do HoTT in Lean 3 with no modifications to Lean itself, albeit by "disabling" singleton elimination from Prop to Type. (An example library is at https://github.com/gebner/hott3 https://github.com/gebner/hott3 .) No idea about the newer Lean 4, but the documentation does not mention any changes to the underlying logic that would affect that.
agluszak 5y ago
I'm so proud to see my uni (University of Warsaw) on the HN front page :D
CliffStoll 5y ago
A bit more approachable for this tired astronomer: Topos Theory in a Nutxhell by John Baez: https://math.ucr.edu/home/baez/topos.html https://math.ucr.edu/home/baez/topos.html
- practal 5y ago
  If you like to read about foundations, maybe you will like this as well: https://obua.com/publications/philosophy-of-abstraction-logic/1/ https://obua.com/publications/philosophy-of-abstraction-logi...

60 points by poetically 5y ago

auggierose 5y ago

That's incomplete, at least 8.4 and 8.5 are missing. Given that is from 2011, it will probably not be updated...

echopurity 5y ago
HN just upvotes category theory to feel smart.

klodolph 5y ago

Oh, neat! I knew that topoi were an alternative mathematical foundation, but this is the first time I've seen it explained in a way that I could understand. I've tried attacking the explanations on Wikipedia but my head just started spinning around each time I did it. I made it to page 8 here before I got a bit bogged down and would need to take a pad of paper out to keep following. I do enjoy this dense yet accessible style of mathematics text, it reminds my of the notes I would get from the most seasoned professors in the mathematics department... you know, the ones that have been around forever and care about teaching.

Syzygies 5y ago

Proof assistants such as Lean are inching their way into the mainstream. Ideas from topos theory, higher category theory, and homotopy theory are all running together: https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/ I'd argue that any new programming language should be designed with an awareness of the languages of formal proof. Otherwise one is barking up the wrong tree. Samuel Eilenberg, perhaps the most influential mathematician to pass through Columbia's math department doors, was in his later years a pioneer of topos theory. Colleagues viewed this with respect and puzzlement; no one else had much of a clue what topos theory even was. As a kid, I saw a photo of Eilenberg "working", deep in afternoon thought while reclining in his apartment, in a Time/Life book on mathematics. I thought, "What a great job!" Years later, he called to hire me. Early on the job, I was out drinking with friends after midnight, way downtown, when a fellow postdoc spotted Sammy at the bar. "What if he sees us!?" Huh, he's here too. We moved across the street to a quieter bar, then I saw him looking for a cab, and invited him to join the four of us. We were out together past dawn, and he beat me into the department that day, as chair. He was seventy.

spekcular 5y ago
Wait, what? Lean doesn't used any ideas from "topos theory, higher category theory, and homotopy theory." It uses pretty vanilla type theory. The HoTT people sometimes express annoyance at the "impurity" of their approach, in fact. Also, it's not so clear that Eilenberg is "most influential mathematician to pass through Columbia's math department doors" when people like Okounkov are there. I don't necessarily disagree, but it's a highly contestable claim.
- deleted 5y ago
  [deleted]
- bionhoward 5y ago
  It’s a good claim. Topos theory is a statement about type systems, right?
- Syzygies 5y ago
  Lean is getting the most math buzz of late. The HoTT people instead use Coq, which has to be adapted to their purpose. The differences could be its own thread. I love how you allow that dependent types are now "vanilla"; perhaps more people will migrate from Haskell to Idris. The HoTT book is the trippiest read. I said "perhaps", and what's an opinion worth if it's not obviously an opinion? Eilenberg has category theory and homological algebra to his credit, those are entire subjects that have shaped the last seventy years of mathematics. I'm happy to throw him into the debate.
  - zozbot234 5y ago
    AIUI, it is possible to do HoTT in Lean 3 with no modifications to Lean itself, albeit by "disabling" singleton elimination from Prop to Type. (An example library is at https://github.com/gebner/hott3 https://github.com/gebner/hott3 .) No idea about the newer Lean 4, but the documentation does not mention any changes to the underlying logic that would affect that.

agluszak 5y ago

I'm so proud to see my uni (University of Warsaw) on the HN front page :D

CliffStoll 5y ago

A bit more approachable for this tired astronomer: Topos Theory in a Nutxhell by John Baez: https://math.ucr.edu/home/baez/topos.html https://math.ucr.edu/home/baez/topos.html

practal 5y ago
If you like to read about foundations, maybe you will like this as well: https://obua.com/publications/philosophy-of-abstraction-logic/1/ https://obua.com/publications/philosophy-of-abstraction-logi...