Why should you learn Type Theory?

This video tries to be a brief introduction to Type Theory. I am sorry for the inaccuracies or potential errors. Feel free to tell me in the comments, I just started learning about this topic but I found it too amazing not to share.

As you probably already can tell, this is my first video speaking in English so I do hope everything can be understood clearly. My pronunciation is not the nicest.

Also this is my entry to SoME1.

Music credits:
- "Inspiration Piano - Calm Background Music For Videos" by Lesfm.
- "Dreamland" by Aakash Gandhi.
- "Sea of Memory" by Aakash Gandhi.

[jacobusburger]

We need more theoretical computing videos on YouTube. Type Theory, Languages, Combinatorial Logic, etc are so interesting but no one seems to be making anything regarding them.

[AnarchoAmericium]

Someone actually having the courage to talk about types for SoME1 and not more linear algebra/calculus.

You get my subscription! And may the algorithm bless you!

[AndriyDrozdyuk]

Great video. Suggestion is get a better microphone - it will take this to the next level.

[BlackRoseMyDeath]

Grant Sanderson's manim really has made a huge impact on YouTube huh.

[MrOvipare]

The font and animations really show just how much 3Blue1Brown has been influential. That guy is a hero.

[tiborgrun]

8:56 "but since 2 + 2 reduces to 4, the type 2+2 = 2+2 is the same as the type 2+2 = 4"

Isn't that what we were trying to show in the first place? How is "reduces to" defined?

I see how only allowing refl leads to not being able to prove things like 2+3 = 4+3 since we have to start with an equality. But I don't see how refl can prove things like 2+3 = 5 if all we are doing is start by 2+3 = 2+3 and then say "2+3 reduces to 5". Or is this assuming the above definition of the sum, and so it's all successors of successors of ... of 0? Is that what's meant by "reduces to"?

[syllight]

For anyone who having a hard time understanding because of the audio, use the captions. It will help a lot!

PS: Thanks for making this video! This will greatly help with my journey on Mathematics! Please don't stop making videos <3

[officebatman]

Always happy to see more type theory videos! great work

[yosh]

Took a functional programming class last year and this reminds me a lot of that! Great video!

[okb]

Man this is amazing. I've been learning a bit by the book Homotopy type theory, which has a nice introduction to type theory. It's very interesting seing it as a foundation.

[willyh.r.]

Indeed, the type theory should be taught at any math education with a comprehensive adaptation, of course. The type theory helps to demystify math at the very fabric of the nature of this noble gradual discipline.
I 100% enjoy your video, please keep it up.

[aquilazyy]

Great video. It’s nice to see more videos on YouTube that talks about the theoretical side of Computer Science. If you have the time to make a series of this, I would love to watch them.

Don’t worry about the mic or your accent. I actually find them quite calming with your presentation style ;)

[duxoakende]

Disappointed this video has less than 200 likes, would appreciate it seeing more. It reminded me of 3b1b and other similar math Youtubers. Keep it up my friend, you've got something here.

[ramit]

It was awesome man! I loved it! As a student of logic and being frustrated with how little expository materials were available in our topic, this definitely stands out! Thanks a ton!

[erzma]

I sense the French person here.
Also I feel the influence of MP studies.

I love the videos, looking forward for the next one.

[tubex]

Sir in minute 6:59 u list down the comparison of the type theory to the logic do you have full books that talk about it

[tanchienhao]

great video, honestly this kickstarted my interest and now im playing with lean :) you have inspired me!

[R]

This was such a good and useful video. It gave a very accessible conceptual introduction to type theory. I appreciated it very much as someone who is self-teaching about computation. I really hope you make more videos like this in the future.

[arcade-fighter]

Thanks you for this introduction to Type Theory! Now I can play myself with Lean environment in order to proof my own Theorems using Type Theory point of view as opposite to Set Theory.

[skit]

Great vid, thx for that introduction!