Wow thanks for this video!! I walked through it slowly and I think I finally understand the notation in Martin-Löf type theory and I think I'm more prepared to understand related ideas like the lambda calculus! What I'm stuck on now is understanding "what we get out of" the computation rules. Like, in the programming interpretation, it seems intuitive that we want to be able to apply lambdas (beta rule) or the language won't be very useful. But I don't know how to say that more formally, or how to think about the eta rule. And in the logic interpretation, I have no idea yet what we get out of "judgmental equality" between elements. Excited to try to figure more out from here!
Great video. Why do the rules only let us form application terms when the contexts of the function and argument are equal? If the contexts are different, is there a way to merge them together to allow the application?
If one context is an extension of the other (or if both are extensions of a context in which the function & argument can be expressed) then we can make sense of it. This is can be deduced from the rule as stated here. But in general, there's no "context merging" rule
![Noughts & Crosses: Set Interpretation [Intro to HoTT, No. 5, Part 0]](http://i.ytimg.com/vi/cw2ZhHWnGXE/mqdefault.jpg)
![Noughts & Crosses: Set Interpretation [Intro to HoTT, No. 5, Part 0]](/img/tr.png)
![Logic & Lambdas: Constructive Modus Ponens [Intro to HoTT, No. 4, Part 0]](http://i.ytimg.com/vi/iaMIT5lL1nc/mqdefault.jpg)
![Booleans in HoTT: Putting Bool to Use [Intro to HoTT, No. 3, Part 1]](http://i.ytimg.com/vi/2d6Ag7uPnlI/mqdefault.jpg)
![ILLSLICK - KILLSHOT REMIX [FULL VERSION]](http://i.ytimg.com/vi/RIK8RrqIAzE/mqdefault.jpg)
![Three for One: Logic Interpretation [Intro to HoTT, No. 1, Part 3]](/img/n.gif)
Amazing content please continue, and it would be nice if there were more homotopy explanations
Thanks! And yeah, next video's gonna be based on the homotopy interpretation
wow I love you for this wonderful series ! Thank you so much
Wow thanks for this video!! I walked through it slowly and I think I finally understand the notation in Martin-Löf type theory and I think I'm more prepared to understand related ideas like the lambda calculus!
What I'm stuck on now is understanding "what we get out of" the computation rules. Like, in the programming interpretation, it seems intuitive that we want to be able to apply lambdas (beta rule) or the language won't be very useful. But I don't know how to say that more formally, or how to think about the eta rule. And in the logic interpretation, I have no idea yet what we get out of "judgmental equality" between elements. Excited to try to figure more out from here!
For introduction rule for beta I suggest providing the type for the conclusion of the inference rule.
What does the expression λx.f x mean at 14:36, when x has not been defined in our context like with the λ-abstraction and β-reduction rules?
Great video. Why do the rules only let us form application terms when the contexts of the function and argument are equal? If the contexts are different, is there a way to merge them together to allow the application?
If one context is an extension of the other (or if both are extensions of a context in which the function & argument can be expressed) then we can make sense of it. This is can be deduced from the rule as stated here. But in general, there's no "context merging" rule