Really enjoying this video series so far. Coming at this from a professional software engineer POV with a casual interest in mathematics, it's easy to follow (thank god you didn't go too deep on topology or else I'd be lost). Never even occurred to me that type systems could be used for something this powerful.
Yep! I must've done something wrong in the installation, since C-c C-l is the only command that works, but the others can be accessed through vscode's command entry system, which is what I do in this video
![Formalities & Informalities: HoTT Workflows [Intro to HoTT, No. 2, Part 0]](http://i.ytimg.com/vi/-QKLxN1_nvk/mqdefault.jpg)
![Formalities & Informalities: HoTT Workflows [Intro to HoTT, No. 2, Part 0]](/img/tr.png)
![Three for One: Programming Interpretation [Intro to HoTT, No. 1, Part 1]](http://i.ytimg.com/vi/VnO2-ynvDsw/mqdefault.jpg)
Really enjoying this video series so far. Coming at this from a professional software engineer POV with a casual interest in mathematics, it's easy to follow (thank god you didn't go too deep on topology or else I'd be lost). Never even occurred to me that type systems could be used for something this powerful.
I love these! The teaching is so down-to-earth
this series is perfect, been a while reading about CT/HoTT and this is one of the best videos i have seen. keep going,!! thanks you
This is exactly what I was looking for. It clicked at 8:26. Thanks so much!
dude it`s just awesome how simple you make this topic
Russian occupants tortured my friend Ivan
@srghma sorry to hear that, it wasn't me btw
omg, 1 being like "the"? *chefs kiss*
Awesome series! Looking forward to more videos
Hell yeah, time to have my mind blown again
Thanks a lot this is a great video 👍
Are you using the VScode agda-mode ?
Yep! I must've done something wrong in the installation, since C-c C-l is the only command that works, but the others can be accessed through vscode's command entry system, which is what I do in this video
That was an awesome video, thank you @jacobneu-videos . It would be great if you could publish more example content using agda and vscode
nice, do more pelase
yes
Gonna swim in -the- a Specific Ocean
Is the type "exists n : n > 2 and n^2 = 2^n" the same type as unit?
Yes, for the appropriate notion of "the same type"
Cool!
This thumbnail is a bit tough to distinguish from the last one, so I skipped over this at first. Maybe I just need more coffee.
Thanks for mentioning that. Maybe I'll make it more distinct somehow