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.

[@AndriyDrozdyuk]

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

[@dappermink]

I know right, I am very sorry for the microphone but I didn't feel like purchasing one yet. Thank you so much!

[@1495978707]

Also try not to eat the microphone. That was more of an issue than cheap microphone

[@eccentricOrange]

@@1495978707 I know that you only mean to give constructive feedback, but am laughing pretty hard now.

[@extremeheat7947]

Try using your phone to record the audio

[@barbietripping]

@@dappermink I’m sure people would be willing to help your purchase one if you’re making videos like these.

[@jacobusburger]

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

[@dappermink]

Exactly the thought that pushed me to make this video despite I knew both my English and my microphone were poor

[@jacobusburger]

@@dappermink It's great that you did. Maybe this will inspire more videos on this kind of topic?

[@dappermink]

@@jacobusburger I do hope so!

[@fppt1555]

I like watching code report, he posts about this kind of stuff too! Nice video here nonetheless.

[@TheJacklwilliams]

@@dappermink That is quite alright. You get 1000 points for taking that thought and making it a reality. Keep it up and your bound to keep improving as the rest of us joining you are working on. Huge thanks for the effort and the quality work you put out. Re your English? Us Americans are pitiful. Everywhere I traveled in the last thirty years I met people who were multilingual with English being one of them. We, are way behind you all and too many of us know only English (including me). Lastly, those of us who work in tech have well learned how to adjust to accent/annunciation from other cultures, or should've by now. The NUMBER ONE benefit I've received from a lifetime in this business is my understanding and appreciation for other cultures and the friendships I've made.

[@BlackRose4MyDeath]

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

[@dappermink]

right? 🙃

[@KlaudiusL]

He did more than just teach maths .. He brought the tools so anyone can teach too. That's a great act of altruism

[@duartesilva7907]

@@KlaudiusL that's why the man is a legend.

[@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!

[@dappermink]

Thanks a lot for the support! I'm still very new to type theory, but since there were almost no video on it on KZbin I thought it was too interesting not to share!

[@itsmeagain1415]

@@dappermink Yes, I just actually heard about it a couple of days ago and just by the looks of it it feeled very interesting, I'm actually interested in learning it now, but I don't know if it should be after completing predicate logic or I can just start learning about it

[@dappermink]

@@itsmeagain1415 I guess you can learn it anytime. Having more background with other fields might help you make connections but I don't think it's required at all. Just be aware the "logic" of type theory is intuitionist or constructivist, which studies what can or cannot be constructed (proofs), as opposed to predicate logic that studies what is or isn't true.

[@MrOvipare]

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

[@dappermink]

Ikr His tool his public tho, so that's why

[@syllight9053]

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

[@dappermink]

Thank you a lot!! Glad it can help! Yeah, since both my accent and the microphone quality are bad I decided to at least add captions manually haha

[@alex95sang52]

@@dappermink Where are you from?

[@dappermink]

@@alex95sang52 In case that wasn't obvious already, I'm French, like you 🙃

[@duxoakende]

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

[@dappermink]

Thanks a ton for the awesome support!!

[@officebatman9411]

Always happy to see more type theory videos! great work

[@dappermink]

Thank you Batman!!

[@tiborgrun6963]

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"?

[@dappermink]

Yes it's exactly that. 2+3=5 is a type By definition, we have 5 := s(s(s(s(s(0))))) and 2+3 := sum( s(s(0)), s(s(s(0))) ) := := s(s(s(s(s(0))))) We can replace anything by its definition, it's like an alias, so 2+3=5 is just the type s(s(s(s(s(0))))) = s(s(s(s(s(0))))) rewritten with syntactic sugar (which can also be written 5=5) So finally, we know refl(5) has the type 5=5, and so that's not only a proof that 5=5 but also a proof of the same proposition rewritten differently such as 2+3=5 It kinda feels like cheating, but if that doesn't really feel like we're proving anything it's because we don't need to tell the computer 2+3 reduces to 5, it can automatically see it applying the definitions we provided Hope I could make it a bit clearer

[@prudiiarca]

@@dappermink I loved your video! Just as a constructive feedback, I think this explanation should have been part of the video. It‘s those little details, which make math so hard…

[@dappermink]

@@prudiiarca You're entirely right, I should have I didn't because first I wasn't sure of my understanding on this at the time of writing the script, and also because of the SoME1 deadline. However I currently plan to cover the topic further and from another angle, so this explanation will definitely be part of it. But first of all I need to need to figure out how to have a decent audio quality haha

[@dappermink]

@@prudiiarca Anyway thanks a lot for both the feedback and the support!

[@okb6436]

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.

[@dappermink]

Thank you so much, it means a lot to me!

[@yosh9651]

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

[@dappermink]

Thanks a lot! Yeah this has a lot to do with lambda calculus, which functional programming is based on

[@aquilazyy1125]

Great video. It’s nice to see more videos on KZbin 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 ;)

[@dappermink]

Thank you so much, really! I do plan to make other videos to go further on this topic, but I have not enough free time for now to work on it so it's probably gonna take a while.

[@tanchienhao]

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

[@dappermink]

Amazing!!! Thanks a lot!

[@tanchienhao]

@@dappermink there seems to be very little videos on lean on youtube, maybe consider making some tutorials :) wld be great for the outreach

[@dappermink]

@@tanchienhao I am also starving for more lean videos, I am only discovering lean for now so I don't consider doing tutorials haha There also are other proof assistants than lean such as coq, but I haven't investigated them yet. Maybe some of them have more online resources?

[@neilclay5835]

I think you're on to a great idea. I hope you get a better microphone though, because I was struggling quite a bit to hear. Your English is fine. Best of luck.

[@5708R]

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.

[@dappermink]

Thank you so much, this kind of support really helps motivation! Also, sure, it's planned (':

[@ramit7]

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!

[@dappermink]

Thanks a ton for the cheerful support! This video definitely exists because of my own frustration of how undercovered this topic is, so I am more than content I can make people discover and like it! This is just a poor attempt at introducing Type Theory which I am myself learning, so if that triggered your interest be aware there is much more fascinating about it that I couldn't cover yet, so feel free to explore it by yourself (I personally read the HoTT book which introduces Type Theory at the beginning)

[@ramit7]

@@dappermink Thanks for the invite. I am an explorer of this realm. I am yet to settle on where I want to research further. But I had dabbled with (introductory) HoTT by myself. Couldn't keep up the motivation because no one surrounding me was interested in it and it did get fairly involved that I needed guidance from an expert which wasn't available. All the best in your journey to HoTT :) I wish you luck. And would love it if you also get to cover the more convoluted aspects. Usually, the online materials I find are the simpler ones( or the introductory material) very well enunciated but the trickier/harder ones are usually left out. For the case of general maths, I think there, a lot of expert popularisers are coming into the scene which makes youtube a constant thrilling experience! I wish for topics in logic, esoteric ideas of forcing to prove independence of the continuum hypothesis, quantifier elimination of peano arithmetic, borel determinacy theorem, zero-one laws for first order logic, etc have their expositions as well.

[@dappermink]

I feel you, I also wish I knew an expert to guide me. Instead all I can do is trying to gathering the bits of knowledge here and there on the internet, which itself isn't even that bad if I had enough free time haha. I wish I could cover more but that would be too presumptuous, if I could at least cover enough of the introductory/intermediate material (which I need to understand myself first), that would be already amazing to me!

[@ramit7]

You are doing an amazing job! ^_^@@dappermink

[@Bruno-el1jl]

Thanks so much for this gem! Really really interesting topic! 🙌🙌🙌

[@dappermink]

Thank you!!

[@viniciusataidedealbuquerqu2837]

your transitions are top notch

[@dappermink]

Thank you!

[@skit555]

Great vid, thx for that introduction!

[@willyh.r.1216]

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.

[@dappermink]

I completely agree, thanks a lot btw!

[@patrickgh3]

satisfying animations! type theory seems interesting, even though i don't quite grasp how proof verifiers work, but I guess they work somehow. can only cover so much in 10 minutes, hah.

[@dappermink]

Thank you! As far as I know, they work a bit like any programming language with a type system: When you write a typed function in a typed programming language, if your last return statement has a wrong type the compiler will tell you Well, for a proof assistant, if you write a proof you're basically constructing an element with a specific type combining preexisting elements and constructors, so the assistant can check for any errors the same way. No type error means your proof is correct!

[@patrickgh3]

@@dappermink ahh, gotcha, so it's checking that a proof you're writing is correct, not proving that an algorithm you're writing is correct. thanks.

[@dappermink]

@@patrickgh3 Though you can also write proofs about your algorithms. That's like the next level of unit testing haha

[@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.

[@dappermink]

That's awesome, thank you! : )

[@maxdemian6312]

An outstanding video on this topic

[@WasifHasanBaig]

This is GOLD

[@michaelhearmon9965]

Thank you for explaining this. I have been watching Professor Altenkirch's Type Theory, but didn't understand the basics. Please make some more :)

[@dappermink]

I definitely will, thank you so much for the kind words it means a lot

[@alfheiureddasigurardottir5427]

Excellent video! It made me interested in type theory 😊

[@dappermink]

Thank you so much!!

[@Manoj6550]

Hey, Thank you for creating this video. I learnt something new.

[@dappermink]

That's awesome! Thanks a lot for the kind comment!

[@erzma9908]

I sense the French person here. Also I feel the influence of MP studies. I love the videos, looking forward for the next one.

[@dappermink]

Haha, looks like I cannot hide my accent Thanks a lot!

[@Rule_110]

The best 👍👍👍👍👍👍 Great Video

[@dappermink]

Thank you so much!

[@joaosilveira29]

Great video!

[@svenskapankako]

The last part where "2+2=2+2" became "2+2=4" and that that implied p could be both 2+2 and 4 was pretty hand wavy. Why could we do arithmetic when it was a type? How do we prove that you can change 2+2 into 4?

[@dappermink]

Well, that part confused me too since I'm only discovering type theory. As I understand it, 2+2 is the same as 4 by definition (the definition of sum). 4 is the reduced form of 2+2 so that's why you can replace it wherever you want. But I'm not even sure I'm correct. Sorry, the HOTT book probably explains it better.

[@_okedata]

we can use the defintion from before. 2+2 = sum(2,2) 2+2 = sum(ss 0, ss 0) 2+2 = s sum(s 0, ss 0) 2+2 = ss sum(0, ss 0) 2+2 = ss ss 0 2+2 = 4 (i used s instead of the arrow)

[@svenskapankako]

@@_okedata Yeah I understand that but why can we do that when 2+2=2+2 and 2+2=4 are types and not values. There might not be a difference. I think it's mostly that I don't know the rules, so this type of proof feels like your inventing things you can do.

[@CanIHaveSomeMore]

@@dappermink if "2+2 is the same as 4 by definition" than proving 2+2=4" as described is a circular argument, or at least a redundant one.

[@dappermink]

@@CanIHaveSomeMore That's not really circular, you can reduce 2+2 to 4 using the sum definition, and then you can use the refl constructor to proof that 2+2=4 is inhabited.

[@5hape5hift3r]

Didnt know that national geographic had this type of content

[@evertonsantosdeandradejuni3787]

very good, the more math and eduators the better !

[@dappermink]

Thank you so much!

[@sohangchopra6478]

Nice video! Unlike some other videos I watched on Type Theory and Category Theory (they are related), this one was actually interesting, and not a dry / boring video. I have been looking to learn type theory (mainly because I like Haskell). Is there any good video resource you would recommend?

[@dappermink]

Thank you so much! I'm sorry, I'm not aware of any good video resources on the topic since that's the reason why I made my own : (

[@ramonjales9941]

amazing vídeo!

[@hugeride]

This videos is too good to keep with this audio quality! You should remake it! Thank you.

[@dappermink]

Thank you! I guess remaking it could be a good idea, but if I had some free time I'd rather use it to make a whole new video than just a remake : )

[@hugeride]

@@dappermink well that would be even better, although the video is pretty neat. :-)

[@fizzyeltsuo]

I was struggling with dependent types until I saw this video.

[@Phymaths]

Your animations are really good. Which platform do you use for it? Thanks

[@dappermink]

Thank you, I used manim, an animation tool using Python made by 3b1b

[@Phymaths]

@@dappermink ohh I see. Thanks

[@veysel7232]

Thanks for the video. It helped me a lot to understand programming language theory. Are there books you read or that can help me understand logic.

[@dappermink]

Sorry I don't know any book about logic since I mostly studied it at uni and with wikipedia, but I suppose you can find some quite easily. Please note that type theory doesn't use classical logic but intuitionistic (or constructive) logic instead

[@fyradur]

Lean is 100% the future of mathematics

[@islandcave8738]

0 is not a natural number. 0 is a whole number. Natural numbers are integers that start with 1. Whole numbers are integers that start with 0. Integers are 0 and positive and negative integrals.

[@dappermink]

It really depends on your definition. The wikipedia page of natural numbers says there are two major distincts definitions: with or without zero. And with zero seems to be the standard one by the way. But anyway, here I am talking about the natural numbers as defined in Type Theory, and those include the zero.

[@ianmathwiz7]

Do all types correspond to a logical proposition? If so, what proposition does the Boolean type correspond to? Or the integer type?

[@dappermink]

I am very new to type theory and far from perfectly understanding the topic, so if anyone more knowledgeable that me could clarify that it would be awesome! Anyway, as far as *I* know, all types do correspond to logical propositions, but the common types (Bool, Integer, ...) are to trivial to express anything interesting: they simply state that they can be inhabited, namely that there exists a bool, or that there exists an integer. And providing an integer is indeed an element of that type and a constructive proof that integers do exist. It gets more interesting with dependant types who are inhabited depending on specific values, such as the "A or B" type. Since this type has only two constructors, the first one requiring an element of A and the second an element of B, having an element of "A or B" is indeed a proof that you either have A or have B. Hope I could make this a bit clearer!

[@joaofrancisco8864]

"theorem quickmaths" really got me

[@joaofrancisco8864]

oh, and great video btw! i had never heard of Type Theory before, but now i'm eager to learn more about it

[@dappermink]

@@joaofrancisco8864 Thanks a lot! I too never heard of Type Theory until recently, SoME1 and the fact it's so hard finding content on this topic pushed me making this. But even with only the very little I know, there is yet so much more (and way more fascinating) to cover. If I manage to improve my audio quality, then I just need to cover more!

[@joaofrancisco8864]

@@dappermink please do!

[@a0um]

I really liked the graphic rendering of the formulas. May I ask what software you used?

[@dappermink]

Thank you! Sure, it's manim, created by 3blue1brown

[@LakanBanwa]

Great video, you got a new subscriber! I also like lean and have been enjoying going through it recently!! Now, when you get into the proposition as types topic at the 5 minute mark, when you say something is "not provable", shouldn't we really be saying "not provable with *these sets of axioms*"? Or have we somehow found out that this statement is not provable no matter what axioms you choose? The latter being an incredibly strong statement leads me to believe we really mean the former.

[@dappermink]

Thank you so much!! Yes of course, what is provable depends of the set of axioms. I suppose you refer to the proposition "if a type has no inhabitant, then it is unprovable". What I meant by that is that if you cannot find an inhabitant of a given type, then that means you cannot prove its corresponding proposition. I was using "unprovable" as part of the metalanguage. If you want to PROVE that something is unprovable, you need to prove that it is impossible to construct any inhabitant of its corresponding type. That can sometimes be possible by allowing specific axioms, but by default Type Theory is built onto constructivism logic in which you cannot use proofs by contradiction.

[@LakanBanwa]

@@dappermink Thanks for the response! I appreciate that clarification into both the type theory and constructivist way of thinking about it as I'm getting myself familiarized with it and getting out of my set theory comfort zone (aside: I have a personal goal of linking it up with categorical ways of thinking about these, e.g. the curry-howard-lambek "isomorphism", I've always been a sucker for redundant ways of seeing the same things I think) The intention behind the question originally was a lot less on the technical side. In other words I think it's obvious to us that what's provable depends on the set of axioms we have, but on the other hand I see a lot of people that e.g. go watch Veritasium's video on foundational mathematics, and they come out with this notion of "absolute unprovability" or even worse "math is subjective", "this proves my god and disproves your god", which I have no idea what any of those are supposed to mean. To be fair, the latter two are kind of crazy, outlier examples, but here's a take from one of my favorite mathematicians Alon Amit, criticizing even Stephen Hawking take on the Godel incompleteness theorem: "The paragraph concludes with "Thus mathematics is either inconsistent or incomplete. The smart money is on incomplete." [quote from Stephen Hawking's article] It isn't "mathematics" that is either inconsistent or incomplete. That statement is meaningless. It is certain (not all) formal systems that are used to analyze mathematical proofs which are inconsistent or incomplete." (If you want to read the rest of the article, it's Alon Amit's post on quora titled "On Hawking's "Gödel and the End of Physics" ". It's also not a one off, you'll find a lot of posts of his going into how much something like the incompleteness theorems get totally misrepresented even by people who work in heavy mathematics, maybe not necessarily foundational maths of course) So to cap this long post, basically although this is quite a lot for something that should be very simple, I think it's something that you might be interested in exploring and clarifying for people not used to thinking this way. At this point you could argue this is moreso epistemology than mathematics (but really, the lines blur, especially in foundational topics ground everything we know so far), but believe it or not a lot of us really suck at despite probably how many proofs we go through in say university. I definitely never had a class on it, I had to learn the hard way.

[@LakanBanwa]

@@dappermink I think at this point I should offer a tl;dr, but basically, just like the other kind people who also devote their time to communicating yet another subject: quantum mechanics have to deal with, foundational mathematics sadly also attracts a lot of woo who misinterpret both communities. Otoh you might even see it as a "glass half full" thing and see opportunity there to cover something about it if you find epistemology interesting. (to me I use it as an excuse to trojan horse in my love of math, but disguise it as something else to not necessarily math people :D )

[@lloydgush]

Is that for 3B1B? Great video!

[@dappermink]

Yeah it was, thanks a lot!

[@tubex1300]

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

[@1.2.3.4..5]

Excellent video

[@dappermink]

Thank you!!

[@encapsulatio]

Is there a book(or multiple books) that's considered gold standard for learning all the logic necessary in type theory that is used in different papers on gradual types, dependent types? Thank you

[@dappermink]

There is this one that I used (HoTT), it introduces the basics homotopytypetheory.org/book/

[@TheRedbeardster]

oh, monsieur, merci beaucoup! :) but what if i need to go deeper and prove, say, the code written in Erlang or anything not related to arithmetics?

[@dappermink]

Haha thanks! I don't know much about this yet since I am very new to the topic, so I wish you best of luck for your online researches if you're interested ( :

[@fourdee3402]

i like this video.

[@KasperDahlTangen]

You actually forgot … -1 = 3 for it to be quickmaths

[@dappermink]

damn you're right :(

[@mr-ubik]

Pronunciation is not an issue actually, just the mic quality, I'd recommend (as others said) to get a good mic

[@harveyroper5526]

i’m stuck around the 5:23 mark. What exactly do you mean by a ‘proof of proposition A’ like more specifically what are you saying?

[@dappermink]

That's the tricky and mindblowing part: There is a perfect correspondance between types/inhabitants and propositions/proofs Say you have a type A, it corresponds to a logical proposition. If you can find an inhabitant of A, then this inhabitant corresponds to a proof of the corresponding logical proposition. As a trivial and non interesting example, the type "bool" corresponds to the logical proposition "there exists a boolean". You are able to construct an inhabitant of bool: for example "true" has the type bool. Therefore, using this analogy, it means "true" is a proof of the proposition "there exists a boolean", and indeed that makes sense since providing true which is a boolean effectively proves there exists a boolean. Now that may not seem interesting since bool is a type you can always construct, so I will give a second more interesting example: A -> B is a the type of functions that takes as input inhabitants of A and returns inhabitants of B. For example f(x) = 2x is an inhabitant of the type R -> R. This type also corresponds to a logical proposition: it corresponds to "A implies B" which in logic means "If you have A, then you also have B". As an example I will define A to be "It's raining" and B "The ground is wet" "A -> B" therefore corresponds to the proposition "if it's raining, then the ground is wet" So how could be prove such a proposition: well, as said earlier we just need to find an inhabitant of this type, namely a function that takes as input an inhabitant of A and outputs an inhabitant of B. In other words, such a function will take a proof that it's raining and provide a proof that the ground is wet. It's like a machine that can prove the ground is wet if you already know it's raining, so having such a function is indeed a proof that you have the implication "if it's raining then the ground is wet". Suppose you have "a : A" (a proof of A), then using your function "f : A -> B" (a proof that A implies B), then by applying "a" as a parameter of the function "f", you can get "b := f(a) : B" (a proof of B). What I just did there is the equivalent of the modus ponens which is an inference rule in logic that states if you have A and A implies B, then you can deduce B. There are type equivalences to every logical proposition you can think of, so if you want for instance to prove the infinitude of primes, then there exists a type that corresponds to "there are infinitely many primes" and if you want this proposition to be correct you will need to find an inhabitant of this type. As a last example, "1+1=2" and "1+1=3" are both types that exist. However, while it's possible to find inhabitants of the former, it's impossible to find any inhabitant of the latter (meaning the first proposition is provable but the second one is not). I hope I could clarify a bit this analogy that just took me way too long to understand personally.

[@harveyroper5526]

​@@dappermink Thank you for the explanation. I have some familiarity with propositional logic, am I correct in saying that when you say a is some proof of A, it is equivalent to proving the existence of some object a which satisfies A? I thought the way you draw the parallel between logic and type theory to be really interesting and made a lot of sense. I would have liked it though if you had been more delicate with your explanation of logic, since despite having studied logic, I found myself a little lost by the assumptions that you were making. Otherwise fantastic video, and thank you for the further explanation!!

[@dappermink]

@@harveyroper5526 Yeah you're entirely right (as for how I understand it). This parallel is named "propositions as types" which is a special case of the "Curry-Howard correspondence" if you're interested. Yeah, I'm sorry it was kinda hard to explain for me. Thank you so much!

[@harveyroper5526]

@@dappermink I will have to look into that. All the best :)

[@a0um]

Is there any book you’d recommend to self-study type-theory?

[@dappermink]

I personally read Homotopy Type Theory (HoTT) but it is not only focused on type theory and since this is the only book I'm reading, I don't really know if there are better ones, sorry

[@NoNameAtAll2]

since you do talk about Lean, maybe cover "Natural Numbers game"?

[@dappermink]

Didn't know it, it's amazing! Thanks!!

[@Kram1032]

Very nice but you probably also want to explain what you are doing during the Lean coding section as the notation is different from what you did in the video up to that point

[@dappermink]

Thank you! You're right, I should have done that. I will maybe do videos dedicated to Lean in the futures anyway (if I can find a way to improve the audio haha)

[@esquilax5563]

Hmm, type theory always seemed to me to be making simple things unnecessarily complex, and this video hasn't dispelled that impression. I've still subscribed though, I'm curious to see what else you have to say about it!

[@dappermink]

Thank you! Type Theory is a math foundation, it doesn't seem more complicated to, say, ZFC, if you've seen how numbers are defined in this theory. As I understand it, the benefits of Type Theory are among other things, the fact they use the same language for the logic and the maths, and that it's easier to implement it in proof assistants, since you just need to make a function in a typed language to prove a theorem. In my opinion, set theory seems more like... just an encoding: using sets to encode concepts. Think of the formal definition of a function for instance. On the other hand, the type theory definitions seem much more intuitive and direct. Really, just compare the positive integers definition in set and type theories

[@davidwild2962]

How numbers are represented here, reminds me of lambda calculus

[@mlliarm]

A really nice video thank you. The only negative I found was the sound. I think you might need a better microphone.

[@munol2524]

your way of speech sounds similar to Professor Altenkirch who covered Type Theory on Computerphile. Are you two the same person ?

[@MCRuCr]

I think in type theory, there is no Bool Type. Instead true is defined as the Unittype (which has one instance I guess) and false is defined as the EmptyType (that has no instance)

[@Xayuap]

isn't = a function that takes two numbers and maps to a Boolean? N × N -> B

[@dappermink]

In most programming languages, yes. But that's not what we want here: We want a type for every possible equality (1+1=2, 5=42, x+4=0, ...) and we don't want it to be reduced to a boolean that tells us if the equality stands or not yet. Instead we want to have a constructor for all equality types that are true, but only for these ones. So we want to be able to find elements of the type "1+1=2" (such elements would be proofs that "1+1=2") but we want it to be impossible to find elements of the type "5=42" meaning it's impossible to prove that "5=42". What's important with that approach is that we're then able to prove propositions including equalities with variables such as "for all x, y in Nat, x+y=y+x". That's a proposition that is true, and so also a type that has inhabitants. If the equality returned a boolean instead, we couldn't write this proposition since "x+y=y+x" would then just be an alias for either true or false depending on your definition. I'm not sure if that can help you understand it better, but I hope it does!

[@arnaudparan1419]

the video is great but the sound quality is not great, it might help you to use a pop filter. Also a better quality mic would be really nice.

[@dappermink]

Thank you! Yeah I am really sorry for the poor audio quality, I will definitely need to improve that for future videos, so thanks for thr advices!

[@cmilkau]

The real Gödel theorem is that his results may never be quoted correctly. It is absolutely possible to prove the consistency of theories and has been done several times. What Gödel proved is that you cannot use a theory (powerful enough to include arithmetics) to prove its OWN consistency. You need a more powerful theory, which obviously could be inconsistent itself.

[@dappermink]

I know, that's exactly what I wrote on the video but I simplified what I said because I didn't want to talk about Peano arithmetics without explaining what it is and those details didn't feel that important for what I wanted to explain here so I chose to leave them only on the video as text.

[@abdelhakimakodadi3073]

Oh, 3blue1brown has become 1blue1white1red :P

[@dappermink]

Shit, my secret identity is not that secret anymore 😢

[@abdelhakimakodadi3073]

​@@dappermink From a pie chart to a stack bar chart lol. Nice video btw, keep em coming

[@Xayuap]

¿did you define what is + of types?

[@dappermink]

No I only defined the sum (+) of Nats

[@artey6671]

1:51 How does that make sense? 1+2P mod p ist 1, so (1+2P)/p is never an integer, so that sin is never 0, so the product is not 0.

[@dappermink]

If 1+2P is a prime number, then it's just one of the p's, and if it's not, then that means it is divisible by some prime number p. In either case, the fraction is gonna be one for at least one of the p's. Your observation is also correct. That's why we have a contradiction. (yeah it's a really convoluted proof that hides its details but at least it fits on the screen 😅)

[@artey6671]

@@dappermink Well, in the latter case the fraction would never be 1, but some integer, which is all we need. Still, that's the most awkward way of writing it. It's kind of a predicate logic statement translated into numbers. I'm not sure whether that's smart or just silly. But there's a relation between \pi and prime numbers, so maybe \pi would be an integer if there were only finitely many primes, so the product being positive could be wrong. ;)

[@artey6671]

@@dappermink Don't mind what I said about \pi being an integer, it probably is unrelated.

[@dappermink]

@@artey6671 Well, that's just a weird way to encode the supposedly finitude of primes into a number, and then showing this number can't exist. \pi and \sin just seem to help making this encoding haha

[@Aesthetycs]

It is not clear to me at the end how come you presume the type of 2+2 and the type of 4 to equate.

[@dappermink]

That is because, by definition, 2+2 and 4 both reduce to the same expression: 4 = s(s(s(s(0)))) 2+2 = s(s(0))+s(s(0)) =s(s(s(0))+s(0)) =s(s(s(s(0)))+0) =s(s(s(s(0)))) That's kinda as if 2+2 were just an alias for 4 in this theory. Though I agree that's not the best example I could have chosen...

[@Aesthetycs]

@@dappermink Thank you for kindly replying to my first comment on KZbin. I appreciate it.

[@dappermink]

@@Aesthetycs No problem at all haha

[@johndebord7802]

1:07 is Gödel contradicting himself?

[@dappermink]

No, he's just proved that if a system can prove his own consistency, then it implies some contradiction. I'm not sure to understand what you're asking, tell me if I don't get it

[@johndebord7802]

@@dappermink Our English language is a system, therefore there's no way to prove what Gödel is trying to prove?

[@dappermink]

@@johndebord7802 As far as I know, he proved it into the Peano system, not English, so any system that includes Peano arithmetics is either incomplete or inconsistent (or both).

[@kyspace1024]

The final example is too trivial that I am afraid if I have never used Refl myself I will totally lose the point.

[@dappermink]

I guess you're right, I should have shown how to proof that a+b = b+a but that would have been way longer Or maybe the modus ponens?

[@TheWonderfulMageofOz]

MOAAARRRRR

[@gamekiller0123]

Axioms are not arbitrary. You can do mathematics with any axioms, but you can't do interesting mathematics with any axioms, and you can't do useful mathematics with any axioms, and you can't do understandable mathematics with any axioms.

[@dappermink]

Yeah, humans prefer using axioms they can make use of and that are easier to reason about. But my point for the video was just that anything is technically ok as long as they don't let you conclude some contradictory statements.

[@MCRuCr]

1:51 is that a valid proof for infinite primes? Does not make any sense to me

[@dappermink]

It is haha, there is a video explaining it if you want: kzbin.info/www/bejne/Y6eZqoOqgpmJgqM

[@MCRuCr]

@@dappermink thank you 😊

[@peterwaksman9179]

You obfuscated at the key moment of 2+2.

[@thegamechanger7157]

Your bullying me, I can't do Js. I will make Jarvis, and make it program for me

[@kaiserouo]

I am taking a course of Introduction to Computational Logic this semester, and this video would a very good addition to what I just learnt. Actually, if I didn't take that class, I would not have a single idea what this whole thing is about...

[@dappermink]

Thank you! I wish I had courses covering this topic, or at least something close haha

[@mrl9418]

"Because we're basically insatiable and we'll gobble up whatever mathematical theory that comes our way." How about that? Video would be too short, I have to admit 😁

[@thetrickster9885]

Bro r u franceh

[@dappermink]

I am haha

[@thetrickster9885]

@@dappermink nice your video are really good. Keep it up man. 😎👍

[@dappermink]

@@thetrickster9885 Thanks a lot! : )

[@k_meleon]

tu es francais ?

[@dappermink]

Évidemment 🙃

[@danhabib3441]

Merci 😂

[@sharan9993]

bro ur voice has a lot of dispersion. It is hard to hear anything. Change it.

[@miro.s]

Great video, but hard to follow due to pronunciation. It would help to include English subtitles.

[@dappermink]

I know, I apologize for the audio quality and my accent. But I did add English captions!

[@laurenpinschannels]

wow. fucked up iff true...

[@Eknoma]

Imagine being French

[@herrefaber999]

Bad sound, bad voice, bad accent. Don't watch.

[@humanperson2375]

I can't watch this. I'm sorry, but I can't understand half of any sentence

[@dappermink]

I'm sorry, both my English accent and my microphone are catastrophic. I added English captions though if that can help.

[@azzteke]

Terrible accent, terrible quality.

[@itsmeagain1415]

dafak??? terrible quality??

[@itsmeagain1415]

oh! you mean the mic? yeah that's a problem😬

[@syllight9053]

stfu, this person is trying to help people learn math. At least be grateful for that P.S: Use the captions

[@3a146]

If I were to fit the 4 corners, I would do ≡, U, ∑, ∏.

[@cloudy_luna]

Great video!

[@nilp0inter2]

Great video!

[@dappermink]

Thank you!