今回は、Agdaというプログラミング言語で、
自然数と足し算を作っていきます。（※１）
ゲーム世界の神様になるような箱庭的要素がありますので、そういうゲームをやる人も、楽しめるんじゃないかなと思っています。
つまり、登場人物とその登場人物同士の関係、みたいのを自由に設定できます。
今回であれば、
・登場人物：自然数
・関係：足し算
みたいな位置づけです。
そういう関係（足し算）を定義したら、何か法則性（定理）が見えてくる、
そういうのは証明できるかもしれないので、やってみよう。という流れになります。
前回話題に上がった、
(3 × 4) + (3 × 5) = 3 × (4 + 5)
みたいなやつですね。
上の定理を証明するには足し算だけでなく、掛け算も定義することになってきます。今回は自然数と足し算の定義のみです。（※２）
次回は、足し算に関する証明をいくつか行う予定です。
(★追記)
第一回終了時のagdaファイルと、この一連のAgda関連の動画を見る際に最低限必要になるSpacemacsのコマンドについてのファイルを用意しました（https://polymony.net/wp-content/uploads/2019/06/agda2ndSource.zip）
第二回のファイルも一緒に入っています。良ければ参考にしてみてください。
（※１）
動画の視聴者として想定しているのは、
①Spacemacsを導入(※３)していて、Vim操作を選んでいる人、
②vimの操作に全然慣れていない人、
です。この動画をつくるに至った動機が、
パソコンで数学の定理を証明するって何か面白そう、
でもAgdaって何？そもそもプログラムとかもよくわからない、
という人にもAgdaを一度触ってもらいたい、というものだからです。
本当は、小中学生向けにもっとレベルを落としたものにしたかったですが、
最初はこのレベルで、と言った感じです。
なので、
（１）emacsに慣れている人
（２）vim操作に慣れている人
からすると、途中でちょいちょい入る、
操作関連の説明がまどろっこしいかも知れませんが、
暖かい目で見ていただければと思います。
（※２）
動画では自分流で足し算を定義しましたが、
他のやり方も当然ありえます。
すなわち、
m + zero = m
m + succ n = succ (m + n)としていますが、
zero + n = n
(succ m) + n = succ (m + n)
としても良いはずです。
神(プログラマ)が思うがままに世界を構築、みたいな壮大な感じがします。
事実として、こういうのを学者さんも宇宙（universe）と表現するみたいです。
今は自然数と足し算だけですが、だんだん増やしていく予定です。
注）動画でのwhereの説明が不正確な気がしました。「ここで、以下の通りとなっている」、という程度が正解ですね。
natとは以下の通りである、ではなく、
natはSetという型を持つ、ここで以下の通りとなっている、すなわちnat型のzeroというものが存在し、nat -> nat型の関数succというものが存在する、というのが正しいと思います。
読むときの心の動きとしては、nat : Setと見て、Setは知っている（説明してませんがSetはAgdaの標準ですでに定義されています。）が、natってなんぞ？初見だぞ？という印象を持ったところに、その後whereがきて、その下を読むと、ああ、natはzeroとかsuccてので作られるんだな、メモメモ、という流れになります。
（※３）
spacemacsでAgdaをやれる環境の構築については、ここ（https://polymony.net/2019/05/16/07-installationofagda/）で紹介しています。良ければ参考にしてみてください。Agdaの公式サイトは(https://wiki.portal.chalmers.se/agda/pmwiki.php)です。