An introduction to topos theory (2011) [pdf]
fuw.edu.pl
fuw.edu.pl
Topos Theory in a Nutxhell by John Baez: https://math.ucr.edu/home/baez/topos.html
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.
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.
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.
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.