hwk3

.envrc

@@ -0,0 +1,9 @@
+use_flake() {
+    watch_file flake.nix
+    watch_file flake.lock
+    eval "$(nix print-dev-env --profile "$(direnv_layout_dir)/flake-profile")"
+}
+
+mkdir -p .direnv
+
+use_flake

.gitignore

@@ -30,8 +30,9 @@ Gemfile.lock
 
 ## Emacs files
 auto/
+\#*\#
 
 ## Misc build files
 out/
 *.zip
-versions/plfa.github.io-web-*/
+versions/plfa.github.io-web-*/

.gitmodules

@@ -1,3 +1,3 @@
 [submodule "standard-library"]
 	path = standard-library
-	url = git@github.com:agda/agda-stdlib.git
+	url = https://github.com/agda/agda-stdlib.git

.vscode/settings.json

@@ -0,0 +1,7 @@
+{
+  "editor.fontSize": 15,
+  "vim.insertModeKeyBindings": [
+    { "before": ["k", "j"], "after": ["<Esc>"] }
+  ],
+  "editor.fontFamily": "\"PragmataPro Mono Liga\", \"Roboto Mono\", 'Droid Sans Mono', 'monospace', monospace, 'Droid Sans Fallback'"
+}

README.md

@@ -101,7 +101,7 @@ PLFA ships with the required version of the Agda standard library, so if you clo
 If you forgot to add the `--recurse-submodules` flag, no worries, we can fix that!
 ```bash
 cd plfa/
-git submodule update --recursive
+git submodule update --init --recursive
 ```
 If you obtained PLFA by downloading the zip archive, you can get the required version of the Agda standard library from GitHub. You can either clone the repository and switch to the correct branch, or you can download the [the zip archive][agda-stdlib]:
 ```bash

emacs/init.el

@@ -0,0 +1,26 @@
+(require 'use-package)
+(require 'use-package-ensure)
+(setq use-package-always-ensure t)
+
+(use-package evil)
+(use-package agda2-mode)
+(use-package gruvbox-theme)
+
+(setq evil-undo-system 'undo-tree)
+(require 'evil)
+(evil-mode 1)
+
+(load-theme 'gruvbox t)
+
+(menu-bar-mode -1)
+(tool-bar-mode -1)
+(toggle-scroll-bar -1)
+
+(load-file (let ((coding-system-for-read 'utf-8))
+                (shell-command-to-string "agda-mode locate")))
+
+(setq auto-mode-alist
+      (append
+        '(("\\.agda\\'" . agda2-mode)
+          ("\\.lagda.md\\'" . agda2-mode))
+        auto-mode-alist))

flake.lock

@@ -0,0 +1,77 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "locked": {
+        "lastModified": 1631561581,
+        "narHash": "sha256-3VQMV5zvxaVLvqqUrNz3iJelLw30mIVSfZmAaauM3dA=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "7e5bf3925f6fbdfaf50a2a7ca0be2879c4261d19",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1634090417,
+        "narHash": "sha256-GGRQSC+dBFtynnwHCG65bdzygXK058NJ92boHGXz8Gg=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "c9ddb803ce95c0ec2ab4d57ba29f136b8ce9fe71",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-agda": {
+      "locked": {
+        "lastModified": 1624913309,
+        "narHash": "sha256-HHZTzHgLuoOmTrHckl9eGG8UWTp32pYXmCoOjgQYIB4=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "860b56be91fb874d48e23a950815969a7b832fbc",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "860b56be91fb874d48e23a950815969a7b832fbc",
+        "type": "github"
+      }
+    },
+    "plfa": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1628614312,
+        "narHash": "sha256-e5wLKKjabrZesjAd5p5sXeYW28LXoZPGY2jp6cnB9qM=",
+        "owner": "plfa",
+        "repo": "plfa.github.io",
+        "rev": "8fec0eb208e48401908414347d060767af48309f",
+        "type": "github"
+      },
+      "original": {
+        "owner": "plfa",
+        "repo": "plfa.github.io",
+        "rev": "8fec0eb208e48401908414347d060767af48309f",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs",
+        "nixpkgs-agda": "nixpkgs-agda",
+        "plfa": "plfa"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,69 @@
+{
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs";
+    flake-utils.url = "github:numtide/flake-utils";
+
+    nixpkgs-agda.url = "github:nixos/nixpkgs?rev=860b56be91fb874d48e23a950815969a7b832fbc";
+    plfa = {
+      flake = false;
+      url = "github:plfa/plfa.github.io?rev=8fec0eb208e48401908414347d060767af48309f";
+    };
+  };
+
+  outputs = { self, nixpkgs, nixpkgs-agda, flake-utils, plfa }:
+    flake-utils.lib.eachDefaultSystem (system:
+    let
+      pkgs = nixpkgs.legacyPackages.${system};
+
+      myPkgs = rec {
+        agda = import ./nix/agda.nix {
+          inherit system plfa;
+          nixpkgs = nixpkgs-agda;
+        };
+        nvim-agda = import ./nix/nvim-agda {
+          inherit system;
+          nixpkgs = nixpkgs-agda;
+        };
+
+        neovim = pkgs.callPackage ./nix/neovim.nix { inherit nvim-agda; };
+      };
+
+      vscode-agda-mode = pkgs.vscode-utils.extensionFromVscodeMarketplace {
+        name = "agda-mode";
+        publisher = "banacorn";
+        version = "0.2.19";
+        sha256 = "2PFfFySOoxFEZdYb2BF6XQeYEygbTn/WJub/8IKfc1Y=";
+      };
+      combinedExtensionsDrv = pkgs.buildEnv {
+        name = "vscodium-extensions";
+        paths = [
+          vscode-agda-mode
+          pkgs.vscode-extensions.vscodevim.vim
+        ];
+      };
+      vscodium = pkgs.runCommand "vscodium-with-extensions" {
+        nativeBuildInputs = [ pkgs.makeWrapper ];
+        buildInputs = [ pkgs.vscodium ];
+        meta = pkgs.vscodium.meta;
+      } ''
+        mkdir -p $out/bin
+        makeWrapper "${pkgs.vscodium}/bin/codium" "$out/bin/codium" \
+          --add-flags "--extensions-dir ${combinedExtensionsDrv}/share/vscode/extensions"
+      '';
+    in
+    {
+      packages = flake-utils.lib.flattenTree myPkgs;
+
+      devShell = pkgs.mkShell {
+        buildInputs = with pkgs; with myPkgs; [
+          agda
+          vscodium
+          neovim
+          nvim-agda
+          lua51Packages.luautf8
+        ];
+      };
+    }
+  );
+}
+

nix/agda.nix

@@ -0,0 +1,20 @@
+{ nixpkgs, system, plfa, ... }:
+
+let
+  pkgs = nixpkgs.legacyPackages.${system};
+in
+pkgs.agda.withPackages (p: [
+  p.standard-library
+  (p.mkDerivation {
+    pname = "plfa";
+    meta = null;
+    version = "1.0.0";
+    buildInputs = [ p.standard-library ];
+    preBuild = ''
+      echo "module Everything where" > Everything.agda
+      find src -name '*.lagda.md' | sed -e 's/src\///' -e 's/\.lagda\.md//' -e 's/\//\./g' -e 's/^/import /' | grep -Ev '^import plfa\.part1\.Equality|Naturals$' >> Everything.agda
+      export LANG=C.UTF-8
+    '';
+    src = plfa;
+  })
+])

nix/neovim.nix

@@ -0,0 +1,36 @@
+{ neovim, vimPlugins, luajitPackages, nvim-agda }:
+
+neovim.override {
+  configure = {
+    plug = {
+      plugins = with vimPlugins; [
+        ctrlp-vim
+        nerdtree
+        nvim-agda
+        vim-code-dark
+        vim-polyglot
+      ];
+    };
+
+    customRC = ''
+      lua << EOF
+        package.cpath = package.cpath .. ";${luajitPackages.luautf8}/lib/lua/5.1/lua-utf8.so"
+      EOF
+
+      set hidden
+      set cursorline
+      set number
+      set splitright
+      set modeline
+      set expandtab
+      set colorcolumn=80
+      syntax on
+      filetype on
+      filetype plugin indent on
+      colorscheme codedark
+
+      nnoremap <C-n> :NERDTreeToggle<CR>
+      imap kj <Esc>
+    '';
+  };
+}

nix/nvim-agda/agda-vim-excerpts/LICENSE

@@ -0,0 +1,24 @@
+Copyright (c) 2013, Derek Elkins
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+Redistributions of source code must retain the above copyright notice, this
+list of conditions and the following disclaimer.
+
+Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer in the
+documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

nix/nvim-agda/agda-vim-excerpts/README

@@ -0,0 +1,2 @@
+autoload.vim and ftplugin.vim are mostly taken from
+https://github.com/derekelkins/agda-vim, with slight modification.

nix/nvim-agda/agda-vim-excerpts/autoload.vim

@@ -0,0 +1,668 @@
+" Agda Input Abbreviations
+"
+let s:cpo_save = &cpo
+set cpo&vim
+
+" Public to allow referencing in custom overrides.
+if !exists('g:agda#default_glyphs')
+  let g:agda#default_glyphs = {}
+
+  " Extra Shit
+  call extend(g:agda#default_glyphs, {
+    \   'Gl-': 'ƛ',
+    \   '==': '≡',
+    \   '<': '⟨',
+    \   '>': '⟩',
+    \   'em': '—',
+    \   '=>': '⇒',
+    \   '~-': '≃',
+    \   'r': '→',
+    \   '0': '∅',
+    \})
+
+  " Combining marks
+  call extend(g:agda#default_glyphs, {
+    \   'over`': ' ̀',
+    \   "over'": ' ́',
+    \   'over^': ' ̂',
+    \   'overv': ' ̌',
+    \   'over~': ' ̃',
+    \   'over-': ' ̄',
+    \   'over_': ' ̅',
+    \   'over–': ' ̅',
+    \   'over—': ' ̅',
+    \   'overcup': ' ̆',
+    \   'overcap': ' ̑',
+    \   'over.': ' ̇',
+    \   'over..': ' ̈',
+    \   'over"': ' ̈',
+    \   'over...': ' ⃛',
+    \   'overright.': ' ͘',
+    \   'overo': ' ̊',
+    \   'over``': ' ̏',
+    \   "over''": ' ̋',
+    \   'overvec': ' ⃑',
+    \   'vec': ' ⃑',
+    \   'overlvec': ' ⃐',
+    \   'lvec': ' ⃐',
+    \   'overarc': ' ⃕',
+    \   'overlarc': ' ⃔',
+    \   'overto': ' ⃗',
+    \   'overfrom': ' ⃖',
+    \   'overfromto': ' ⃡',
+    \   'over*': ' ⃰',
+    \   'under`': ' ̖',
+    \   "under'": ' ̗',
+    \   'under,': ' ̗',
+    \   'under.': ' ̣',
+    \   'under..': ' ̤',
+    \   'under"': ' ̤',
+    \   'undero': ' ̥',
+    \   'under-': ' ̱',
+    \   'under_': ' ̲',
+    \   'under–': ' ̲',
+    \   'under—': ' ̲',
+    \   'through~': ' ̴',
+    \   'through-': ' ̵',
+    \   'through_': ' ̶',
+    \   'through–': ' ̶',
+    \   'through—': ' ̶',
+    \   'through/': ' ̷',
+    \   'not': ' ̷',
+    \   'through?': ' ̸',
+    \   'Not': ' ̸',
+    \   'through\|': ' ⃒',
+    \   'throughshortmid': ' ⃓',
+    \   'througho': ' ⃘',
+    \})
+
+  " Math
+    " \   ':': '∶',
+  call extend(g:agda#default_glyphs, {
+    \   '{{': '⦃',
+    \   '}}': '⦄',
+    \   ':': '⦂',
+    \   '::': '∷',
+    \   ';': '﹔',
+    \   '..': '‥',
+    \   '=?': '≟',
+    \   'all': '∀',
+    \   'always': '□',
+    \   'approx': '≈',
+    \   'bot': '⊥',
+    \   'box': '□',
+    \   'boxdot': '⊡',
+    \   'box.': '⊡',
+    \   'boxminus': '⊟',
+    \   'box-': '⊟',
+    \   'boxplus': '⊞',
+    \   'box+': '⊞',
+    \   'boxtimes': '⊠',
+    \   'box*': '⊠',
+    \   'bul': '•',
+    \   'C': 'ℂ',
+    \   'cdot': '·',
+    \   '.': '∙',
+    \   'cdots': '⋯',
+    \   'check': '✓',
+    \   'yes': '✓',
+    \   'Check': '✔',
+    \   'Yes': '✔',
+    \   'circ': '∘',
+    \   'clock': '↻',
+    \   'cclock': '↺',
+    \   'comp': '∘',
+    \   'contra': '↯',
+    \   'deg': '°',
+    \   'den': '⟦⟧<left>',
+    \   'diamond': '◇',
+    \   'dots': '…',
+    \   'down': '↓',
+    \   'downtri': '▼',
+    \   'Down': '⇓',
+    \   'dunion': '⊎',
+    \   'du': '⊎',
+    \   'ell': 'ℓ',
+    \   'empty': '∅',
+    \   'equiv': '≡',
+    \   'eq': '≡',
+    \   'eventually': '◇',
+    \   'exists': '∃',
+    \   'flat': '♭',
+    \   'fold': '⦇⦈<left>',
+    \   '(\|': '⦇',
+    \   '\|)': '⦈',
+    \   'forall': '∀',
+    \   'from': '←',
+    \   '<-': '←',
+    \   'From': '⇐',
+    \   'fromto': '↔',
+    \   'Fromto': '⇔',
+    \   'ge': '≥',
+    \   'glub': '⊓',
+    \   'iff': '⇔',
+    \   'implies': '⇒',
+    \   'impliedby': '⇐',
+    \   'in': '∈',
+    \   'infty': '∞',
+    \   'inf': '∞',
+    \   'int': '∫',
+    \   'intersect': '∩',
+    \   'iso': '≅',
+    \   'join': '⋈',
+    \   'land': '∧',
+    \   'langle': '⟨',
+    \   'lbrac': '⟦',
+    \   '[[': '⟦',
+    \   'ldots': '…',
+    \   'ldown': '⇃',
+    \   'leadsto': '⇝',
+    \   '~>': '⇝',
+    \   'le': '≤',
+    \   'lift': '⌊⌋<left>',
+    \   'floor': '⌊⌋<left>',
+    \   'llangle': '⟪',
+    \   'longto': '⟶ ',
+    \   '--': '⟶ ',
+    \   '–': '⟶ ',
+    \   'lor': '∨',
+    \   'lower': '⌈⌉<left>',
+    \   'ceil': '⌈⌉<left>',
+    \   'lub': '⊔',
+    \   'lup': '↿',
+    \   'mapsto': '↦',
+    \   'map': '↦',
+    \   'mid': '∣',
+    \   'models': '⊨',
+    \   '\|=': '⊨',
+    \   'N': 'ℕ',
+    \   'ne': '≠',
+    \   'nearrow': '↗',
+    \   'Nearrow': '⇗',
+    \   'neg': '¬',
+    \   '/=': '≠',
+    \   'nequiv': '≢',
+    \   'neq': '≢',
+    \   'nexist': '∄',
+    \   'none': '∄',
+    \   'ni': '∋',
+    \   'nin': '∉',
+    \   'niso': '≇',
+    \   'notin': '∉',
+    \   'nwarrow': '↖',
+    \   'Nwarrow': '⇖',
+    \   'oast': '⊛',
+    \   'odot': '⊙',
+    \   'o.': '⊙',
+    \   'of': '∘',
+    \   'o': '∘',
+    \   'ominus': '⊖',
+    \   'o-': '⊖',
+    \   'oplus': '⊕',
+    \   'o+': '⊕',
+    \   'oslash': '⊘',
+    \   'o/': '⊘',
+    \   'otimes': '⊗',
+    \   'o*': '⊗',
+    \   'par': '∂',
+    \   'pge': '≽',
+    \   'pgt': '≻',
+    \   'ple': '≼',
+    \   'plt': '≺',
+    \   'p≥': '≽',
+    \   'p>': '≻',
+    \   'p≤': '≼',
+    \   'p<': '≺',
+    \   'pm': '±',
+    \   'prec': '≼',
+    \   'prod': '∏',
+    \   'proves': '⊢',
+    \   '\|-': '⊢',
+    \   'provedby': '⊣',
+    \   'Q': 'ℚ',
+    \   'qed': '∎',
+    \   'R': 'ℝ',
+    \   'rangle': '⟩',
+    \   'rbrac': '⟧',
+    \   ']]': '⟧',
+    \   'rdown': '⇂',
+    \   'righttri': '▸',
+    \   'rrangle': '⟫',
+    \   'rup': '↾',
+    \   'searrow': '↘',
+    \   'Searrow': '⇘',
+    \   'setminus': '∖',
+    \   'sharp': '♯',
+    \   '#': '♯',
+    \   'sim': '∼',
+    \   'simeq': '≃',
+    \   'some': '∃',
+    \   'sqge': '⊒',
+    \   'sqgt': '⊐',
+    \   'sqle': '⊑',
+    \   'sqlt': '⊏',
+    \   's≥': '⊒',
+    \   's>': '⊐',
+    \   's≤': '⊑',
+    \   's<': '⊏',
+    \   'sqr': '²',
+    \   'sqrt': '√',
+    \   'star': '✭',
+    \   'subset': '⊂',
+    \   'sub': '⊂',
+    \   'subseteq': '⊆',
+    \   'subeq': '⊆',
+    \   'subsetneq': '⊊',
+    \   'subneq': '⊊',
+    \   'sum': '∑',
+    \   'supset': '⊃',
+    \   'sup': '⊃',
+    \   'supseteq': '⊇',
+    \   'supeq': '⊇',
+    \   'supsetneq': '⊋',
+    \   'supneq': '⊋',
+    \   'swarrow': '↙',
+    \   'Swarrow': '⇙',
+    \   'thus': '∴',
+    \   'times': '×',
+    \   '*': '×',
+    \   'to': '→',
+    \   '-': '→',
+    \   'To': '⇒',
+    \   '=': '⇒',
+    \   'top': '⊤',
+    \   'tuple': '⟨⟩<left>',
+    \   'up': '↑',
+    \   'updown': '↕',
+    \   'ud': '↕',
+    \   'unfold': '⦉⦊<left>',
+    \   '<\|': '⦉',
+    \   '\|>': '⦊',
+    \   'up;down': '⇅',
+    \   'u;d': '⇅',
+    \   'uptri': '▲',
+    \   'Up': '⇑',
+    \   'union': '∪',
+    \   'vdots': '⋮',
+    \   'voltage': '⚡',
+    \   'xmark': '✗',
+    \   'no': '✗',
+    \   'Xmark': '✘',
+    \   'No': '✘',
+    \   'Z': 'ℤ',
+    \})
+
+  " Not math
+  call extend(g:agda#default_glyphs, {
+    \   'sec': '§',
+    \})
+
+  " Superscripts
+  call extend(g:agda#default_glyphs, {
+    \   '^0': '⁰',
+    \   '^1': '¹',
+    \   '^2': '²',
+    \   '^3': '³',
+    \   '^4': '⁴',
+    \   '^5': '⁵',
+    \   '^6': '⁶',
+    \   '^7': '⁷',
+    \   '^8': '⁸',
+    \   '^9': '⁹',
+    \   '^A': 'ᴬ',
+    \   '^B': 'ᴮ',
+    \   '^D': 'ᴰ',
+    \   '^E': 'ᴱ',
+    \   '^G': 'ᴳ',
+    \   '^H': 'ᴴ',
+    \   '^I': 'ᴵ',
+    \   '^J': 'ᴶ',
+    \   '^K': 'ᴷ',
+    \   '^L': 'ᴸ',
+    \   '^M': 'ᴹ',
+    \   '^N': 'ᴺ',
+    \   '^O': 'ᴼ',
+    \   '^P': 'ᴾ',
+    \   '^R': 'ᴿ',
+    \   '^T': 'ᵀ',
+    \   '^U': 'ᵁ',
+    \   '^V': 'ⱽ',
+    \   '^W': 'ᵂ',
+    \   '^a': 'ᵃ',
+    \   '^b': 'ᵇ',
+    \   '^c': 'ᶜ',
+    \   '^d': 'ᵈ',
+    \   '^e': 'ᵉ',
+    \   '^f': 'ᶠ',
+    \   '^g': 'ᵍ',
+    \   '^h': 'ʰ',
+    \   '^i': 'ⁱ',
+    \   '^j': 'ʲ',
+    \   '^k': 'ᵏ',
+    \   '^l': 'ˡ',
+    \   '^m': 'ᵐ',
+    \   '^n': 'ⁿ',
+    \   '^o': 'ᵒ',
+    \   '^p': 'ᵖ',
+    \   '^r': 'ʳ',
+    \   '^s': 'ˢ',
+    \   '^t': 'ᵗ',
+    \   '^u': 'ᵘ',
+    \   '^v': 'ᵛ',
+    \   '^w': 'ʷ',
+    \   '^x': 'ˣ',
+    \   '^y': 'ʸ',
+    \   '^z': 'ᶻ',
+    \   '^+': '⁺',
+    \   '^-': '⁻',
+    \   '^=': '⁼',
+    \   '^(': '⁽',
+    \   '^)': '⁾',
+    \   "'": '′',
+    \   "''": '″',
+    \   "'''": '‴',
+    \   "''''": '⁗',
+    \   '"': '″',
+    \   '""': '⁗',
+    \   '`': '‵',
+    \   '``': '‶',
+    \   '```': '‷',
+    \})
+
+  " Subscripts
+  call extend(g:agda#default_glyphs, {
+    \   '_0': '₀',
+    \   '_1': '₁',
+    \   '_2': '₂',
+    \   '_3': '₃',
+    \   '_4': '₄',
+    \   '_5': '₅',
+    \   '_6': '₆',
+    \   '_7': '₇',
+    \   '_8': '₈',
+    \   '_9': '₉',
+    \   '_a': 'ₐ',
+    \   '_e': 'ₑ',
+    \   '_h': 'ₕ',
+    \   '_i': 'ᵢ',
+    \   '_j': 'ⱼ',
+    \   '_k': 'ₖ',
+    \   '_l': 'ₗ',
+    \   '_m': 'ₘ',
+    \   '_n': 'ₙ',
+    \   '_o': 'ₒ',
+    \   '_p': 'ₚ',
+    \   '_r': 'ᵣ',
+    \   '_s': 'ₛ',
+    \   '_t': 'ₜ',
+    \   '_u': 'ᵤ',
+    \   '_v': 'ᵥ',
+    \   '_x': 'ₓ',
+    \   '_+': '₊',
+    \   '_-': '₋',
+    \   '_=': '₌',
+    \   '_(': '₍',
+    \   '_)': '₎',
+    \   'p0': 'π₀',
+    \   'p1': 'π₁',
+    \   'p2': 'π₂',
+    \   'p3': 'π₃',
+    \   'p4': 'π₄',
+    \   'p5': 'π₅',
+    \   'p6': 'π₆',
+    \   'p7': 'π₇',
+    \   'p8': 'π₈',
+    \   'p9': 'π₉',
+    \   'i0': 'ι₀',
+    \   'i1': 'ι₁',
+    \   'i2': 'ι₂',
+    \   'i3': 'ι₃',
+    \   'i4': 'ι₄',
+    \   'i5': 'ι₅',
+    \   'i6': 'ι₆',
+    \   'i7': 'ι₇',
+    \   'i8': 'ι₈',
+    \   'i9': 'ι₉',
+    \})
+
+  " Greek (lower)
+  call extend(g:agda#default_glyphs, {
+    \   'alpha': 'α',
+    \   'a': 'α',
+    \   'beta': 'β',
+    \   'b': 'β',
+    \   'gamma': 'γ',
+    \   'g': 'γ',
+    \   'delta': 'δ',
+    \   'd': 'δ',
+    \   'epsilon': 'ε',
+    \   'e': 'ε',
+    \   'zeta': 'ζ',
+    \   'z': 'ζ',
+    \   'eta': 'η',
+    \   'h': 'η',
+    \   'theta': 'θ',
+    \   'iota': 'ι',
+    \   'i': 'ι',
+    \   'kappa': 'κ',
+    \   'k': 'κ',
+    \   'lambda': 'λ',
+    \   'l': 'λ',
+    \   'mu': 'μ',
+    \   'm': 'μ',
+    \   'nu': 'ν',
+    \   'n': 'ν',
+    \   'xi': 'ξ',
+    \   'omicron': 'ο',
+    \   'pi': 'π',
+    \   'p': 'π',
+    \   'rho': 'ρ',
+    \   'sigma': 'σ',
+    \   's': 'σ',
+    \   'varsigma': 'ς',
+    \   'vars': 'ς',
+    \   'tau': 'τ',
+    \   't': 'τ',
+    \   'u': 'υ',
+    \   'phi': 'φ',
+    \   'f': 'φ',
+    \   'chi': 'χ',
+    \   'x': 'χ',
+    \   'psi': 'ψ',
+    \   'c': 'ψ',
+    \   'omega': 'ω',
+    \   'v': 'ω',
+    \})
+
+  " Greek (upper)
+  call extend(g:agda#default_glyphs, {
+    \   'Alpha': 'Α',
+    \   'Beta': 'Β',
+    \   'Gamma': 'Γ',
+    \   'G': 'Γ',
+    \   'Delta': 'Δ',
+    \   'D': 'Δ',
+    \   'Epsilon': 'Ε',
+    \   'Zeta': 'Ζ',
+    \   'Eta': 'Η',
+    \   'Theta': 'Θ',
+    \   'Iota': 'Ι',
+    \   'Kappa': 'Κ',
+    \   'Lambda': 'Λ',
+    \   'L': 'Λ',
+    \   'Mu': 'Μ',
+    \   'Nu': 'Ν',
+    \   'Xi': 'Ξ',
+    \   'Omicron': 'Ο',
+    \   'Pi': 'Π',
+    \   'P': 'Π',
+    \   'Rho': 'Ρ',
+    \   'Sigma': 'Σ',
+    \   'S': 'Σ',
+    \   'Tau': 'Τ',
+    \   'Upsilon': 'Υ',
+    \   'Phi': 'Φ',
+    \   'F': 'Φ',
+    \   'Chi': 'Χ',
+    \   'Psi': 'Ψ',
+    \   'Omega': 'Ω',
+    \   'V': 'Ω',
+    \})
+
+  " Blackboard
+  call extend(g:agda#default_glyphs, {
+    \   'bA': '𝔸',
+    \   'bB': '𝔹',
+    \   'bC': 'ℂ',
+    \   'bD': '𝔻',
+    \   'bE': '𝔼',
+    \   'bF': '𝔽',
+    \   'bG': '𝔾',
+    \   'bH': 'ℍ',
+    \   'bI': '𝕀',
+    \   'bJ': '𝕁',
+    \   'bK': '𝕂',
+    \   'bL': '𝕃',
+    \   'bM': '𝕄',
+    \   'bN': 'ℕ',
+    \   'bO': '𝕆',
+    \   'bP': 'ℙ',
+    \   'bQ': 'ℚ',
+    \   'bR': 'ℝ',
+    \   'bS': '𝕊',
+    \   'bT': '𝕋',
+    \   'bU': '𝕌',
+    \   'bV': '𝕍',
+    \   'bW': '𝕎',
+    \   'bX': '𝕏',
+    \   'bY': '𝕐',
+    \   'bZ': 'ℤ',
+    \   'b0': '𝟘',
+    \   'b1': '𝟙',
+    \   'b2': '𝟚',
+    \   'b3': '𝟛',
+    \   'b4': '𝟜',
+    \   'b5': '𝟝',
+    \   'b6': '𝟞',
+    \   'b7': '𝟟',
+    \   'b8': '𝟠',
+    \   'b9': '𝟡',
+    \   'bsum': '⅀',
+    \})
+
+  " Math chars
+  call extend(g:agda#default_glyphs, {
+    \   'McA': '𝓐',
+    \   'McB': '𝓑',
+    \   'McC': '𝓒',
+    \   'McD': '𝓓',
+    \   'McE': '𝓔',
+    \   'McF': '𝓕',
+    \   'McG': '𝓖',
+    \   'McH': '𝓗',
+    \   'McI': '𝓘',
+    \   'McJ': '𝓙',
+    \   'McK': '𝓚',
+    \   'McL': '𝓛',
+    \   'McM': '𝓜',
+    \   'McN': '𝓝',
+    \   'McO': '𝓞',
+    \   'McP': '𝓟',
+    \   'McQ': '𝓠',
+    \   'McR': '𝓡',
+    \   'McS': '𝓢',
+    \   'McT': '𝓣',
+    \   'McU': '𝓤',
+    \   'McV': '𝓥',
+    \   'McW': '𝓦',
+    \   'McX': '𝓧',
+    \   'McY': '𝓨',
+    \   'McZ': '𝓩',
+    \   'Mca': '𝒶',
+    \   'Mcb': '𝒷',
+    \   'Mcc': '𝒸',
+    \   'Mcd': '𝒹',
+    \   'Mcf': '𝒻',
+    \   'Mch': '𝒽',
+    \   'Mci': '𝒾',
+    \   'Mcj': '𝒿',
+    \   'Mck': '𝓀',
+    \   'Mcl': '𝓁',
+    \   'Mcm': '𝓂',
+    \   'Mcn': '𝓃',
+    \   'Mcp': '𝓅',
+    \   'Mcq': '𝓆',
+    \   'Mcr': '𝓇',
+    \   'Mcs': '𝓈',
+    \   'Mct': '𝓉',
+    \   'Mcu': '𝓊',
+    \   'Mcv': '𝓋',
+    \   'Mcw': '𝓌',
+    \   'Mcx': '𝓍',
+    \   'Mcy': '𝓎',
+    \   'Mcz': '𝓏',
+    \   'MfA': '𝔄',
+    \   'MfB': '𝔅',
+    \   'MfD': '𝔇',
+    \   'MfE': '𝔈',
+    \   'MfF': '𝔉',
+    \   'MfG': '𝔊',
+    \   'MfJ': '𝔍',
+    \   'MfK': '𝔎',
+    \   'MfL': '𝔏',
+    \   'MfM': '𝔐',
+    \   'MfN': '𝔑',
+    \   'MfO': '𝔒',
+    \   'MfP': '𝔓',
+    \   'MfQ': '𝔔',
+    \   'MfS': '𝔖',
+    \   'MfT': '𝔗',
+    \   'MfU': '𝔘',
+    \   'MfV': '𝔙',
+    \   'MfW': '𝔚',
+    \   'MfX': '𝔛',
+    \   'MfY': '𝔜',
+    \   'Mfa': '𝔞',
+    \   'Mfb': '𝔟',
+    \   'Mfc': '𝔠',
+    \   'Mfd': '𝔡',
+    \   'Mfe': '𝔢',
+    \   'Mff': '𝔣',
+    \   'Mfg': '𝔤',
+    \   'Mfh': '𝔥',
+    \   'Mfi': '𝔦',
+    \   'Mfj': '𝔧',
+    \   'Mfk': '𝔨',
+    \   'Mfl': '𝔩',
+    \   'Mfm': '𝔪',
+    \   'Mfn': '𝔫',
+    \   'Mfo': '𝔬',
+    \   'Mfp': '𝔭',
+    \   'Mfq': '𝔮',
+    \   'Mfr': '𝔯',
+    \   'Mfs': '𝔰',
+    \   'Mft': '𝔱',
+    \   'Mfu': '𝔲',
+    \   'Mfv': '𝔳',
+    \   'Mfw': '𝔴',
+    \   'Mfx': '𝔵',
+    \   'Mfy': '𝔶',
+    \   'Mfz': '𝔷',
+    \})
+
+  " From Favonia
+  call extend(g:agda#default_glyphs, {
+    \   'breve': '˘',
+    \   'monus': '∸',
+    \   '<>': '⟨⟩<left>',
+    \   'greekq': ';',
+    \})
+
+  lockvar g:agda#default_glyphs
+endif
+
+if !exists('g:agda#glyphs')
+  let g:agda#glyphs = deepcopy(g:agda#default_glyphs)
+endif
+
+let &cpo = s:cpo_save

nix/nvim-agda/agda-vim-excerpts/ftplugin.vim

@@ -0,0 +1,88 @@
+let s:cpo_save = &cpo
+set cpo&vim
+
+let b:undo_ftplugin = ''
+
+for [sequence, symbol] in items(g:agda#glyphs)
+  execute printf('noremap! <buffer> <LocalLeader>%s %s', sequence, symbol)
+endfor
+
+setlocal matchpairs&vim
+setlocal matchpairs+=(:)
+setlocal matchpairs+=<:>
+setlocal matchpairs+=[:]
+setlocal matchpairs+={:}
+setlocal matchpairs+=«:»
+setlocal matchpairs+=‹:›
+setlocal matchpairs+=⁅:⁆
+setlocal matchpairs+=⁽:⁾
+setlocal matchpairs+=₍:₎
+setlocal matchpairs+=⌈:⌉
+setlocal matchpairs+=⌊:⌋
+setlocal matchpairs+=〈:〉
+setlocal matchpairs+=⎛:⎞
+setlocal matchpairs+=⎝:⎠
+setlocal matchpairs+=⎡:⎤
+setlocal matchpairs+=⎣:⎦
+setlocal matchpairs+=⎧:⎫
+setlocal matchpairs+=⎨:⎬
+setlocal matchpairs+=⎩:⎭
+setlocal matchpairs+=⎴:⎵
+setlocal matchpairs+=❨:❩
+setlocal matchpairs+=❪:❫
+setlocal matchpairs+=❬:❭
+setlocal matchpairs+=❮:❯
+setlocal matchpairs+=❰:❱
+setlocal matchpairs+=❲:❳
+setlocal matchpairs+=❴:❵
+setlocal matchpairs+=⟅:⟆
+setlocal matchpairs+=⟦:⟧
+setlocal matchpairs+=⟨:⟩
+setlocal matchpairs+=⟪:⟫
+setlocal matchpairs+=⦃:⦄
+setlocal matchpairs+=⦅:⦆
+setlocal matchpairs+=⦇:⦈
+setlocal matchpairs+=⦉:⦊
+setlocal matchpairs+=⦋:⦌
+setlocal matchpairs+=⦍:⦎
+setlocal matchpairs+=⦏:⦐
+setlocal matchpairs+=⦑:⦒
+setlocal matchpairs+=⦓:⦔
+setlocal matchpairs+=⦕:⦖
+setlocal matchpairs+=⦗:⦘
+setlocal matchpairs+=⸠:⸡
+setlocal matchpairs+=⸢:⸣
+setlocal matchpairs+=⸤:⸥
+setlocal matchpairs+=⸦:⸧
+setlocal matchpairs+=⸨:⸩
+setlocal matchpairs+=〈:〉
+setlocal matchpairs+=《:》
+setlocal matchpairs+=「:」
+setlocal matchpairs+=『:』
+setlocal matchpairs+=【:】
+setlocal matchpairs+=〔:〕
+setlocal matchpairs+=〖:〗
+setlocal matchpairs+=〘:〙
+setlocal matchpairs+=〚:〛
+setlocal matchpairs+=︗:︘
+setlocal matchpairs+=︵:︶
+setlocal matchpairs+=︷:︸
+setlocal matchpairs+=︹:︺
+setlocal matchpairs+=︻:︼
+setlocal matchpairs+=︽:︾
+setlocal matchpairs+=︿:﹀
+setlocal matchpairs+=﹁:﹂
+setlocal matchpairs+=﹃:﹄
+setlocal matchpairs+=﹇:﹈
+setlocal matchpairs+=﹙:﹚
+setlocal matchpairs+=﹛:﹜
+setlocal matchpairs+=﹝:﹞
+setlocal matchpairs+=（:）
+setlocal matchpairs+=＜:＞
+setlocal matchpairs+=［:］
+setlocal matchpairs+=｛:｝
+setlocal matchpairs+=｟:｠
+setlocal matchpairs+=｢:｣
+let b:undo_ftplugin .= ' | setlocal matchpairs<'
+
+let &cpo = s:cpo_save

nix/nvim-agda/default.nix

@@ -0,0 +1,26 @@
+{ nixpkgs, system, ... }:
+
+let
+  pkgs = nixpkgs.legacyPackages.${system};
+in
+pkgs.vimUtils.buildVimPlugin rec {
+  pname = "nvim-agda";
+  version = "2bed0b9a1d42f20438d22a3229c59faaf2b6a8df";
+  src = pkgs.fetchFromGitHub {
+    owner = "ashinkarov";
+    repo = pname;
+    rev = version;
+    hash = "sha256-cMEOSGMyFHp/iABjpbxb3GFi4lBFYOhIDcI/EwgVgdw=";
+  };
+  buildPhase = ''
+    for patch in ${./patches}/*; do
+      echo Applying $patch...
+      patch -p1 --verbose < $patch
+    done
+
+    mkdir autoload
+    cp ${agda-vim-excerpts/autoload.vim} autoload/agda.vim
+    cat ${agda-vim-excerpts/ftplugin.vim} >> ftplugin/agda.vim
+    cat ${./keybinds.vim} >> ftplugin/agda.vim
+  '';
+}

nix/nvim-agda/keybinds.vim

@@ -0,0 +1,11 @@
+nnoremap <buffer> <LocalLeader>r :<c-u>AgdaLoad<cr>
+nnoremap <buffer> <LocalLeader>t :<c-u>AgdaInfer<cr>
+nnoremap <buffer> <LocalLeader>q :<c-u>AgdaCloseMsg<cr>
+nnoremap <buffer> <LocalLeader>x :<c-u>AgdaCompute<cr>
+nnoremap <buffer> <LocalLeader>a :<c-u>AgdaRefine<cr>
+nnoremap <buffer> <LocalLeader>A :<c-u>AgdaAuto<cr>
+nnoremap <buffer> <LocalLeader>c :<c-u>AgdaMakeCase<cr>
+nmap     <buffer> K :<c-u>AgdaTypeContext<cr>
+nnoremap <buffer> [g :<c-u>GoalPrev<cr>
+nnoremap <buffer> ]g :<c-u>GoalNext<cr>
+nnoremap <buffer> gd :<c-u>AgdaWhyInscope<cr>

nix/nvim-agda/patches/0001-remove-default-keybinds.patch

@@ -0,0 +1,31 @@
+diff --git a/ftplugin/agda.vim b/ftplugin/agda.vim
+index f3264b5..2585b54 100644
+--- a/ftplugin/agda.vim
++++ b/ftplugin/agda.vim
+@@ -39,26 +39,3 @@ command! GoalPrev :call AgdaMod.agda_goal_prev(expand("%:p"))
+ command! AgdaCloseMsg :call AgdaMod.close_msg_win()
+ command! GoalContent :call AgdaMod.gc()
+ command! GetEvbuf :call AgdaMod.getevbuf()
+-
+-
+-" Key mappings
+-nm <buffer> <LocalLeader>l :<c-u>AgdaLoad<cr>
+-nm <buffer> <LocalLeader>q :<c-u>AgdaCloseMsg<cr>
+-nm <buffer> <LocalLeader>, :<c-u>AgdaTypeContext<cr>
+-nm <buffer> <LocalLeader>u, :<c-u>AgdaTypeContextNorm<cr>
+-nm <buffer> <LocalLeader>d :<c-u>AgdaInfer<cr>
+-nm <buffer> <LocalLeader>r :<c-u>AgdaRefine<cr>
+-nm <buffer> <LocalLeader>c :<c-u>AgdaMakeCase<cr>
+-nm <buffer> <LocalLeader>n :<c-u>AgdaCompute<cr>
+-nm <buffer> <LocalLeader>a :<c-u>AgdaAuto<cr>
+-nm <buffer> <LocalLeader>h :<c-u>AgdaHelperFun<cr>
+-nm <buffer> <LocalLeader>o :<c-u>AgdaModuleContents<cr>
+-nm <buffer> <LocalLeader>w :<c-u>AgdaWhyInscope<cr>
+-nm <buffer> <LocalLeader>e :<c-u>MkPrompt<cr>
+-nm <buffer> <LocalLeader>? :<c-u>PrintGoals<cr>
+-nm <buffer> <LocalLeader>f :<c-u>GoalNext<cr>
+-nm <buffer> <LocalLeader>b :<c-u>GoalPrev<cr>
+-
+-
+-" mappings
+-runtime agda-input.vim

questions.txt

@@ -0,0 +1 @@
+_<_ why is one constructor allowed to only have one

src/Extra2.agda

@@ -0,0 +1,34 @@
+module _ where
+
+open import Relation.Binary.PropositionalEquality
+
+record ⊤ : Set where
+  constructor tt
+
+postulate
+  tt′ : ⊤
+
+lemma₀ : tt ≡ tt′
+lemma₀ = refl
+
+open import Data.Nat
+open import Data.Nat.Properties
+
+record Terminating (n : ℕ) : Set where
+  inductive
+  constructor box
+  field
+    call : ∀ {m : ℕ} → m <′ n → Terminating m
+open Terminating
+
+term : ∀ (n : ℕ) → Terminating n
+term 0 .call ()
+term (suc n) .call ≤′-refl = term n
+term (suc n) .call (≤′-step sm≤n) = term n .call sm≤n
+
+postulate
+  _/2 : ℕ → ℕ
+  /2-<′ : ∀ (n : ℕ) → n /2 <′ n
+
+merge : (n : ℕ) → Terminating n → ℕ
+merge n (box caller) = merge (n /2) (caller (/2-<′ n))

src/Extra3.agda

@@ -0,0 +1,87 @@
+module _ where
+
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+open import Function
+open import Data.Nat
+open import Data.Fin hiding (_+_)
+open import Data.Product hiding (map)
+
+-- Functions as Lists
+
+Vec : Set → ℕ → Set
+Vec A n = Fin n → A
+
+map-Vec : {A B : Set} {n : ℕ} → (A → B) → Vec A n → Vec B n
+map-Vec f v = f ∘′ v
+
+map-Vec-compose : {A B C : Set} {n : ℕ} (f : B → C) (g : A → B) (v : Vec A n)
+  → map-Vec (f ∘ g) v ≡ map-Vec f (map-Vec g v)
+map-Vec-compose f g v = refl
+
+List : Set → Set
+List A = Σ ℕ (λ n → Vec A n)
+
+map : {A B : Set} → (A → B) → List A → List B
+map f (n , v) = n , (f ∘′ v)
+
+map-compose : {A B C : Set} (f : B → C) (g : A → B) (l : List A)
+  → map (f ∘ g) l ≡ map f (map g l)
+map-compose f g l = refl
+
+[] : {A : Set} → List A
+[] = 0 , λ ()
+
+_∷_ : {A : Set} → A → List A → List A
+a ∷ (n , v) = (suc n) , λ{ zero → a ; (suc n) → v n }
+
+--- Questions
+
+-- Q1: Instance arguments...
+-- A1: Don't abuse it
+
+-- Q2: Convervativity of the eta rule of sigma types
+-- A2: this is a very interesting question!!!
+--
+-- ETT is conservative with respect to (ITT + K) + function ext, by Martin Hofmann
+
+-- Q3: Differences between judgmental eq, propositional eq, and isomorphisms
+
+-- A3: Judgmental equality is given
+
+_ = 1 + 1 ≡ 2
+_ = refl
+
+-- Propositional equality is a type that can be either
+
+-- 1. the inductive types generated by reflexivity, or
+-- 2. ...
+-- 3. ...
+
+-- Isomorphisms only make sense between two types.
+
+-- Q4: syntax
+
+postulate
+  F : (Set → Set) → (Set → Set)
+
+syntax F (λ x → e) (λ y → f) = e - x - y - f
+
+-- Q5. subtying in kinds
+
+-- Speed coding
+
++-comm : ∀ n m → n + m ≡ m + n
++-comm 0 m = ?
++-comm (suc n) m =
+  begin
+    suc n + m
+  ≡⟨ ? ⟩
+    suc n + m
+  ≡⟨ ? ⟩
+    suc n + m
+  ≡⟨ ? ⟩
+    suc n + m
+  ≡⟨ ? ⟩
+    m + suc n
+  ∎

src/Homework1.agda

@@ -0,0 +1,221 @@
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; module ≡-Reasoning)
+open ≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_)
+open import Data.Nat.Properties using (+-identityʳ; +-assoc; +-suc; +-comm)
+
+module Homework1 where
+
+-- zero property
+0-prop : ∀ (n : ℕ) → n * 0 ≡ 0
+0-prop zero = refl
+0-prop (suc n) = 0-prop n
+
+-- multiplicative identity
+*-identity : ∀ (n : ℕ) → n * 1 ≡ n
+*-identity zero = refl
+*-identity (suc n) = 
+  begin
+    suc n * 1
+  ≡⟨⟩
+    1 + n * 1
+  ≡⟨ cong (1 +_) (*-identity n) ⟩
+    1 + n
+  ∎
+
+
+-- multiplicative commutativity
+-- using induction on both variables
+*-comm : ∀ (a b : ℕ) → a * b ≡ b * a
+*-comm zero zero = refl
+*-comm a zero = 0-prop a
+*-comm zero b = sym (0-prop b)
+*-comm (suc a) (suc b) =
+  begin
+    suc a * suc b
+  ≡⟨⟩
+    suc b + a * suc b
+  ≡⟨ cong (suc b +_) (*-comm a (suc b)) ⟩
+    suc b + suc b * a
+  ≡⟨⟩
+    suc b + (a + b * a)
+  ≡⟨ sym (+-assoc (suc b) a (b * a)) ⟩
+    suc b + a + b * a
+  ≡⟨ cong (_+ (b * a)) (+-comm (suc b) a) ⟩
+    a + suc b + b * a
+  ≡⟨ cong (_+ (b * a)) (+-suc a b) ⟩
+    suc (a + b) + b * a
+  ≡⟨ cong (_+ (b * a)) (cong suc (+-comm a b)) ⟩
+    suc (b + a) + b * a
+  ≡⟨ cong (_+ (b * a)) (sym (+-suc b a)) ⟩
+    b + suc a + b * a
+  ≡⟨ cong (_+ (b * a)) (+-comm b (suc a)) ⟩
+    suc a + b + b * a
+  ≡⟨ cong (suc a + b +_) (*-comm b a) ⟩
+    suc a + b + a * b
+  ≡⟨ +-assoc (suc a) b (a * b) ⟩
+    suc a + (b + a * b)
+  ≡⟨⟩
+    suc a + suc a * b
+  ≡⟨ cong (suc a +_) (*-comm (suc a) b) ⟩
+    suc a + b * suc a
+  ≡⟨⟩
+    suc b * suc a
+  ∎
+
+-- multiplication distributive property
+*-distrib-+ : ∀ (a b c : ℕ) → a * (b + c) ≡ (a * b) + (a * c)
+*-distrib-+ a zero c =
+  begin
+    a * (zero + c)
+  ≡⟨⟩
+    a * c
+  ≡⟨⟩
+    zero + (a * c)
+  ≡⟨ cong (_+ (a * c)) (sym (0-prop a)) ⟩
+    (a * zero) + (a * c)
+  ∎
+*-distrib-+ a (suc b) c =
+  begin
+    a * (suc b + c)
+  ≡⟨⟩
+    a * suc (b + c)
+  ≡⟨ *-comm a (suc (b + c)) ⟩
+    suc (b + c) * a
+  ≡⟨⟩
+    a + (b + c) * a
+  ≡⟨ cong (a +_) (*-comm (b + c) a) ⟩
+    a + a * (b + c)
+  ≡⟨ cong (a +_) (*-distrib-+ a b c) ⟩
+    a + ((a * b) + (a * c))
+  ≡⟨ cong (a +_) (cong (_+ (a * c)) (*-comm a b)) ⟩
+    a + ((b * a) + (a * c))
+  ≡⟨ sym (+-assoc a (b * a) (a * c)) ⟩
+    a + (b * a) + (a * c)
+  ≡⟨⟩
+    (suc b * a) + (a * c)
+  ≡⟨ cong (_+ (a * c)) (*-comm (suc b) a) ⟩
+    (a * suc b) + (a * c)
+  ∎
+
+
+-- multiplicative associativity
+*-assoc : ∀ (a b c : ℕ) → (a * b) * c ≡ a * (b * c)
+*-assoc zero b c = refl
+*-assoc (suc a) b c =
+  begin
+    (suc a * b) * c
+  ≡⟨⟩
+    (b + a * b) * c
+  ≡⟨ *-comm (b + a * b) c ⟩
+    c * (b + a * b)
+  ≡⟨ *-distrib-+ c b (a * b) ⟩
+    (c * b) + (c * (a * b))
+  ≡⟨ cong ((c * b) +_) (sym (*-assoc c a b)) ⟩
+    (c * b) + (c * a * b)
+  ≡⟨ cong (_+ (c * a * b)) (*-comm c b) ⟩
+    (b * c) + (c * a * b)
+  ≡⟨ cong ((b * c) +_) (cong (_* b) (*-comm c a)) ⟩
+    (b * c) + (a * c * b)
+  ≡⟨ cong ((b * c) +_) (*-assoc a c b) ⟩
+    (b * c) + (a * (c * b))
+  ≡⟨ cong ((b * c) +_) (cong (a *_) (*-comm c b)) ⟩
+    (b * c) + (a * (b * c))
+  ∎
+
+
+-- 1-identity
+1-identity : ∀ (n : ℕ) → 1 * n ≡ n
+1-identity n =
+  begin
+    1 * n
+  ≡⟨⟩
+    n + 0 * n
+  ≡⟨⟩
+    n + 0
+  ≡⟨ +-comm n 0 ⟩
+    0 + n
+  ≡⟨⟩
+    n
+  ∎
+
+-- exponentiation distributive property
+^-distribˡ-|-* : ∀ (m n p : ℕ) → m ^ (n + p) ≡ (m ^ n) * (m ^ p)
+^-distribˡ-|-* m zero p =
+  begin
+    m ^ (zero + p)
+  ≡⟨⟩
+    m ^ p
+  ≡⟨ sym (1-identity (m ^ p)) ⟩
+    1 * (m ^ p)
+  ≡⟨⟩
+    (m ^ zero) * (m ^ p)
+  ∎
+^-distribˡ-|-* m (suc n) p =
+  begin
+    m ^ (suc n + p)
+  ≡⟨⟩
+    m ^ (suc (n + p))
+  ≡⟨⟩
+    m * (m ^ (n + p))
+  ≡⟨ cong (m *_) (^-distribˡ-|-* m n p) ⟩
+    m * ((m ^ n) * (m ^ p))
+  ≡⟨ sym (*-assoc m (m ^ n) (m ^ p)) ⟩
+    (m * (m ^ n)) * (m ^ p)
+  ≡⟨⟩
+    (m ^ suc n) * (m ^ p)
+  ∎
+
+-- exponential distribution from the right
+^-distribʳ-* : ∀ (m n p : ℕ) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
+^-distribʳ-* m n zero = refl
+^-distribʳ-* m n (suc p) =
+  begin
+    (m * n) ^ (suc p)
+  ≡⟨⟩
+    (m * n) * (m * n) ^ p
+  ≡⟨ cong (m * n *_) (^-distribʳ-* m n p) ⟩
+    (m * n) * ((m ^ p) * (n ^ p))
+  ≡⟨ sym (*-assoc (m * n) (m ^ p) (n ^ p)) ⟩
+    (m * n) * (m ^ p) * (n ^ p)
+  ≡⟨ cong (_* (n ^ p)) (*-assoc m n (m ^ p)) ⟩
+    (m * (n * (m ^ p))) * (n ^ p)
+  ≡⟨ cong (_* (n ^ p)) (cong (m *_) (*-comm n (m ^ p))) ⟩
+    (m * ((m ^ p) * n)) * (n ^ p)
+  ≡⟨ cong (_* (n ^ p)) (sym (*-assoc m (m ^ p) n)) ⟩
+    m * (m ^ p) * n * (n ^ p)
+  ≡⟨⟩
+    (m ^ suc p) * n * (n ^ p)
+  ≡⟨ *-assoc (m ^ suc p) n (n ^ p) ⟩
+    (m ^ suc p) * (n * (n ^ p))
+  ≡⟨⟩
+    (m ^ suc p) * (n ^ suc p)
+  ∎
+
+-- exponential association
+^-*-assoc : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
+^-*-assoc m n zero =
+  begin
+    (m ^ n) ^ zero
+  ≡⟨⟩
+    1
+  ≡⟨⟩
+    m ^ zero
+  ≡⟨ cong (m ^_) (sym (0-prop n)) ⟩
+    m ^ (n * zero)
+  ∎
+^-*-assoc m n (suc p) =
+  begin
+    (m ^ n) ^ (suc p)
+  ≡⟨⟩
+    (m ^ n) * (m ^ n) ^ p
+  ≡⟨ cong (m ^ n *_) (^-*-assoc m n p) ⟩
+    (m ^ n) * m ^ (n * p)
+  ≡⟨ sym (^-distribˡ-|-* m n (n * p)) ⟩
+    m ^ (n + n * p)
+  ≡⟨ cong (m ^_) (cong (n +_) (*-comm n p)) ⟩
+    m ^ (n + p * n)
+  ≡⟨⟩
+    m ^ (suc p * n)
+  ≡⟨ cong (m ^_) (*-comm (suc p) n) ⟩
+    m ^ (n * suc p)
+  ∎

src/Homework2.agda

@@ -0,0 +1,77 @@
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+open import Data.Nat
+open import Data.Nat.Properties
+
+module Homework2 where
+
+data Bin : Set where
+  O : Bin
+  _I : Bin → Bin
+  _II : Bin → Bin
+
+-------------------------------------------------------
+-- from
+-------------------------------------------------------
+
+from : Bin → ℕ
+from O = 0
+from (b I) = 1 + (from b) * 2
+from (b II) = 2 + (from b) * 2
+
+-------------------------------------------------------
+-- to
+-------------------------------------------------------
+
+inc : Bin → Bin
+inc O = O I
+inc (b I) = b II
+inc (b II) = (inc b) I
+
+to : ℕ → Bin
+to 0 = O
+to (suc n) = inc (to n)
+
+-------------------------------------------------------
+-- from∘to
+-------------------------------------------------------
+
+from-inc : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
+from-inc O = refl
+from-inc (n I) = refl
+from-inc (n II) = cong suc (cong (_* 2) (from-inc n))
+
+from∘to : ∀ n → from (to n) ≡ n
+from∘to zero = refl
+from∘to (suc n) = trans (from-inc (to n)) (cong suc (from∘to n))
+
+-------------------------------------------------------
+-- to∘from
+-------------------------------------------------------
+
+toI : ∀ (n : ℕ) → to (1 + n * 2) ≡ (to n) I
+toI zero = refl
+toI (suc n) = cong inc (cong inc (toI n))
+
+to∘from : ∀ b → to (from b) ≡ b
+to∘from O = refl
+to∘from (n I) =
+  begin
+    to (1 + (from n) * 2)
+  ≡⟨ toI (from n) ⟩
+    (to (from n)) I
+  ≡⟨ cong _I (to∘from n) ⟩
+    n I
+  ∎
+to∘from (n II) =
+  begin
+    to (from (n II))
+  ≡⟨⟩
+    to (2 + (from n) * 2)
+  ≡⟨⟩
+    inc (to (1 + (from n) * 2))
+  ≡⟨ cong inc (toI (from n)) ⟩
+    inc ((to (from n)) I)
+  ≡⟨ cong inc (cong _I (to∘from n)) ⟩
+    n II
+  ∎

src/Homework3.agda

@@ -0,0 +1,77 @@
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Decidable using (True; toWitness)
+open import Homework3Prelude
+
+module Homework3 where
+
+---------------------------------------------------------
+-- task 1
+---------------------------------------------------------
+
+V¬—→ : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ ⊢ A}
+  → Value M
+  → ¬ (M —→ N)
+V¬—→ V-ƛ ()
+V¬—→ V-zero ()
+V¬—→ (V-suc v) (ξ-suc m) = V¬—→ v m
+
+---------------------------------------------------------
+-- task 2
+---------------------------------------------------------
+
+mul : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
+mul = μ -- *
+  ƛ -- m
+  ƛ -- n
+  (case (# 1) -- match on m
+    -- case `zero → return 0
+    (`zero)
+
+    -- case `suc m₁ → return n + (m₁ * n)
+    (plus · # 1 · (# 3 · # 0 · # 1))
+  )
+
+task2 : mul {∅} · one · one —↠ one
+task2 =
+  begin
+    mul · one · one
+  —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
+    (ƛ ƛ (case (# 1) `zero (plus · # 1 · (mul · # 0 · # 1)))) · one · one
+  —→⟨ ξ-·₁ (β-ƛ (V-suc V-zero)) ⟩
+    (ƛ (case one `zero (plus · # 1 · (mul · # 0 · # 1)))) · one
+  —→⟨ β-ƛ (V-suc V-zero) ⟩
+    case one `zero (plus · one · (mul · # 0 · one))
+  —→⟨ β-suc V-zero ⟩
+    plus · one · (mul · `zero · one)
+  —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
+    (ƛ ƛ (case (# 1) (# 0) (`suc (plus · # 0 · # 1)))) · one · (mul · `zero · one)
+  —→⟨ ξ-·₁ (β-ƛ (V-suc V-zero)) ⟩
+    (ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) · (mul · `zero · one)
+  —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (ξ-·₁ β-μ)) ⟩
+    (ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
+      ((ƛ ƛ (case (# 1) `zero (plus · # 1 · (mul · # 0 · # 1)))) · `zero · one)
+  —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-zero)) ⟩
+    (ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
+      ((ƛ (case `zero `zero (plus · # 1 · (mul · # 0 · # 1)))) · one)
+  —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
+    (ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
+      (case `zero `zero (plus · one · (mul · # 0 · one)))
+  —→⟨ ξ-·₂ V-ƛ β-zero ⟩
+    (ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) · `zero
+  —→⟨ β-ƛ V-zero ⟩
+    case one `zero (`suc (plus · # 0 · `zero))
+  —→⟨ β-suc V-zero ⟩
+    `suc (plus · `zero · `zero)
+  —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
+    `suc ((ƛ ƛ (case (# 1) (# 0) (`suc (plus · # 0 · # 1)))) · `zero · `zero)
+  —→⟨ ξ-suc (ξ-·₁ (β-ƛ V-zero)) ⟩
+    `suc ((ƛ (case `zero (# 0) (`suc (plus · # 0 · # 1)))) · `zero)
+  —→⟨ ξ-suc (β-ƛ V-zero) ⟩
+    `suc (case `zero `zero (`suc (plus · # 0 · `zero)))
+  —→⟨ ξ-suc β-zero ⟩
+    one
+  ∎

src/Homework3Prelude.agda

@@ -0,0 +1,241 @@
+-- This file contains the code extracted from the DeBruijn chapter in PLFA
+
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Decidable using (True; toWitness)
+
+module Homework3Prelude where
+
+infix  4 _⊢_
+infix  4 _∋_
+infixl 5 _,_
+
+infixr 7 _⇒_
+
+infix  5 ƛ_
+infix  5 μ_
+infixl 7 _·_
+infix  8 `suc_
+infix  9 `_
+infix  9 S_
+infix  9 #_
+
+data Type : Set where
+  _⇒_ : Type → Type → Type
+  `ℕ  : Type
+
+data Context : Set where
+  ∅   : Context
+  _,_ : Context → Type → Context
+
+data _∋_ : Context → Type → Set where
+
+  Z : ∀ {Γ A}
+      ---------
+    → Γ , A ∋ A
+
+  S_ : ∀ {Γ A B}
+    → Γ ∋ A
+      ---------
+    → Γ , B ∋ A
+
+data _⊢_ : Context → Type → Set where
+
+  `_ : ∀ {Γ A}
+    → Γ ∋ A
+      -----
+    → Γ ⊢ A
+
+  ƛ_  : ∀ {Γ A B}
+    → Γ , A ⊢ B
+      ---------
+    → Γ ⊢ A ⇒ B
+
+  _·_ : ∀ {Γ A B}
+    → Γ ⊢ A ⇒ B
+    → Γ ⊢ A
+      ---------
+    → Γ ⊢ B
+
+  `zero : ∀ {Γ}
+      ---------
+    → Γ ⊢ `ℕ
+
+  `suc_ : ∀ {Γ}
+    → Γ ⊢ `ℕ
+      ------
+    → Γ ⊢ `ℕ
+
+  case : ∀ {Γ A}
+    → Γ ⊢ `ℕ
+    → Γ ⊢ A
+    → Γ , `ℕ ⊢ A
+      ----------
+    → Γ ⊢ A
+
+  μ_ : ∀ {Γ A}
+    → Γ , A ⊢ A
+      ---------
+    → Γ ⊢ A
+
+length : Context → ℕ
+length ∅        =  zero
+length (Γ , _)  =  suc (length Γ)
+
+lookup : {Γ : Context} → {n : ℕ} → (p : n < length Γ) → Type
+lookup {(_ , A)} {zero}    (s≤s z≤n)  =  A
+lookup {(Γ , _)} {(suc n)} (s≤s p)    =  lookup p
+
+count : ∀ {Γ} → {n : ℕ} → (p : n < length Γ) → Γ ∋ lookup p
+count {_ , _} {zero}    (s≤s z≤n)  =  Z
+count {Γ , _} {(suc n)} (s≤s p)    =  S (count p)
+
+#_ : ∀ {Γ}
+  → (n : ℕ)
+  → {n∈Γ : True (suc n ≤? length Γ)}
+    --------------------------------
+  → Γ ⊢ lookup (toWitness n∈Γ)
+#_ n {n∈Γ}  =  ` count (toWitness n∈Γ)
+
+one : ∀ {Γ} → Γ ⊢ `ℕ
+one = `suc `zero
+
+two : ∀ {Γ} → Γ ⊢ `ℕ
+two = `suc `suc `zero
+
+plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
+plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
+
+ext : ∀ {Γ Δ}
+  → (∀ {A} →       Γ ∋ A →     Δ ∋ A)
+    ---------------------------------
+  → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
+ext ρ Z      =  Z
+ext ρ (S x)  =  S (ρ x)
+
+rename : ∀ {Γ Δ}
+  → (∀ {A} → Γ ∋ A → Δ ∋ A)
+    -----------------------
+  → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+rename ρ (` x)          =  ` (ρ x)
+rename ρ (ƛ N)          =  ƛ (rename (ext ρ) N)
+rename ρ (L · M)        =  (rename ρ L) · (rename ρ M)
+rename ρ (`zero)        =  `zero
+rename ρ (`suc M)       =  `suc (rename ρ M)
+rename ρ (case L M N)   =  case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
+rename ρ (μ N)          =  μ (rename (ext ρ) N)
+
+exts : ∀ {Γ Δ}
+  → (∀ {A} →       Γ ∋ A →     Δ ⊢ A)
+    ---------------------------------
+  → (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
+exts σ Z      =  ` Z
+exts σ (S x)  =  rename S_ (σ x)
+
+subst : ∀ {Γ Δ}
+  → (∀ {A} → Γ ∋ A → Δ ⊢ A)
+    -----------------------
+  → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+subst σ (` k)          =  σ k
+subst σ (ƛ N)          =  ƛ (subst (exts σ) N)
+subst σ (L · M)        =  (subst σ L) · (subst σ M)
+subst σ (`zero)        =  `zero
+subst σ (`suc M)       =  `suc (subst σ M)
+subst σ (case L M N)   =  case (subst σ L) (subst σ M) (subst (exts σ) N)
+subst σ (μ N)          =  μ (subst (exts σ) N)
+
+_[_] : ∀ {Γ A B}
+  → Γ , B ⊢ A
+  → Γ ⊢ B
+    ---------
+  → Γ ⊢ A
+_[_] {Γ} {A} {B} N M =  subst {Γ , B} {Γ} σ {A} N
+  where
+  σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
+  σ Z      =  M
+  σ (S x)  =  ` x
+
+data Value : ∀ {Γ A} → Γ ⊢ A → Set where
+
+  V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
+      ---------------------------
+    → Value (ƛ N)
+
+  V-zero : ∀ {Γ}
+      -----------------
+    → Value (`zero {Γ})
+
+  V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ}
+    → Value V
+      --------------
+    → Value (`suc V)
+
+infix 2 _—→_
+
+data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+  ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
+    → L —→ L′
+      ---------------
+    → L · M —→ L′ · M
+
+  ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
+    → Value V
+    → M —→ M′
+      ---------------
+    → V · M —→ V · M′
+
+  β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
+    → Value W
+      --------------------
+    → (ƛ N) · W —→ N [ W ]
+
+  ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
+    → M —→ M′
+      -----------------
+    → `suc M —→ `suc M′
+
+  ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+    → L —→ L′
+      -------------------------
+    → case L M N —→ case L′ M N
+
+  β-zero :  ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+      -------------------
+    → case `zero M N —→ M
+
+  β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+    → Value V
+      ----------------------------
+    → case (`suc V) M N —→ N [ V ]
+
+  β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
+      ----------------
+    → μ N —→ N [ μ N ]
+
+infix  2 _—↠_
+infix  1 begin_
+infixr 2 _—→⟨_⟩_
+infix  3 _∎
+
+data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+  _∎ : (M : Γ ⊢ A)
+      ------
+    → M —↠ M
+
+  _—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
+    → L —→ M
+    -- → L —↠ M
+    → M —↠ N
+      ------
+    → L —↠ N
+
+begin_ : ∀ {Γ A} {M N : Γ ⊢ A}
+  → M —↠ N
+    ------
+  → M —↠ N
+begin M—↠N = M—↠N

src/LambdaPi.agda

@@ -0,0 +1,81 @@
+module LambdaPi where
+
+open import Data.Nat using (ℕ; suc; _≟_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Nullary using (yes; no; ¬_)
+
+infix  4 _—→_
+infix  5  ƛ_
+infixl 7  _·_
+infix  9  `_
+infix  9 _[_:=_]
+
+data Term : Set where
+  -- var
+  `_ : ℕ → Term
+
+  -- lam
+  ƛ_ : Term → Term
+
+  -- app
+  _·_ : Term → Term → Term
+
+data Value : Term → Set where
+  -- lam is a value
+  V-ƛ : ∀ {N} → Value (ƛ N)
+
+----------------------------------------------------
+-- substitution
+----------------------------------------------------
+_[_:=_] : Term → ℕ → Term → Term
+
+-- var
+(` n₁) [ n₂ := V ] with n₁ ≟ n₂
+... | yes _ = V
+... | no _ = ` n₁
+
+-- lam 
+(ƛ N) [ n := V ] = ƛ (N [ suc n := V ])
+
+-- app
+(L · M) [ y := V ] = L [ y := V ] · M [ y := V ]
+
+----------------------------------------------------
+-- reduction
+----------------------------------------------------
+data _—→_ : Term → Term → Set where
+  -- beta reduction for lambda applications
+  β-ƛ : ∀ {x N V} → Value V → (ƛ N) · V —→ N [ x := V ]
+
+----------------------------------------------------
+-- typing
+----------------------------------------------------
+data Type : Set where
+  _⇒_ : Type → Type → Type
+  `ℕ : Type
+
+----------------------------------------------------
+-- typing context
+----------------------------------------------------
+data Context : Set where
+  ∅ : Context
+  _::_ : Type → Context
+
+----------------------------------------------------
+-- typing judgment
+----------------------------------------------------
+data _⊢_⦂_ : Context → Term → Type → Set where
+
+----------------------------------------------------
+-- progress
+----------------------------------------------------
+data Progress (M : Term) : Set where
+  step : ∀ {N} → M —→ N → Progress M
+  done : Value M → Progress M
+
+progress : ∀ {M A} → ∅ ⊢ M ⦂ A → Progress M
+
+----------------------------------------------------
+-- preservation
+----------------------------------------------------
+preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N → ∅ ⊢ N ⦂ A

src/LambdaTest.agda

@@ -0,0 +1,27 @@
+module LambdaTest where
+
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; _≢_; refl; sym; cong; cong₂)
+open import Data.String using (String; _≟_)
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Product
+  using (_×_; proj₁; proj₂; ∃; ∃-syntax)
+  renaming (_,_ to ⟨_,_⟩)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Function using (_∘_)
+V¬—→ V-ƛ = ?
+V¬—→ V-zero = ?
+V¬—→ (V-suc v) (ξ-suc m) = ?
+V¬—→ V-zero = ?
+V¬—→ (V-suc v) = ?
+open import plfa.part2.Lambda
+
+V¬—→ : ∀ {M N}
+  → Value M
+    ----------
+  → ¬ (M —→ N)
+V¬—→ V-ƛ ()
+V¬—→ V-zero ()
+V¬—→ (V-suc v) (ξ-suc m) = V¬—→ v m

src/OtherShit.agda

@@ -0,0 +1,30 @@
+module OtherShit where
+
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+open import Data.Nat
+open import Data.Nat.Properties
+open import Data.Unit
+open import Data.Empty
+
+data Bin : Set where
+  O : Bin
+  _I : Bin → Bin
+  _II : Bin → Bin
+
+data even : ℕ → Set
+data odd  : ℕ → Set
+
+data even where
+  zero : even zero
+  suc  : ∀ {n : ℕ} → odd n → even (suc n)
+
+data odd where
+  suc  : ∀ {n : ℕ} → even n → odd (suc n)
+
+to : ℕ → Bin
+to zero = O
+to n with odd n
+... | x = O I
+to n with even n
+... | x = O II

src/Project/Lambda1.agda

@@ -0,0 +1,19 @@
+module Project.Lambda1 where
+
+open import Data.Nat using (ℕ; suc; _≟_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Nullary using (yes; no; ¬_)
+
+data Term : Set where
+  `_ : ℕ →  Term
+  ƛ_ : Term →  Term
+  _·_ : Term →  Term →  Term
+
+  `suc _ : Term →  Term
+  `zero : Term
+
+data Value : Term →  Set where
+  V-ƛ : ∀ {N} →  Value (ƛ N)
+
+data Context : Set where
+  ⊙ : Context

src/plfa/part1/Induction.lagda.md

@@ -868,7 +868,17 @@ just apply the previous results which show addition
 is associative and commutative.
 
 ```
--- Your code goes here
++-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
++-swap m n p =
+  begin
+    m + (n + p)
+  ≡⟨ sym (+-assoc m n p) ⟩
+    (m + n) + p
+  ≡⟨ cong (_+ p) (+-comm m n) ⟩
+    (n + m) + p
+  ≡⟨ +-assoc n m p ⟩
+    n + (m + p)
+  ∎
 ```
 
 
@@ -881,7 +891,33 @@ Show multiplication distributes over addition, that is,
 for all naturals `m`, `n`, and `p`.
 
 ```
--- Your code goes here
+*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
+*-distrib-+ zero n p =
+  begin
+    (zero + n) * p
+  ≡⟨ cong (_* p) (+-comm zero n) ⟩
+    (n + zero) * p
+  ≡⟨ cong (_* p) (+-identityʳ n) ⟩
+    n * p
+  ∎
+*-distrib-+ (suc m) n p =
+  begin
+    (suc m + n) * p
+  ≡⟨ cong (_* p) (+-comm (suc m) n) ⟩
+    (n + suc m) * p
+  ≡⟨ cong (_* p) (+-suc n m) ⟩
+    suc (n + m) * p
+  ≡⟨ cong (_* p) (cong suc (+-comm n m)) ⟩
+    suc (m + n) * p
+  ≡⟨⟩
+    p + (m + n) * p
+  ≡⟨ cong (p +_) (*-distrib-+ m n p) ⟩
+    p + (m * p + n * p)
+  ≡⟨ sym (+-assoc p (m * p) (n * p)) ⟩
+    p + m * p + n * p
+  ≡⟨⟩
+    suc m * p + n * p
+  ∎
 ```
 
 
@@ -895,6 +931,17 @@ for all naturals `m`, `n`, and `p`.
 
 ```
 -- Your code goes here
+*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
+*-assoc zero n p =
+  begin
+    (zero * n) * p
+  ∎
+*-assoc (suc m) n p =
+  begin
+    (suc m * n) * p
+  ≡⟨  ⟩
+    
+  ∎
 ```
 
 

src/plfa/part1/Naturals.lagda.md

@@ -81,7 +81,7 @@ successor of two; and so on.
 Write out `7` in longhand.
 
 ```
--- Your code goes here
+_ = suc (suc (suc (suc (suc (suc (suc zero))))))
 ```
 
 
@@ -427,7 +427,8 @@ other word for evidence, which we will use interchangeably, is _proof_.
 
 #### Exercise `+-example` (practice) {name=plus-example}
 
-Compute `3 + 4`, writing out your reasoning as a chain of equations, using the equations for `+`.
+Compute `3 + 4`, writing out your reasoning as a chain of equations, using the
+equations for `+`.
 
 ```
 -- Your code goes here
@@ -506,7 +507,9 @@ Define exponentiation, which is given by the following equations:
 Check that `3 ^ 4` is `81`.
 
 ```
--- Your code goes here
+_^_ : ℕ → ℕ → ℕ
+m ^ zero = 1
+m ^ suc n = m * ( m ^ n)
 ```
 
 
@@ -919,6 +922,29 @@ Confirm that these both give the correct answer for zero through four.
 
 ```
 -- Your code goes here
+inc : Bin → Bin
+inc ⟨⟩ = ⟨⟩ O
+inc (n O) = n I
+inc (⟨⟩ I) = ⟨⟩ I O
+inc (n I) = (inc n) O
+
+_ : inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
+_ = refl
+
+to : ℕ → Bin
+to zero = ⟨⟩ O
+to (suc n) = inc (to n)
+
+from : Bin → ℕ
+from ⟨⟩ = 0
+from (n O) = 2 * (from n)
+from (n I) = 2 * (from n) + 1
+
+_ : to 12 ≡ ⟨⟩ I I O O
+_ = refl
+
+_ : from (⟨⟩ I O I I) ≡ 11
+_ = refl
 ```
 
 

src/plfa/part1/Relations.lagda.md

@@ -754,7 +754,15 @@ successor of the sum of two even numbers, which is even.
 Show that the sum of two odd numbers is even.
 
 ```
--- Your code goes here
+import Data.Nat.Properties
+open Data.Nat.Properties using (+-suc)
+
+o+o≡e : ∀ {m n : ℕ}
+  → odd m → odd n
+  → even (m + n)
+
+-- o+o≡e om (suc en) = suc (+-suc (o+e≡o om en))
+o+o≡e om (suc en) = +-suc ?
 ```
 
 #### Exercise `Bin-predicates` (stretch) {name=Bin-predicates}

src/plfa/part2/Lambda.lagda.md

@@ -197,7 +197,11 @@ two natural numbers.  Your definition may use `plus` as
 defined earlier.
 
 ```
--- Your code goes here
+mul : Term
+mul = μ "*" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
+         case ` "m"
+           [zero⇒ ` "n"
+           |suc "m" ⇒ ` "+" · ` "n" · (` "*" · ` "m" · ` "n") ]
 ```
 
 
@@ -209,7 +213,8 @@ definition may use `plusᶜ` as defined earlier (or may not
 — there are nice definitions both ways).
 
 ```
--- Your code goes here
+mulᶜ : Term
+mulᶜ =  ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ (` "m" · (` "n" · ` "s") · ` "z")
 ```
 
 
@@ -262,6 +267,18 @@ plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
 ```
 Write out the definition of multiplication in the same style.
 
+```
+mul′ : Term
+mul′ = μ′ * ⇒ ƛ′ m ⇒ ƛ′ n ⇒
+          case′ m
+            [zero⇒ n
+            |suc m ⇒ plus′ · n · (* · m · n) ]
+  where
+  *  =  ` "*"
+  m  =  ` "m"
+  n  =  ` "n"
+```
+
 
 ### Formal vs informal
 
@@ -542,6 +559,7 @@ substitution.
 
 ```
 -- Your code goes here
+
 ```
 
 
@@ -1038,7 +1056,34 @@ to the list
     [ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ]
 
 ```
--- Your code goes here
+open import plfa.part1.Isomorphism using (_≃_)
+open import Data.Product using (_×_; _,_)
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning renaming (begin_ to begin-≡_; _∎ to _∎-≡)
+
+contextOfList : (l : List (Id × Type)) →  Context
+contextOfList [] = ∅
+contextOfList ((id , type) ∷ l) = (contextOfList l) , id ⦂ type
+
+listOfContext : (c : Context) →  List (Id × Type)
+listOfContext ∅ = []
+listOfContext (c , x ⦂ x₁) = (x , x₁) ∷ listOfContext c
+
+contextListIso : (c : Context) →  contextOfList (listOfContext c) ≡ c
+contextListIso ∅ = refl
+contextListIso (c , x ⦂ x₁) = cong (_, x ⦂ x₁) (contextListIso c)
+
+listContextIso : (l : List (Id × Type)) →  listOfContext (contextOfList l) ≡ l
+listContextIso [] = refl
+listContextIso (x ∷ l) = cong (x ∷_) (listContextIso l)
+
+Context≃List : Context ≃ List (Id × Type)
+Context≃List = record
+  { from = contextOfList
+  ; to = listOfContext
+  ; from∘to = contextListIso
+  ; to∘from = listContextIso
+  }
 ```
 
 ### Lookup judgment