# 카네기 멜론 HoTT 강의

수학기초론에 흥미를 가지면 HoTT의 이름 정도는 듣게 되지만, 막상 공부를 시작하려면 상당한 허들이 있다. 참조할 수 있는 텍스트는 2년 전에 나온 레퍼런스 뿐이고, 명확한 prerequisite 가이드라인도 없는 상태.

여기 어려움을 느끼는 사람이라면 유용한 자료 하나. 카네기 멜론 Robert Harper 교수의 HoTT 강의인데, 이제 막 보기 시작한 참이지만 평소 궁금하던 많은 부분들을 해결해 준다.

밑은 1강에서 흥미로운 몇 구절의 발췌.

Although it’s called homotopy type theory because its motivations come from homotopy theory… it really is a self standing subject, it’s not really tied to algebraic topology, and what it really is is a somewhat sophisticated analysis of the concept of equality in constructive type theory.

딱 걱정하던 부분. 다행히 대수위상부터 배워야 하는 끔찍한 진입장벽은 아닌 듯.

It’s not arbitrary which assumptions you deny. (Chuckle) It’s all founded on the notion of construction. And if you think through carefully, “what is the idea of a proof?”, for example, from the perspective of the notion of construction, then you will be inevitably, irreversibly led to question the universal validity of the Law of Excluded Middle. And then, you are a constructivist.

구성주의 변론도 비중있게 다루는 모양.

What type theory is, is the Grand Unified Theory of Computation. It’s all about communication, it’s all about language, it’s all about what programs exist… They’re all about computation. It is what programming languages is. That’s the first thing. There’s nothing else. There is nothing else. We’re just studying type theory. So eventually, all the arbitrary programming languages are going to be just swept away with the oceans, and we will have the permanence of constructive intuitionist type theory as the master theory of computation, without doubt in my mind. No question.

이렇게 출사표가 호쾌한 프로그램은 역사적으로 끝이 좋지 않았다는 인상이 있지만 (…) 무엇을 근거로 이런 자신감을 갖는 것인지는 꽤나 기대가 된다.

Like what you read? Give \ a round of applause.

From a quick cheer to a standing ovation, clap to show how much you enjoyed this story.