You are an extremely good teacher. Clearly, you have put a lot of effort into making this and it shows. You are not boring like many others and you really made me enthusiastic about the uses of HoTT. Thank you!!!!
This is incredibly cool and engaging. As a bachelor undergrad im very glad to finally find not just another graduate level explanations of the HoTT. Keep going!
Loving your content mate. Very straightforward explanation. Any chance of extending the Martin-Lof TT series? It helped me a lot to finally wrap my head around dependent types. All the best.
Glad to hear it! And yeah, the idea is that this will be a "reboot" of the MLTT videos, so in a couple videos I'll have covered everything from those videos, and I'll eventually get on to actually covering dependent types, identity types, and the rest of HoTT. Thanks for your patience as I slowly get there!
I've seen lectures on a little bit of type theory that looked more like pure math than computer science. I've also gotten a little bit of that from chatgpt under the right prompts. Are there any text books that give a mathematical treatment of type theory with little to no mention of computer science? Thanks in advance
It's better to typehint your function def reactorTempFactor(n: float) -> float Your version was kinda type correct it just has a return type of float | str or a union type of a string and a number
Well, in the original “Was sollen die Zahlen”, “die Zahlen” is plural (the numbers). “HoTT” is singular so most correct would probably be “Was soll HoTT”. But either way it sounds very old school. Today you wouldn’t say it like this at all. Maybe a bit more modern would be “Warum HoTT” On the other hand, you would miss the reference to the original title, so “Was sollen HoTT” sounds weird but I’ll deem it the best choice :)
@@ngruhn Ah, I failed to consider the singular vs. plural. Oh well. Like you said, I guess I'll sacrifice the grammar for the sake of historical reference.
Came here to comment that it should be "Was ist und soll die HoTT" to flex my newly acquired German skills only to find out that it's been already done by a native speaker 😅
Good question (sorry it took me forever to respond). The main two theorem provers in the HoTT world are Coq & Agda, with the corresponding programming languages being OCaML and Haskell, respectively. So, for instance, Agda is itself implemented in Haskell, borrows a lot of its syntax & conventions, and most people who work in Agda are at least proficient in Haskell. So I'd probably recommend them as good starting points
@@jacobneu-videos Thank you for the information. In such case I will consider to learn Haskell. What will result from that depends to large extent on how much free energy and time I will find.
Yeah I definitely messed that up haha. I changed the title & thumbnail to just "was soll HoTT" for this reason, but in retrospect I should've gone for something like "was sind und was sollen die homotopie typen", or just stuck to languages I actually know. Oh well...
I don't like math being a social activity. Convincing a bunch of apes does not constitute a proof to me. I hated that at Uni. - Where is the proof that your proof is correct? - Oh, you convinced me? Good job, but I'm just a stupid monkey, why should that matter? - Sure, if a monkey finds inconsistency, that is great, but if not, how is that a proof? - That's not math. That's rhetoric, and we all know how well that can go...
of course, trusting Coq etc. is still a matter of "faith" the implementation is correct, to a degree... But at least it doesn't feel as whimsical ... - Engineering forces ideas to clash with reality, and reality is the ultimate decider.
I also hated how they would mix "inconsistently overloaded" math notation and natural language, and expected to be taken seriously. - Not just using natural language as comments to explain their ideas, but as part of the proof itself? Often not using exactly defined language...
I consider crucial the ASI argument: - if ASI proves something that humans cannot comprehend, does that mean it's not proven? - Can ASI convince humans of something that is not true? and flipped for clarity: - if a scientist proves something that "dogs/chimps/children" cannot comprehend, does that mean it's not proven? - Can a scientist convince "dogs/chimps/children" of something that is not true? Yeah ... what a horrible metric.
![Three for One: Intro [Intro to HoTT, No. 1, Part 0]](http://i.ytimg.com/vi/Fn12iWcJDwE/mqdefault.jpg)
![Three for One: Intro [Intro to HoTT, No. 1, Part 0]](/img/tr.png)
![Three for One: Homotopy Interpretation [Intro to HoTT, No. 1, Part 2]](http://i.ytimg.com/vi/XUYPU9LjGKM/mqdefault.jpg)
![[Intro to HoTT - OLD] Martin-Löf Type Theory: Speaking the Language](/img/n.gif)
Welcome back Jacob . Your explanation is the best. Period .
Please continue this series.
No need to hurry, take your time .We are here.
Couldn’t agree more
You are an extremely good teacher. Clearly, you have put a lot of effort into making this and it shows. You are not boring like many others and you really made me enthusiastic about the uses of HoTT. Thank you!!!!
I don't think I ever would've been able to begin wrapping my head around HoTT without your videos. Kudos!
Absolutely brilliant video series! Subscribed.
This is so cool I finally found a good series on HoTT
Dear Jacob, this was purely amazing.
This is incredibly cool and engaging. As a bachelor undergrad im very glad to finally find not just another graduate level explanations of the HoTT. Keep going!
This is great stuff, thanks
Loving your content mate. Very straightforward explanation. Any chance of extending the Martin-Lof TT series? It helped me a lot to finally wrap my head around dependent types. All the best.
Glad to hear it! And yeah, the idea is that this will be a "reboot" of the MLTT videos, so in a couple videos I'll have covered everything from those videos, and I'll eventually get on to actually covering dependent types, identity types, and the rest of HoTT. Thanks for your patience as I slowly get there!
@@jacobneu-videos I can't wait!!
1:12 - I wish this was considered even for primary school maths, lol. - That is the the takeaway most students have from just learning any algebra.
GOOD!!! Our very own #RobinHood!
Loved the Miles Davis reference.
This video is of very, very high quality.
Very cool
In grad school, it was especially the algebraists who never said WHY we should be interested in the subject. What is the psychology here?
I've seen lectures on a little bit of type theory that looked more like pure math than computer science. I've also gotten a little bit of that from chatgpt under the right prompts.
Are there any text books that give a mathematical treatment of type theory with little to no mention of computer science? Thanks in advance
I really appreciate your video!
Awesome video!
Very fine video.
Good vid!
many things in computer science is homo. Homoiconicity, homomorphisms, homotopy type theory. Its very interesting
It's better to typehint your function
def reactorTempFactor(n: float) -> float
Your version was kinda type correct it just has a return type of float | str or a union type of a string and a number
German here. I‘ll give you B+ for pronunciation
Should it have been “Was Solltet HoTT”?
Well, in the original “Was sollen die Zahlen”, “die Zahlen” is plural (the numbers). “HoTT” is singular so most correct would probably be “Was soll HoTT”. But either way it sounds very old school. Today you wouldn’t say it like this at all. Maybe a bit more modern would be “Warum HoTT”
On the other hand, you would miss the reference to the original title, so “Was sollen HoTT” sounds weird but I’ll deem it the best choice :)
@@ngruhn Ah, I failed to consider the singular vs. plural. Oh well. Like you said, I guess I'll sacrifice the grammar for the sake of historical reference.
Came here to comment that it should be "Was ist und soll die HoTT" to flex my newly acquired German skills only to find out that it's been already done by a native speaker 😅
uooh estan rebuenos estos videos.
Loved this video. But the sound that the marker makes on paper is a bit irritating
Nottingham? You should do a video with Brady Haren!
I'm planning on making an appearance on Computerphile sometime in the near future. IDK if I'll get to do Numberphile too, but maybe one day!
9:38 Can I ask, what programming language you advice for learning and use? I guess that can be relevant to master (?) HoTT.
Good question (sorry it took me forever to respond). The main two theorem provers in the HoTT world are Coq & Agda, with the corresponding programming languages being OCaML and Haskell, respectively. So, for instance, Agda is itself implemented in Haskell, borrows a lot of its syntax & conventions, and most people who work in Agda are at least proficient in Haskell. So I'd probably recommend them as good starting points
@@jacobneu-videos Thank you for the information. In such case I will consider to learn Haskell. What will result from that depends to large extent on how much free energy and time I will find.
Hott starting from basic type theory (for non-programmers)? Seems like a long way to go…
lmao i clicked on this expected it to be in German. still good though
@23:23 what did he say? They derived that logic?
"They endeavoured to write that logic down". Bit quick, sorry
It would actually be "Was ist und was soll HoTT?", because HoTT is singular ;)
Yeah I definitely messed that up haha. I changed the title & thumbnail to just "was soll HoTT" for this reason, but in retrospect I should've gone for something like "was sind und was sollen die homotopie typen", or just stuck to languages I actually know. Oh well...
@@jacobneu-videos Yes but it's not a big deal. I really enjoy the series and it helps me a lot!
I don't like math being a social activity. Convincing a bunch of apes does not constitute a proof to me. I hated that at Uni.
- Where is the proof that your proof is correct? - Oh, you convinced me? Good job, but I'm just a stupid monkey, why should that matter?
- Sure, if a monkey finds inconsistency, that is great, but if not, how is that a proof?
- That's not math. That's rhetoric, and we all know how well that can go...
of course, trusting Coq etc. is still a matter of "faith" the implementation is correct, to a degree... But at least it doesn't feel as whimsical ...
- Engineering forces ideas to clash with reality, and reality is the ultimate decider.
I also hated how they would mix "inconsistently overloaded" math notation and natural language, and expected to be taken seriously.
- Not just using natural language as comments to explain their ideas, but as part of the proof itself? Often not using exactly defined language...
I consider crucial the ASI argument:
- if ASI proves something that humans cannot comprehend, does that mean it's not proven?
- Can ASI convince humans of something that is not true?
and flipped for clarity:
- if a scientist proves something that "dogs/chimps/children" cannot comprehend, does that mean it's not proven?
- Can a scientist convince "dogs/chimps/children" of something that is not true?
Yeah ... what a horrible metric.
"I'm right because I convinced you!" is only one step less barbaric than "I'm right because I beat you in a fight!" .... like ... come on.