[HN Gopher] An introduction to topos theory (2011) [pdf]
___________________________________________________________________
An introduction to topos theory (2011) [pdf]
Author : poetically
Score : 50 points
Date : 2021-11-28 07:17 UTC (3 days ago)
(HTM) web link (www.fuw.edu.pl)
(TXT) w3m dump (www.fuw.edu.pl)
| CliffStoll wrote:
| A bit more approachable for this tired astronomer:
|
| Topos Theory in a Nutxhell by John Baez:
| https://math.ucr.edu/home/baez/topos.html
| practal wrote:
| If you like to read about foundations, maybe you will like this
| as well: https://obua.com/publications/philosophy-of-
| abstraction-logi...
| klodolph wrote:
| 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.
| agluszak wrote:
| I'm so proud to see my uni (University of Warsaw) on the HN front
| page :D
| Syzygies wrote:
| 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/
|
| 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 wrote:
| 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]
| bionhoward wrote:
| It's a good claim. Topos theory is a statement about type
| systems, right?
| Syzygies wrote:
| 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 wrote:
| 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 .) No idea
| about the newer Lean 4, but the documentation does not
| mention any changes to the underlying logic that would
| affect that.
| auggierose wrote:
| That's incomplete, at least 8.4 and 8.5 are missing. Given that
| is from 2011, it will probably not be updated...
| echopurity wrote:
| HN just upvotes category theory to feel smart.
___________________________________________________________________
(page generated 2021-12-01 23:03 UTC)