安野貴博・黒岩里奈・片石貴展・岸谷蘭丸(敬称略)の飲み動画、なんなんだ(なんなんだも何もないのだが)
眠い
臆病なので誰も見ていない場所で好き勝手に言うのが楽しい(X は本人に届いてしまうのでこわい)
代数と幾何は双対だよね~という雰囲気だったのに唐突に型は空間ですとか言い出すのやっぱり HoTT おかしいよ……と思ったけど位相的意味論もそうか
そもそもそれは既存の基礎の問題であって……という話を「長い目でみれば」というの良いな
めっちゃ面白い質問飛んでてすごいな
圏論飽きた……(おい)
HoTT やりたくなってきた
よく見えないけど講演者が Emacs で PDF を開いている?
対位法の規則の定義があんまり構成的じゃなさそう(有限的なので問題なし)