Summer of Math Exposition

I think this video would be very hard to understand, especially all the notation, without already being steeped in the language and culture of type-theory/theorem-provers/category-theory. Something like the first video in this YouTube series by jacobneu was more understandable to me.

This video simultaneously convinced me that type theory would be an interesting thing to learn about, and that I should seek out a different way to learn about it. It seems like there are a lot of really transformative ideas here which you kind of blow through very quickly: it’s telling that this is a video about types, identity, and equivalence, and that I also came away with almost zero actual understanding of the precise meaning or definition of “type,” “identity,” or “equivalence.”

Thanks for the video, but I think in the future you might want to do more reflection on what this sounds like to someone who hasn’t done this kind of math before.

I found the arguments really hard to follow. It is not clear what are the assumptions, what is being proven, and where in the proof we are, whether the proof is done or in some intermediate step.

it made me feel overwhelmed at times. video description suggests its an introductory video but the amount of information can feel overwhelming for some. if I had not been familiar with the topic I think I would not learn much after watching it. but i think its great video for someone who needs to quickly refresh his memory about the topic

I put a score at 5 only to input a comment, that I hope will be useful for the contributor, whose effort is noticeable : for such an abstract topic, I would say that the motivation should be clearer / much more emphasized. The thing is to catch the spectator to give him a reason to keep atchning. (also : volume is low, that’s a minor thing but that does not help)

The video assumes a lot of prior knowledge.

I really enjoyed your visuals; the drawings were illuminative and well-done. The volume level was a bit low; I had to turn things up quite a bit to pick up clearly what was being said. I think it would’ve helped the video a lot to spend some more time talking about what a type is, maybe with more examples, before diving into NNOs, the connections between types and topology, etc. There were also a few spots where things were implicitly assumed that might have been useful to make explicit: for instance, in the definition of addition, even if the viewer is expected to know what currying is (which is a reasonable assumption!) it’s a good reminder to note that there’s some currying going on there in the definition, since the type was N->(N->N) rather than (NxN)->N. Overall, though, I thought this was a fine video and it definitely encouraged me to do more diving into HoTT (which has been backburnered for quite a while now). Keep it up!

Good stuff, but waaaaay to fast! I mean those who heard about HoTT before could find this enlightening. Otherwise, the content needs to be unpacked in several videos.