Windows10環境での、Agdaのインストール手順を動画にしました。
Agda本体とそれ用のエディタ(Spacemacs)をインストールしています。（※１）
(追記：実際にプログラミングしている様子を動画にしました。一度見てみて面白そうだったらインストールしてみるというのもありだと思います。(https://polymony.net/2019/05/26/post-536/)
HaskellとかLinuxとかEmacsという単語がピンとくる人は、
公式のAgdaWiki(https://wiki.portal.chalmers.se/agda/pmwiki.php)
を参考にして、ご自身でインストールをすることをお勧めします。
つい最近でしょうか、Windows向けのインストーラが公式に用意されてワンクリックで導入できるようになってました。
自分で苦戦してインストールするのは、それはそれでいい勉強とも思えますが、
こうやって公式が敷居を下げてくれるのは、良いことだと思います。
次回は、英語文書に第一の製作物（PDFリーダー）を適用した実況動画をご紹介します。Agdaで実際にどうプログラムを書くかについては、その次の回にご紹介する予定です。
（※１）2019年5月現在では、公式はエディタとしてEmacsを指定しています。この動画で紹介したSpacemacs(http://spacemacs.org/)は、Emacsの強くてニューゲーム？版です。良い点としては、
①最初からいい感じのEmacsの設定を導入してくれています。
②パッケージについても、動画のように設定ファイルに少し書けば、次回起動時にインストールしてくれます。動画ではagdaと一行追加しました。
③見た目がかっこいいです（VS Codeみたいな）。
④vimというエディタのキーボード操作（キーバインド）を最初から導入できます。動画でも最初の起動時にvimと入力しています。
Emacsやvimは、学習コストの高いエディタのようです。ただ、長期的に見ればマスターしといたほうが良さそうです。
ゲーム的な楽しさがある一方で、日々上達している感が得られるスポーツ的な要素があります。
Agda以外の他の言語であれば、VSCodeとか他にも良いエディタが存在します。しかし、Agdaは公式の指定するEmacs以外の選択はなさそうです。
学習コストを気にすることなくEmacs（Elisp）やVim操作を習得できる良い機会と思っています。