Proof Summit 2012

ヽ|・∀・|ノ @i_am_a_youkan

わたしのPDF,Acrobat以外の何で読んでも、日本語が表示されない(絶望　わたしのPDF,おかしすぎっ！？

ヽ|・∀・|ノ @i_am_a_youkan

めんどくさくなったので、Google docsでいいやという結論になった。今日のスライド:homotopy type theory for coq programmers https://t.co/uiLglI5I ちなみに贈与税の基本控除は110万円らしい

ヽ|・∀・|ノ @i_am_a_youkan

まあ、HoTTが30分で分かるわけない！(怒

ヽ|・∀・|ノ @i_am_a_youkan

割と辛い質問だった　＞　さかいさん「mao さんはこれを使って何をしようとしてるんですか？」

ヽ|・∀・|ノ @i_am_a_youkan

14時に起きたけど、もう眠い

病気の美少女 @lyrical_logical

懇親会お薬ききはじめるまで死に体ですみませんでした… #proofsummit2012

oto @oto_oto_oto

@maophilia らしくない。いつもは余るんちゃうかなって言ってるのに。

ヽ|・∀・|ノ @i_am_a_youkan

今日口頭で話したbicategoryのcoherenceとか。多分書いてる人あんまりいないので。ついでに、さかいさんに質問された"=="の定義も合わせて　https://t.co/j89JVHSs　

ヽ|・∀・|ノ @i_am_a_youkan

@oto_oto_oto 30分は無理だった。1時間は必要やったな

oto @oto_oto_oto

リベンジHoTT

ヽ|・∀・|ノ @i_am_a_youkan

次はdifferential geometry for Coq programmersとかいうネタを RT@oto_oto_oto リベンジHoTT

ヽ|・∀・|ノ @i_am_a_youkan

自分の中で自明すぎるくらい自明なことを何故他人に自明なこととして伝えられないのか

oto @oto_oto_oto

@maophilia 小林昭七追悼という冠つけて二時間番組でお願いします。

erutuf @erutuf13

@masahiro_sakai おお、そのほうが関数型とかの人に受けが良さそうですね。

erutuf @erutuf13

HoTT、n Category Cafe にいろいろ載ってたと思うから眺めよう

Κeіsuke Νakanο @ksknac

@erutuf13 @masahiro_sakai 私も素因数分解というよりは，Knuth-Bendix みたいなものだと認識しています．その方が一意性の意味が理解しやすいですし．

erutuf @erutuf13

斜め読みした限りでは読み易そうだ http://t.co/mKOtS9qR

erutuf @erutuf13

なんか自分の agda フォルダに HoTT っぽいコードが落ちてたんだけどなにも記憶が無い