[Intro to HoTT - OLD] Martin-Löf Type Theory: Speaking the Language
ฝัง
- เผยแพร่เมื่อ 25 ก.ค. 2024
- Video 0 of the Martin-Löf Type Theory lecture, part of the Introduction to Homotopy Type Theory video lecture series. Introduces formal languages & deductive systems, and establishes the key intuitions behind homotopy type theory.
This lecture series roughly follows Egbert Rijke's forthcoming textbook, Introduction to Homotopy Type Theory, which is expected to be released in 2021 by Cambridge University Press. More information can be found here: ncatlab.org/nlab/show/Introdu....
Some relevant resources:
- Article about Mochizuki's purported proof of the ABC conjecture: www.quantamagazine.org/titans...
- SEP article on intuitionistic logic: plato.stanford.edu/entries/lo...
- nLab article on spaces (more technical): ncatlab.org/nlab/show/space
![[Intro to HoTT - OLD] Martin-Löf Type Theory: Judgments, Contexts, and Types](http://i.ytimg.com/vi/9cR2Day-4Bk/mqdefault.jpg)
![[Intro to HoTT - OLD] Martin-Löf Type Theory: Judgments, Contexts, and Types](/img/tr.png)
![Was soll HoTT? [Intro to HoTT, No. 0]](http://i.ytimg.com/vi/Pu16iodESTU/mqdefault.jpg)
![[Categories] Theory of the Category of Sets: Sets and Functions](http://i.ytimg.com/vi/BlmGMRi8k-c/mqdefault.jpg)
I've rebooted this video series, over at th-cam.com/play/PL245PKGUDdcN9-El9D7DRefwX4c9feiYq.html. Check out there for more content about HoTT!
This is great! I learned a lot in these first two videos. I hope you continue to make more
Seems like these two are the only ones we'll get :(
This is such a good video series!! Thank you!!
I also hope you get back to doing more of these. Thank you!
Very clear and helpful. Thank you!
Bravo! This is amazing.
A beautiful introduction ❣️
Very clear. Thx!
Amazing!
Bless you sir
Great video
Could you explain the terminological difference between “Propositions” and “mere Propositions” as alluded to in HoTT book?
Python be like
>if purple:
At 11:35, isn't judgmental equality taken to mean that x and x' have the same VALUE with respect to some notion of value, for example, that they will reduce to the same canonical value term, not that they are necessarily the same TERM?
16:36 Wouldn't an uninhabited proposition type simply be unprovable and not necessarily false?
I think even weaker than that, “unproven” not “unprovable”.
@@bhz8947 If one proves that there *cannot exist* any terms of type T then T is actually unprovable.
True/false vs provable/unprovable are _more or less_ different terminologies for similar things.
@@psttf Different things.
Hallo Thomas
Why this video is marked as "OLD"?
Because I've discontinued this series. My new HoTT videos are at th-cam.com/play/PL245PKGUDdcN9-El9D7DRefwX4c9feiYq.html
@@jacobneu-videos Thank you for the answer. I want to watch all this materials, but probably I won't be able to watch it regularly.
"if-then-else" construct? I see no "then," only "if" and "else." Of course, I already know the construct, but I got the impression you aimed this video at a different audience.