そもそもそれは既存の基礎の問題であって……という話を「長い目でみれば」というの良いな
めっちゃ面白い質問飛んでてすごいな
圏論飽きた……（おい）
HoTT やりたくなってきた
よく見えないけど講演者が Emacs で PDF を開いている？
対位法の規則の定義があんまり構成的じゃなさそう（有限的なので問題なし）
zero-based でないことで顰蹙を買いまくっている音楽の度数
仕様 (specification) があるならなんでも依存型理論で書けるっしょみたいな精神なのかな……
「音楽理論は Agda のプログラミングをする中で勉強した程度なので……」←！？！？
音楽の話が始まった
