diff --git a/README.md b/README.md
index 48f7b08..1598931 100644
--- a/README.md
+++ b/README.md
@@ -128,21 +128,7 @@ solution.
 
     Introduces refinement types
 
-  - [Day 12](src/Years/Y2015/Day12.md)
-
-    New Parser Effect stack and DLists
-
-  - [Day 13](src/Years/Y2015/Day13.md)
-
-    Naive ring buffer and `parameters` blocks[^2]
-
-  - [Day 14](src/Years/Y2015/Day14.md)
-
-    Introduction to streams, infinite collections of data
-
 ## References
 
 [^1]: Idris 2 Manual:
     [Views and the "with" rule](https://idris2.readthedocs.io/en/latest/tutorial/views.html#views-and-the-with-rule)
-
-[^2]: <https://idris2.readthedocs.io/en/latest/tutorial/modules.html#parameterised-blocks-parameters-blocks>
diff --git a/advent.ipkg b/advent.ipkg
index d4d13fe..607e26e 100644
--- a/advent.ipkg
+++ b/advent.ipkg
@@ -41,7 +41,7 @@ main = Main
 
 -- name of executable
 executable = "advent"
-opts = "--directive lazy=weakMemo"
+-- opts =
 sourcedir = "src"
 -- builddir =
 -- outputdir =
diff --git a/book.toml b/book.toml
index a4387d0..4ad1625 100644
--- a/book.toml
+++ b/book.toml
@@ -7,7 +7,7 @@ title = "Idris 2 by Highly Contrived Example"
 
 [build]
 create-missing = false
-# use-default-preprocessors = false
+use-default-preprocessors = false
 
 [output.html]
 preferred-dark-theme = "ayu"
diff --git a/scripts/build-book b/scripts/build-book
index fd108e3..8513e4d 100755
--- a/scripts/build-book
+++ b/scripts/build-book
@@ -23,7 +23,7 @@ sub not-ignored($path) {
 # Copy a file from the current directory to the temporary directory, preserving
 # realtive path. Resolves symlinks in source, but does not reflect symlink
 # resoultion in the output path
-sub copy-to-dest($src) {
+sub cp-temp($src) {
    my $src-path = do given $src {
        when Str {
            $src.IO
@@ -45,16 +45,40 @@ sub copy-to-dest($src) {
    $src-path.resolve.copy: $output-path;
 }
 
-# Special handling for our readme file, we need to butcher up it's links
-my $readme-contents = 'README.md'.IO.slurp;
-$readme-contents ~~ s:g/'src/'//;
-my $readme-dest = $tempdir.add('src/README.md');
-$readme-dest.parent.mkdir;
-$readme-dest.spurt: $readme-contents;
+# Invoke katla on a source file, streaming its output to the temporary directory
+sub katla($src, $ttc-src) {
+    # Run katla and collect the output
+    my $katla = run 'katla', 'markdown', $src, $ttc-src, :out;
+    my $output = $katla.out.slurp(:close);
+    # TODO: Post process them to set themeing correctly
+    $output ~~ s:g/'<style>' .* '</style>'//;
+    $output ~~ s:g/'<br />'//;
+    $output ~~ s:g/'\\*'/*/;
+    $output ~~ s:g/'\\_'/_/;
+    $output ~~ s:g/'\\\\'/\\/;
+    $output ~~ s:g/'<code'/<pre><code/;
+    $output ~~ s:g/'</code>'/<\/code><\/pre>/;
+    $output ~~ s:g/'class="IdrisKeyword"'/class="hljs-keyword"/;
+    $output ~~ s:g/'class="IdrisModule"'/class="hljs-symbol hljs-emphasis"/;
+    $output ~~ s:g/'class="IdrisComment"'/class="hljs-comment"/;
+    $output ~~ s:g/'class="IdrisFunction"'/class="hljs-symbol"/;
+    $output ~~ s:g/'class="IdrisBound"'/class="hljs-name"/;
+    $output ~~ s:g/'class="IdrisData"'/class="hljs-title"/;
+    $output ~~ s:g/'class="IdrisType"'/class="hljs-type"/;
+    $output ~~ s:g/'class="IdrisNamespace"'/class="hljs-symbol hljs-emphasis"/;
+
+    # Spurt the output to the temporary directory
+    my $output-path = $tempdir.add: $src;
+    if !$output-path.parent.d {
+        $output-path.parent.mkdir;
+    }
+    $output-path.spurt($output);
+}
 
 # Copy our metadata files
-copy-to-dest "book.toml";
-copy-to-dest "src/SUMMARY.md";
+cp-temp "book.toml";
+cp-temp "src/README.md";
+cp-temp "src/SUMMARY.md";
 
 # Katla over the source files
 for paths("src", :file(*.&not-ignored)) -> $path {
@@ -74,42 +98,7 @@ rm_rf "book";
 cp $tempdir.add("book"), "book", :r;
 
 if $upload {
-    my $rsync = run 'rsync', '-avzh', $tempdir.add("book/").Str,
-                'ubuntu@static.stranger.systems:/var/www/static.stranger.systems/idris-by-contrived-example';
-    die "rsync went bad" unless $rsync;
-}
-
-# This function goes at the end because it breaks emacs fontification after it
-# for some bizzare reason.
-#
-# Invoke katla on a source file, streaming its output to the temporary directory
-sub katla($src, $ttc-src) {
-    # Run katla and collect the output
-    my $katla = run 'katla', 'markdown', $src, $ttc-src, :out;
-    my $output = $katla.out.slurp(:close);
-    # Post process them to set themeing correctly
-    # TODO: We need to remove the extra new line after the start of code blocks
-    # still
-    $output ~~ s:g/'<style>' .* '</style>'//;
-    $output ~~ s:g/'<br />'//;
-    $output ~~ s:g/'\\*'/*/;
-    $output ~~ s:g/'\\_'/_/;
-    $output ~~ s:g/'\\\\'/\\/;
-    $output ~~ s:g/'<code'/<pre><code/;
-    $output ~~ s:g/'</code>'/<\/code><\/pre>/;
-    $output ~~ s:g/'="IdrisKeyword"'/="hljs-keyword"/;
-    $output ~~ s:g/'="IdrisModule"'/="hljs-symbol hljs-emphasis"/;
-    $output ~~ s:g/'="IdrisComment"'/="hljs-comment"/;
-    $output ~~ s:g/'="IdrisFunction"'/="hljs-symbol"/;
-    $output ~~ s:g/'="IdrisBound"'/="hljs-name"/;
-    $output ~~ s:g/'="IdrisData"'/="hljs-title"/;
-    $output ~~ s:g/'="IdrisType"'/="hljs-type"/;
-    $output ~~ s:g/'="IdrisNamespace"'/="hljs-symbol hljs-emphasis"/;
-
-    # Spurt the output to the temporary directory
-    my $output-path = $tempdir.add: $src;
-    if !$output-path.parent.d {
-        $output-path.parent.mkdir;
-    }
-    $output-path.spurt($output);
+   my $rsync = run 'rsync', '-avzh', $tempdir.add("book").Str,
+       'ubuntu@static.stranger.systems:/var/www/static.stranger.systems/idris-by-contrived-example';
+   die "rsync went bad" unless $rsync;
 }
diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md
index 53be055..79583cf 100644
--- a/src/Parser/Interface.md
+++ b/src/Parser/Interface.md
@@ -110,8 +110,7 @@ Provide wrappers for `rundownFirst` for evaluating it in various contexts.
 
 ```idris
 export
-runFirstIO : HasIO io => MonadRec io =>
-  (f : Parser a) -> String -> io (Either ParseError a)
+runFirstIO : (f : Parser a) -> String -> IO (Either ParseError a)
 runFirstIO f str = do
   Just state <- newInternalIO str
     | _ => pure . Left $ BeforeParse "Empty input"
diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index 7baf9fa..6602210 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -6,8 +6,6 @@ module Parser.JSON
 import public Parser
 import public Parser.Numbers
 
-import Control.Monad.Eval
-
 import Structures.Dependent.DList
 ```
 
@@ -57,7 +55,6 @@ data JSONValue : JSONType -> Type where
 ```
 
 ```idris hide
-export
 Show (JSONValue t) where
   show (VObject xs) = 
     let xs = dMap (\_,(key, value) => "\"\{key}\":\{show value}") xs
@@ -72,7 +69,6 @@ Show (JSONValue t) where
   show VNull = "null"
 
 -- TODO: Deal with keys potentially having different orders in different objects
-export
 Eq (JSONValue t) where
   (VObject xs) == (VObject ys) = 
     assert_total $ xs $== ys
@@ -86,96 +82,6 @@ Eq (JSONValue t) where
 %hide Language.Reflection.TT.WithFC.value
 ```
 
-### JSON Functions
-
-`foldl` Analog for consuming a JSON structure by values. Ignores the keys in
-objects.
-
-```idris
-export
-dFoldL : {t : JSONType} 
-  -> (acc -> (type : JSONType) -> (val : JSONValue type) -> acc) 
-  -> acc -> JSONValue t -> acc
-dFoldL f acc' (VObject xs) = 
-  let recur : acc -> (v : JSONType) -> (String, JSONValue v) -> acc
-      recur acc' v (key, value) = dFoldL f acc' value
-  in DList.dFoldL recur acc' xs
-dFoldL f acc' (VArray xs) = 
-  let recur : acc -> (v : JSONType) -> JSONValue v -> acc
-      recur acc' v value = dFoldL f acc' value
-  in DList.dFoldL recur acc' xs
-dFoldL f acc (VString s) = f acc _ (VString s)
-dFoldL f acc (VNumber d) = f acc _ (VNumber d)
-dFoldL f acc (VBool b) = f acc _ (VBool b)
-dFoldL f acc VNull = f acc _ VNull
-```
-
-Look up a property in an object
-
-```idris
-export
-getProperty : (prop : String) -> (object : JSONValue TObject)
-  -> Maybe (type : JSONType ** JSONValue type)
-getProperty prop (VObject xs) = 
-  case dFind (\_, (key, _) => key == prop) xs of
-    Nothing => Nothing
-    Just (type ** (_, val)) => Just (type ** val)
-```
-
-Return the values from an object.
-
-```idris
-export
-getValues : (object : JSONValue TObject) 
-  -> (types : List JSONType ** DList JSONType JSONValue types)
-getValues (VObject xs) = 
-  dMap' (\t, (k, v) => (t ** v)) xs
-```
-
-Recursively apply a filter to a JSON structure.
-
-```idris
-export
-dFilter : (f : (type : JSONType) -> (val : JSONValue type) -> Bool) 
-  -> {t : JSONType} -> JSONValue t -> Maybe (JSONValue t)
-dFilter f value = eval $ dFilter' f value
-  where
-    dFilter' : (f : (type : JSONType) -> (val : JSONValue type) -> Bool) 
-      -> {t : JSONType} -> JSONValue t -> Eval $ Maybe (JSONValue t)
-    dFilter' f (VObject xs) = do
-      True <- pure $ f _ (VObject xs)
-        | _ => pure Nothing
-      let xs = toList xs
-      xs : List (Maybe (x : JSONType ** (String, JSONValue x))) <- 
-        traverse
-          (\(t ** (k, v)) => do
-            Just v <- dFilter' f v
-              | _ => pure Nothing
-            pure $ Just (t ** (k, v)))
-          xs
-      let (_ ** xs) : (t : List JSONType ** DList _ _ t) = 
-        fromList $ catMaybes xs
-      pure . Just $ VObject xs
-    dFilter' f (VArray xs) = do 
-      True <- pure $ f _ (VArray xs)
-        | _ => pure Nothing
-      let xs = toList xs
-      xs : List (Maybe (x : JSONType ** JSONValue x)) <- 
-        traverse
-          (\(t ** v) => do
-            Just v <- dFilter' f v
-              | _ => pure Nothing
-            pure $ Just (t ** v))
-          xs
-      let (_ ** xs) : (t : List JSONType ** DList _ _ t) = 
-        fromList $ catMaybes xs
-      pure . Just $ VArray xs
-    dFilter' f x =
-      pure $ case f _ x of
-        False => Nothing
-        True => Just x
-```
-
 ## Parsers
 
 We are going to get mutually recursive here. Instead of using a `mutual` block,
@@ -262,7 +168,6 @@ object = do
     pairs = do
       first <- keyValue
       rest <- many restKeyValue
-      -- TODO: headTail combinator for this
       pure $ first ::: rest
     occupiedObject : Parser (JSONValue TObject)
     occupiedObject = do
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 3fad4c9..2cf1e0b 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -33,6 +33,3 @@
   - [Day 9 - Naive Graph Traversal](Years/Y2015/Day9.md)
   - [Day 10 - Digits View](Years/Y2015/Day10.md)
   - [Day 11 - Refinement Types](Years/Y2015/Day11.md)
-  - [Day 12 - Custom Parser Effect and DLists](Years/Y2015/Day12.md)
-  - [Day 13 - Naive Ring Buffer and parameters blocks](Years/Y2015/Day13.md)
-  - [Day 14 - Introduction to Streams](Years/Y2015/Day14.md)
diff --git a/src/Util.md b/src/Util.md
index 7d1342e..4e8de44 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -10,50 +10,10 @@ import Data.SortedSet
 import Data.String
 import Data.List.Lazy
 import Data.List1
-import Data.Vect
-import Data.Fin
 
 %default total
 ```
 
-## Foldable
-
-General utility functions for foldables
-
-```idris hide
-namespace Foldable
-```
-
-### minBy
-
-```idris
-  ||| Get the minimum element of a collection using the provided comparison
-  ||| function and seed value
-  export
-  minBy : Foldable f => (cmp : a -> a -> Ordering) -> (acc : a) -> f a -> a
-  minBy cmp acc x = 
-    foldl 
-      (\acc, e => 
-        case e `cmp` acc of
-          LT => e
-          _ => acc)
-      acc x
-```
-
-```idris
-  ||| Get the maximum element of a collection using the provided comparison
-  ||| function and seed value
-  export
-  maxBy : Foldable f => (cmp : a -> a -> Ordering) -> (acc : a) -> f a -> a
-  maxBy cmp acc x = 
-    foldl 
-      (\acc, e => 
-        case e `cmp` acc of
-          GT => e
-          _ => acc)
-      acc x
-```
-
 ## Functions
 
 ### repeatN
@@ -96,13 +56,13 @@ namespace List
 Returns `True` if the list contains the given value
 
 ```idris
-  export
-  contains : Eq a => a -> List a -> Bool
-  contains x [] = False
-  contains x (y :: xs) = 
-    if x == y 
-      then True
-      else contains x xs
+export
+contains : Eq a => a -> List a -> Bool
+contains x [] = False
+contains x (y :: xs) = 
+  if x == y 
+    then True
+    else contains x xs
 ```
 
 ### rotations
@@ -116,102 +76,16 @@ rotations [1, 2, 3] == [[1, 2, 3], [3, 1, 2], [2, 3, 1]]
 ```
 
 ```idris
-  export
-  rotations : List a -> List (List a) 
-  rotations xs = rotations' (length xs) xs []
-    where
-      rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a)
-      rotations' 0 xs acc = acc
-      rotations' (S k) [] acc = acc
-      rotations' (S k) (x :: xs) acc = 
-        let next = xs ++ [x]
-        in rotations' k next (next :: acc)
-```
-
-### permutations
-
-Lazily generate all of the permutations of a list
-
-```idris
-  export
-  permutations : List a -> LazyList (List a)
-  permutations [] = pure []
-  permutations xs = do
-    (head, tail) <- select xs
-    tail <- permutations (assert_smaller xs tail)
-    pure $ head :: tail
-    where 
-      consSnd : a -> (a, List a) -> (a, List a)
-      consSnd x (y, xs) = (y, x :: xs)
-      select : List a -> LazyList (a, List a)
-      select [] = []
-      select (x :: xs) = (x, xs) :: map (consSnd x) (select xs)
-```
-
-## Vect
-
-```idris hide
-namespace Vect
-```
-
-### permutations
-
-Lazily generate all the permutations of a Vect
-
-```idris
-  export
-  permutations : Vect n a -> LazyList (Vect n a)
-  permutations [] = []
-  permutations [x] = [[x]]
-  permutations (x :: xs) = do
-    (head, tail) <- select (x :: xs)
-    tail <- permutations tail
-    pure $ head :: tail
-    where
-      consSnd : a -> (a, Vect m a) -> (a, Vect (S m) a)
-      consSnd x (y, xs) = (y, x :: xs)
-      select : Vect (S m) a -> LazyList (a, Vect m a)
-      select [y] = [(y, [])]
-      select (y :: (z :: ys)) = 
-        (y, z :: ys) :: map (consSnd y) (select (z :: ys))
-```
-
-### minBy and maxBy
-
-```idris
-  ||| Get the minimum element of a non-empty vector by using the provided
-  ||| comparison function 
-  export
-  minBy : (f : a -> a -> Ordering) -> Vect (S n) a -> a
-  minBy f (x :: xs) = Foldable.minBy f x xs
-
-  ||| Get the maximum element of a non-empty vector by using the provided
-  ||| comparison function 
-  export
-  maxBy : (f : a -> a -> Ordering) -> Vect (S n) a -> a
-  maxBy f (x :: xs) = Foldable.maxBy f x xs
-```
-
-### Convert a list to a vect as a sigma type
-
-```idris
-  export
-  listToVect : List a -> (n : Nat ** Vect n a)
-  listToVect xs = (length xs ** fromList xs)
-```
-
-## Fin
-
-```idris hide
-namespace Fin
-```
-
-```idris
-  ||| Decriment a Fin, wrapping on overflow
-  export
-  unfinS : {n : _} -> Fin n -> Fin n
-  unfinS FZ = last
-  unfinS (FS x) = weaken x
+export
+rotations : List a -> List (List a) 
+rotations xs = rotations' (length xs) xs []
+  where
+    rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a)
+    rotations' 0 xs acc = acc
+    rotations' (S k) [] acc = acc
+    rotations' (S k) (x :: xs) acc = 
+      let next = xs ++ [x]
+      in rotations' k next (next :: acc)
 ```
 
 ## Vectors
@@ -292,24 +166,20 @@ off of the string at a time, checking if the needle is a prefix at each step.
 
 ### Cartesian product
 
-```idris hide
-namespace LazyList
-```
-
 Lazily take the cartesian product of two foldables
 
 ```idris
-  export
-  cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f)
-  cartProd x y = 
-    let y = foldToLazy y
-    in foldr (\e, acc => combine e y acc) [] x
-    where
-      foldToLazy : Foldable a' => a' e' -> LazyList e'
-      foldToLazy x = foldr (\e, acc => e :: acc) [] x
-      combine : e -> LazyList f -> LazyList (e, f) -> LazyList (e, f)
-      combine x [] rest = rest
-      combine x (y :: ys) rest = (x, y) :: combine x ys rest
+export
+cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f)
+cartProd x y = 
+  let y = foldToLazy y
+  in foldr (\e, acc => combine e y acc) [] x
+  where
+    foldToLazy : Foldable a' => a' e' -> LazyList e'
+    foldToLazy x = foldr (\e, acc => e :: acc) [] x
+    combine : e -> LazyList f -> LazyList (e, f) -> LazyList (e, f)
+    combine x [] rest = rest
+    combine x (y :: ys) rest = (x, y) :: combine x ys rest
 ```
 
 ### Concat
@@ -317,10 +187,10 @@ Lazily take the cartesian product of two foldables
 Lazily concatenate a LazyList of LazyLists
 
 ```idris
-  export
-  lazyConcat : LazyList (LazyList a) -> LazyList a
-  lazyConcat [] = []
-  lazyConcat (x :: xs) = x ++ lazyConcat xs
+export
+lazyConcat : LazyList (LazyList a) -> LazyList a
+lazyConcat [] = []
+lazyConcat (x :: xs) = x ++ lazyConcat xs
 ```
 
 ### Group
@@ -328,30 +198,15 @@ Lazily concatenate a LazyList of LazyLists
 Lazily group a LazyList
 
 ```idris
-  export
-  lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
-  lazyGroup [] = []
-  lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
-    where
-      lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a)
-        -> LazyList (List1 a)
-      lazyGroup' [] current acc = [acc]
-      lazyGroup' (y :: ys) current acc@(head ::: tail) = 
-        if y == current
-          then lazyGroup' ys current (head ::: (y :: tail))
-          else acc :: lazyGroup (y :: ys)
-```
-
-### length
-
-Calculate the length of a LazyList
-
-```idris
-  export
-  length : LazyList a -> Nat
-  length = length' 0
-    where
-      length' : Nat -> LazyList a -> Nat
-      length' k [] = k
-      length' k (x :: xs) = length' (S k) xs
+export
+lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
+lazyGroup [] = []
+lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
+  where
+    lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a) -> LazyList (List1 a)
+    lazyGroup' [] current acc = [acc]
+    lazyGroup' (y :: ys) current acc@(head ::: tail) = 
+      if y == current
+        then lazyGroup' ys current (head ::: (y :: tail))
+        else acc :: lazyGroup (y :: ys)
 ```
diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md
index d4a3b19..c2a0326 100644
--- a/src/Years/Y2015.md
+++ b/src/Years/Y2015.md
@@ -18,9 +18,6 @@ import Years.Y2015.Day8
 import Years.Y2015.Day9
 import Years.Y2015.Day10
 import Years.Y2015.Day11
-import Years.Y2015.Day12
-import Years.Y2015.Day13
-import Years.Y2015.Day14
 ```
 
 # Days
@@ -97,24 +94,6 @@ y2015 = MkYear 2015 [
   , day11
 ```
 
-## [Day 12](Y2015/Day12.md)
-
-```idris
-  , day12
-```
-
-## [Day 13](Y2015/Day13.md)
-
-```idris
-  , day13
-```
-
-## [Day 14](Y2015/Day14.md)
-
-```idris
-  , day14
-```
-
 ```idris
   ]
 ```
diff --git a/src/Years/Y2015/Day12.md b/src/Years/Y2015/Day12.md
deleted file mode 100644
index 2829698..0000000
--- a/src/Years/Y2015/Day12.md
+++ /dev/null
@@ -1,132 +0,0 @@
-# [Year 2015 Day 12](https://adventofcode.com/2015/day/12)
-
-This day provides an introduction to our new
-[`Parser.JSON`](../../Parser/JSON.md) module, as well as the use of `DList`s[^1]
-to collect values from an indexed type family into a single collection.
-
-```idris hide
-module Years.Y2015.Day12
-
-import Control.Eff
-
-import Runner
-```
-
-```idris
-import Structures.Dependent.DList
-
-import Parser
-import Parser.JSON
-```
-
-## Parsing
-
-Parse a list of JSON values into a `DList`.
-
-`JSONValue`'s type constructor has the signature `JSONType -> Type`, forming
-what is known as an "Indexed Type Family".
-
-Each type of JSON value has a separate type, e.g. a Bool has type
-`JSONValue TBool`, a String has type `JSONValue TString`, etc. While these are
-all separate types, they all share the `JSONValue` component of the type
-constructor, making them members of the same family.
-
-Despite being members of the same type family, they still have different types,
-so we can't just shove `JSONValue`s of different types into, say, a
-`List JSONValue`, we need a collection with some amount of heterogeneity. While
-a `List (type : JSONType ** JSONValue type)` would _work_, that introduces
-various ergonomic headaches, so instead we return a `DList`[^1], a `List` like
-data structure specifically designed for collecting values from an indexed typed
-family into a single collection.
-
-The parsing logic is otherwise quite simple, we use the `many` combinator to
-turn the `value` parser, which parses a single JSON value, into one that parses
-a list of JSON values, and then use `DList`'s `fromList` method to collect the
-results into a `DList`.
-
-```idris
-parseJsons : Has (Except String) fs => Has IO fs => (input : String)
-  -> Eff fs (types : List JSONType ** DList JSONType JSONValue types) 
-parseJsons input = do
-  result <- runFirstIO (many value) input
-  case result of
-    Left err => throw $ show err
-    Right result => pure $ fromList result
-```
-
-## Solving
-
-A reducer for `DList.dFoldL` that sums all the numbers within the contained JSON
-Value.
-
-The outer function is meant to be called on a top level object, using
-`DList.dFoldL` on a `DList` of `JSONValue`s, where as the inner function
-directly reduces a `JSONValue` using `JSON.dFoldL`.
-
-```idris
-sumNumbers : Double -> (type : JSONType) -> (value : JSONValue type) -> Double
-sumNumbers dbl type value = dFoldL sumNumbers' dbl value
-  where
-    sumNumbers' : Double -> (type : JSONType) -> (value : JSONValue type) -> Double
-    sumNumbers' dbl TNumber (VNumber d) = dbl + d
-    sumNumbers' dbl _ value = dbl
-```
-
-Filter out objects containing a "red" key
-
-```idris
-noRed  : (type : JSONType) -> (value : JSONValue type) -> Bool
-noRed TObject value = 
-  let (types ** vals) = getValues value
-  in case dFind (\t, v => 
-                  case t of
-                    TString => v == (VString "red")
-                    _ => False
-                ) vals of
-    Nothing => True
-    Just _ => False
-noRed _ value = True
-
-sumNumbersNoRed : 
-  Double -> (type : JSONType) -> (value : JSONValue type) -> Double
-sumNumbersNoRed dbl type value = 
-  case dFilter noRed value of
-    Nothing => dbl
-    Just value => sumNumbers dbl type value
-```
-
-## Part Functions
-
-### Part 1
-
-Parse our JSONs, then fold our `sumNumbers` reducer over them.
-
-```idris
-part1 : Eff (PartEff String) 
-            (Double, (types : List JSONType ** DList JSONType JSONValue types))
-part1 = do
-  input <- askAt "input"
-  (types ** values) <- parseJsons input
-  let result = dFoldL sumNumbers 0.0 values
-  pure (result, (types ** values))
-```
-
-### Part 2
-
-```idris
-part2 : (types : List JSONType ** DList JSONType JSONValue types)
-  -> Eff (PartEff String) Double
-part2 (types ** values) = do
-  let result = dFoldL sumNumbersNoRed 0.0 values
-  pure result
-```
-
-```idris hide
-public export
-day12 : Day
-day12 = Both 12 part1 part2
-```
-
-## References
-
-[^1]: <https://git.sr.ht/~thatonelutenist/Structures/tree/trunk/item/src/Structures/Dependent/DList.md>
diff --git a/src/Years/Y2015/Day13.md b/src/Years/Y2015/Day13.md
deleted file mode 100644
index e0f7f89..0000000
--- a/src/Years/Y2015/Day13.md
+++ /dev/null
@@ -1,263 +0,0 @@
-# [Year 2015 Day 13](https://adventofcode.com/2015/day/13)
-
-This day exhibits a naive, `Vect` based implementation of a ring buffer, as well
-as our first introduction to `parameters` blocks.
-
-```idris hide
-module Years.Y2015.Day13
-
-import Data.Primitives.Interpolation
-
-import Control.Eff
-
-import Runner
-```
-
-```idris
-import Data.String
-import Data.List1
-import Data.List.Lazy
-import Data.Vect
-import Data.Maybe
-import Data.SortedMap.Dependent
-import Decidable.Equality
-
-import Util
-
-%default total
-```
-
-## Parsing and Data Structures
-
-```idris
-Name : Type
-Name = String
-
-Happiness : Type
-Happiness = Integer
-```
-
-Describe a change in happiness from a change in seating arrangement as data
-structure, indexed by the name of the individual whose happiness it describes,
-and provide some projections.
-
-```idris
-data Change : (changee : Name) -> Type where
-  NextTo : (changee : Name) -> (other : Name) -> (amount : Happiness)
-    -> Change (changee)
-
-(.changee) : Change changee -> Name
-(.changee) (NextTo changee _ _) = changee
-
-(.other) : Change changee -> Name
-(.other) (NextTo _ other _) = other
-
-(.amount) : Change changee -> Happiness
-(.amount) (NextTo _ _ amount) = amount
-```
-
-Collect the list of changes provided as input into a structure that encodes our
-assumptions at the type level.
-
-The changes are stored in a in a dependent map, with the name of the individual
-as the key, and lists of potential changes to their happiness as the values.
-
-This problem is a bit nicer to express in terms of a collection of known size,
-and we don't want to be constantly converting the keys list to a `Vect`, so we
-instead store it in `Changes` as a `Vect`. We don't want to accidentally store
-the wrong thing here, so we store an auto-implicit proof of equality,
-`keys_prf`, proving that the `names` list is exactly the list of keys in
-`change_map` converted to a Vect with `fromList`.
-
-It will also make things a bit nicer if we can assume that our `names` list is
-non-empty, after all it really doesn't make sense to talk about seating
-arrangements at a table with 0 people at it, so we store an auto-implict
-`nonempty` proof establishing that the length of `change_map`'s keys list, and
-thus `names`, is at least 1.
-
-```idris
-record Changes where
-  constructor MkChanges
-  change_map : SortedDMap Name (\n => List (Change n))
-  names : Vect (length (keys change_map)) Name
-  {auto keys_prf : names = fromList (keys change_map)}
-  {auto nonempty : IsSucc (length (keys change_map))}
-```
-
-Our usual pattern-matching based parsing of one element of the input, returning
-a dependent pair of the name of the individual this record describes, and the
-change described by that record.
-
-```idris
-parseChange : Has (Except String) fs => 
-  String -> Eff fs (name ** Change name)
-parseChange str = do
-  changee ::: [_, direction, amount, _, _, _, _, _, _, other] 
-    <- pure $ split (== ' ') str
-    | _ => throw "Invalid input string \{str}"
-  amount <- note "Invalid amount \{amount} in \{str}" $ parseInteger amount
-  amount : Happiness <-
-    case direction of
-      "gain" => pure amount
-      "lose" => pure $ negate amount
-      x      => throw "Invalid direction \{x} in \{str}" 
-  let other = pack . filter (/= '.') . unpack $ other
-  pure (_ ** (changee `NextTo` other) amount)
-```
-
-Parse the entire list of changes in the input, collecting them into a dependent
-map as we go along, and performing the checks needed for Idris to be satisfied
-that the conditions encoded by the auto-implict proofs in `Changes` are met.
-
-```idris
-parseChanges : Has (Except String) fs =>
-  List String -> (seed : SortedDMap Name (\n => List (Change n)))
-  -> Eff fs Changes
-parseChanges strs seed = do
-  changes <- traverse parseChange strs
-  let change_map = insertChanges changes seed
-  case isItSucc (length (keys change_map)) of
-    Yes prf => pure $ MkChanges change_map (fromList (keys change_map))
-    No contra => throw "Empty table, not very interesting"
-  where
-    insertChanges : List (name ** Change name) 
-      -> (acc : SortedDMap Name (\n => List (Change n)))
-      -> SortedDMap Name (\n => List (Change n))
-    insertChanges [] acc = acc
-    insertChanges ((name ** change) :: xs) acc = 
-      case lookupPrecise name acc of
-        Nothing => insertChanges xs (insert name [change] acc)
-        Just ys => insertChanges xs (insert name (change :: ys) acc)
-```
-
-## Solver functions
-
-All of these functions are about to take the same first argument,
-`(cs : Changes)`. This is a really common occurrence, especially when dealing
-with dependent proof types, so Idris has syntax sugar to avoid repeating your
-self in theses situations, `parameters` blocks[^1].
-
-A `parameters` block adds the provided arguments to the start of every top level
-signature contained within it, in this case, making the first argument of all of
-these functions have type `(cs : Changes)`. The arguments to the `parameters`
-blocks are also added to the front of the arguments list, using the names
-provided in the signature.
-
-`parameters` blocks also provide another fun bit of functionality that makes
-code within them more concise, within a `parameters` block, the parameters are
-implicitly passed as arguments to calls to functions in the same block.
-
-```idris
-parameters (cs : Changes)
-```
-
-Calculate the happiness change for a given person in a seating arrangement, use
-`finS` and `unfinS` to get the indexes of the parties seated to either side of
-us, and look them up in our map, adding the amount of change described by them
-together.
-
-Notice how `cs` appears neither in the arguments list, nor the type signature,
-yet we can still refer to it as if it was included at the start of both.
-
-```idris
-  happinessFor :
-    (arrangement : Vect (length (keys cs.change_map)) Name)
-    -> (idx : Fin (length (keys cs.change_map)))
-    -> Happiness
-  happinessFor arrangement idx = 
-    let name = idx `index` arrangement
-    in case name `lookupPrecise` cs.change_map of
-      Nothing => 0
-      Just changes => 
-        let name_right = (finS idx) `index` arrangement
-            change_right = 
-              fromMaybe 0 . map (.amount) . find ((== name_right) . (.other)) $ 
-                changes
-            name_left = (unfinS idx) `index` arrangement
-            change_left = 
-              fromMaybe 0 . map (.amount) . find ((== name_left) . (.other)) $ 
-                changes
-        in change_right + change_left
-```
-
-Calculate the overall happiness change for a given arrangement by mapping our
-`happinessFor` function over a list of all possible indexes to the `arrangement`
-vect, and summing the results.
-
-Notice how the `cs` parameter is implicitly passed to `happinessFor`, as we are
-inside the same `parameters` block as it.
-
-```idris
-  happinessChange :
-    (arrangement : Vect (length (keys cs.change_map)) Name)
-    -> Happiness
-  happinessChange arrangement = 
-    let idxes = List.allFins (length (keys cs.change_map))
-        changes = map (happinessFor arrangement) idxes
-    in sum changes
-```
-
-Find the arrangement with the maximum total change in happiness by mapping
-`happinessChange` over a list of all the possible permutations of our seed
-arrangement described by `names`, and using `maxBy` to identify the largest
-positive change in overall happiness.
-
-```idris
-  maxHappiness : Has (Except String) fs =>   
-    Eff fs (Happiness, Vect (length (keys cs.change_map)) Name)
-  maxHappiness =
-    let arrangements = permutations cs.names
-        changes = map happinessChange arrangements
-        pairs = zip changes arrangements
-    in case pairs of
-      [] => throw "No arrangements"
-      (x :: xs) => pure $ maxBy (compare `on` fst) x xs
-```
-
-## Part Functions
-
-### Part 1
-
-Parse our input and feed it into our `maxHappiness` function.
-
-Notice how, since we are outside the `parameters` block, we have to provide the
-`cs` argument to `maxHappiness` explicitly.
-
-```idris
-part1 : Eff (PartEff String) (Happiness, ())
-part1 = do
-  input <- map lines $ askAt "input"
-  changes <- parseChanges input empty
-  (max, arrangement) <- maxHappiness changes
-  pure (max, ())
-```
-
-### Part 2
-
-Our implementation already replaces missing relationships with 0, so we can
-cheese this by injecting ourself with an empty relationship list into the
-`change_map : SortedDMap Name (\n => (List n))`.
-
-The overall `Changes` data structure isn't easy to modify, and since our data
-set is quite small here, we'll just inject this into parsing and reparse our
-data.
-
-```idris
-part2 : () -> Eff (PartEff String) Happiness
-part2 x = do
-  input <- map lines $ askAt "input"
-  let seed = insert "ME!!!!" [] empty
-  changes <- parseChanges input seed
-  (max, arrangement) <- maxHappiness changes
-  pure max
-```
-
-```idris hide
-public export
-day13 : Day
-day13 = Both 13 part1 part2
-```
-
-## References
-
-[^1]: <https://idris2.readthedocs.io/en/latest/tutorial/modules.html#parameterised-blocks-parameters-blocks>
diff --git a/src/Years/Y2015/Day14.md b/src/Years/Y2015/Day14.md
deleted file mode 100644
index 5418617..0000000
--- a/src/Years/Y2015/Day14.md
+++ /dev/null
@@ -1,173 +0,0 @@
-# [Year 2015 Day 14](https://adventofcode.com/2015/day/14)
-
-This day provides us an introduction to streams, infinite, lazily generated,
-collections of data.
-
-```idris hide
-module Years.Y2015.Day14
-
-import Data.Primitives.Interpolation
-
-import Control.Eff
-
-import Runner
-```
-
-```idris
-import Data.String
-import Data.List1
-import Data.Vect
-import Data.Stream
-import Data.Zippable
-import Decidable.Equality
-
-import Util
-```
-
-## Parsing And Datastructures
-
-Collect the aspects defining a reindeer into a record
-
-```idris
-record Reindeer where
-  constructor MkReindeer
-  name : String
-  speed : Nat
-  duration, rest : Nat
-```
-
-```idris hide
-Show Reindeer where
-  show (MkReindeer name speed duration rest) = 
-    "MkReindeer \{name} \{speed} \{duration} \{rest}"
-```
-
-This time around, since the lines describing a reindeer contain a lot of cruft,
-we'll handle the parsing by converting the input, after splitting it on space
-characters, to a `Vect`, and indexing into that `Vect`.
-
-```idris
-parseReindeer : Has (Except String) fs =>
-  (input : String) -> Eff fs Reindeer
-parseReindeer input = do
-  parts <- note "Input has wrong size: \{input}" $
-    toVect 15 . forget . split (== ' ') . trim $ input
-  let name = index 0 parts
-  speed <- note "" $
-    parsePositive $ index 3 parts
-  duration <- note "" $
-    parsePositive $ index 6 parts
-  rest <- note "" $
-    parsePositive $ index 13 parts
-  pure $ MkReindeer name speed duration rest
-```
-
-### Solver Functions
-
-A stream is an infinite analog of a list, storing an infinite collection of
-(lazily generated) values.
-
-Streams are defined like:
-
-```idris
-data Stream' : Type -> Type where
-  (::) : a -> Inf (Stream' a) -> Stream' a
-```
-
-Streams are a member of a family of concepts analogous to iterators in
-imperative languages, the different flavors of colist.
-
-Colists are the codata duals of lists, we'll dig more into to this later, but to
-provide a high level summary, where data is defined by how it is constructed,
-codata is defined by how it is destructed. While a list is defined by how you
-can cons an element `x` onto a list `xs` to produce a new list `x :: xs`, a
-colist is defined by how you can break down a colist `x :: xs` into a head `x`
-and a tail `xs`.
-
-Streams are a particular type of colist that has no empty case, breaking down a
-`Stream` will always produce an element and another stream, resulting in streams
-always being infinite in length.
-
-Destructing a `Stream` by pattern matching is semantically equivalent to calling
-the `next` method on an iterator in a language like rust, it produces the
-element at the head of a stream, and a new stream producing future elements.
-
-We will model are reindeer's future history of locations as a stream, with each
-element being the position at the time given by the index into the stream,
-generating it with a pair of mutually recursive functions. The `run` function
-adds the speed to current position to produce the next one, and the `rest`
-function doesn't modify the position whill still consuming a time step.
-
-```idris
-distances : Reindeer -> Stream Nat
-distances x = run x x.duration 0
-  where
-    run : (deer : Reindeer) -> (left : Nat) -> (position : Nat) 
-     -> Stream Nat
-    rest : (deer : Reindeer) -> (left : Nat) -> (position : Nat) 
-     -> Stream Nat
-    run deer 0 position = rest deer deer.rest position
-    run deer (S k) position = position :: run deer k (position + deer.speed)
-    rest deer 0 position = run deer deer.duration position
-    rest deer (S k) position = position :: rest deer k position
-```
-
-Carry an accumulator containing the scores for each reindeer down the stream, at
-each position, granting one point to each reindeer at the leader position after
-the end of the second.
-
-```idris
-leaderScoring : {n : _} -> Vect (S n) (Stream Nat) -> Stream (Vect (S n) Nat)
-leaderScoring xs = leaderScoring' (replicate _ 0) xs
-  where
-    leaderScoring' : {n : _} -> (acc : Vect (S n) Nat) -> Vect (S n) (Stream Nat)
-      -> Stream (Vect (S n) Nat)
-    leaderScoring' acc xs = 
-      let positions = map (head . tail) xs
-          leader_pos = maxBy compare 0 positions
-          points : Vect _ Nat = 
-            map (\x => if x == leader_pos then 1 else 0) positions
-      in acc :: leaderScoring' (zipWith (+) acc points) (map tail xs)
-```
-
-## Part Functions
-
-### Part 1
-
-Parse the input, generate the position `Stream`s for each reindeer, then index
-the finish position in each stream.
-
-```idris
-part1 : Eff (PartEff String) (Nat, ())
-part1 = do
-  lines <- map lines $ askAt "input"
-  reindeer <- traverse parseReindeer lines
-  debug $ show reindeer
-  let dists = map distances reindeer
-  let dists_end = map (index 2503) dists
-  let max = maxBy compare 0 dists_end
-  pure (max, ())
-```
-
-Parse the input into a vect, and make sure it is not empty, then generate the
-stream with the `leaderScoring` function and index into it.
-
-```idris
-part2 : () -> Eff (PartEff String) Nat
-part2 x = do
-  lines <- map lines $ askAt "input"
-  let (len ** lines) = listToVect lines
-  case len of
-    0 => throw "No reindeer :("
-    (S k) => do
-    reindeer <- traverse parseReindeer lines
-    let dists = leaderScoring $ map distances reindeer
-    let dists_end = index 2503 dists
-    pure $ maxBy compare 0 dists_end
-```
-
-```idris hide
-public export
-day14 : Day 
-day14 = Both 14 part1 part2
-```