diff --git a/src/Main.idr b/src/Main.idr
deleted file mode 100644
index d47b9ae..0000000
--- a/src/Main.idr
+++ /dev/null
@@ -1,158 +0,0 @@
-module Main
-
-import System
-import System.Path
-import System.File
-import System.Directory
-import System.Console.GetOpt
-import Data.String
-import Data.Vect
-
-import Control.Eff
-import Derive.Prelude
-
-import Structures.Dependent.FreshList
-
-import Runner
-import Util
-import Util.Eff
-
-import Years.Y2015;
-
-%language ElabReflection
-%default total
-
-data Flag = UseExample | Verbose
-%runElab derive "Flag" [Eq, Show]
-
-advent : Advent
-advent = MkAdvent [
-    y2015
-  ]
-
-options : List (OptDescr Flag)
-options =
-  [
-    MkOpt ['u'] ["use-example"] (NoArg UseExample) "Use example input instead of main input"
-  , MkOpt ['v'] ["verbose"] (NoArg Verbose) "Enable logging to stderr"
-  ]
-
-header : String
-header = "Usage: advent YEAR DAY [OPTION...]"
-
-data Error : Type where
-  OptionsError : (errs : List String) -> Error
-  ArgumentsError : (count : Nat) -> Error
-  InvalidYear : (year : String) -> Error
-  InvalidDay : (year : Nat) -> (day : String) -> Error
-  NoSuchDay : (year : Nat) -> (day : Nat) -> Error
-  NoCurrentDir : Error
-  InputRead : (path : String) -> (err : FileError) -> Error
-  SolveError : Show e => (year, day, part : Nat) -> (err : e) -> Error
-%name Error err
-
-Show Error where
-  show (OptionsError errs) =
-    let errs = unlines . map ("  " ++) . lines . joinBy "\n" $ errs
-    in "Error parsing options:\n" ++ errs ++ "\n" ++ usageInfo header options
-  show (ArgumentsError count) =
-    "Error parsing arguments: Expected 2 positional arguments, got \{show count}. Provide only year and date.\n" ++
-    usageInfo header options
-  show (InvalidYear year) =
-    "Error parsing arguments: Unable to parse year argument: \{year}"
-  show (InvalidDay year day) =
-    "Error parsing arguments: Failed to parse day \{day} of year \{show year}"
-  show (NoSuchDay year day) =
-    "Error locating day: No such day \{show day} of year \{show year}"
-  show NoCurrentDir =
-    "Unknown error getting current working directory"
-  show (InputRead path err) =
-    let err = unlines . map ("  " ++) . lines . show $ err
-    in "Error reading input: Encountered error reading input at \{path}\n" ++ err
-  show (SolveError year day part err) =
-    let err = unlines . map ("  " ++) . lines . show $ err
-    in "Error solving day \{show day} part \{show part} of year \{show year}: \n" ++ err
-
-||| Convert the non-option arguments into a Year/Day pair
-argumentsToPair : Has (Except Error) fs =>
-  List String -> Eff fs (Nat, Nat)
-argumentsToPair [] = throw $ ArgumentsError 0
-argumentsToPair [x] = throw $ ArgumentsError 1
-argumentsToPair [year, day] = do
-  year <- note (InvalidYear year) $ parsePositive year
-  day <- note (InvalidDay year day) $ parsePositive day
-  pure (year, day)
-argumentsToPair xs = throw $ ArgumentsError (length xs)
-
-covering
-||| Actual main, as an effectful computation
-start : Eff [IO, Except Error] ()
-start = do
-  -- Read and parse arguments/options
-  args <- getArgs
-  let opts = getOpt Permute options (drop 1 args)
-  when (not . null $ opts.errors) $
-    throw (OptionsError opts.errors)
-  (year, day_n) <- argumentsToPair opts.nonOptions
-  -- If the verbose flag is set, hook up the logging writer to stderr
-  let verbose = any (== Verbose) opts.options
-  let logHandler : Eff [IO, Except Error, WriterL "log" String] () -> Eff [IO, Except Error] () =
-    if verbose
-       then handleLog ePutStrLn
-       else handleLog (\x => pure ())
-  -- Add the logging writer to the effect
-  logHandler $ do
-  -- Locate and read in the input file
-  Just cwd <- currentDir | _ => throw NoCurrentDir
-  let cwd = parse cwd
-  let use_example = any (== UseExample) opts.options
-  let base_dir = cwd /> "inputs" /> (if use_example then "examples" else "real");
-  let input_path = show $ base_dir /> (show year) /> (show day_n)
-  info "Reading input from \{input_path}"
-  Right contents <- readFile input_path | Left err => throw $ InputRead input_path err
-  -- Now add the reader that provides the input to the effect
-  runReaderAt "input" contents {fs = PartEff Error} $ do
-  -- Attempt to locate the provided day
-  Just day <- pure $ locate year day_n advent | _ => throw $ NoSuchDay year day_n
-  -- Run part 1
-  part_1 <- lift $ runExcept day.part1
-  (part_1, ctx) <- rethrow . mapLeft (SolveError year day_n 1 @{day.showErr1}) $ part_1
-  putStrLn "\{show year} day \{show day_n} part 1:"
-  putStrLn $ unlines . map ("  " ++) . lines . show @{day.showOut1} $ part_1
-  -- Run part 2 if we have it
-  case day.part2 of
-    Nothing => pure ()
-    Just part_2_f => do
-      part_2 <- lift . runExcept $ part_2_f ctx
-      part_2 <- rethrow . mapLeft (SolveError year day_n 2 @{day.showErr2}) $ part_2
-      putStrLn "\{show year} day \{show day_n} part 2:"
-      putStrLn $ unlines . map ("  " ++) . lines . show @{day.showOut2} $ part_2
-  where
-    -- print to standard error
-    ePutStrLn : String -> IO ()
-    ePutStrLn str = do
-      _ <- fPutStrLn stderr str
-      pure ()
-    -- Decompose a writer, eases type inference
-    unwriter : WriterL "log" String a -> (a, String)
-    unwriter (Tell vw) = ((), vw)
-    -- Lowers logging into IO within the effect using the given IO function
-    handleLog :
-      Has (WriterL "log" String) fs => Has IO (fs - WriterL "log" String) => 
-      (tell : String -> IO ()) -> Eff fs a -> Eff (fs - (WriterL "log" String)) a
-    handleLog tell x =
-      handle
-        (\msg, f =>
-            do let (val, msg) = unwriter msg
-               _ <- send $ tell msg
-               f val) x
-
-covering
-||| Shim main, which simply executes the effectful computation
-main : IO ()
-main = runEff start [id, handleError]
-  where
-  handleError : Except Error a -> IO a
-  handleError (Err err) = do
-    printLn err
-    exitFailure
diff --git a/src/Main.md b/src/Main.md
new file mode 100644
index 0000000..726b85e
--- /dev/null
+++ b/src/Main.md
@@ -0,0 +1,302 @@
+<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-refresh-toc -->
+**Table of Contents**
+
+- [Advent of Code](#advent-of-code)
+- [Command Line Interface](#command-line-interface)
+    - [Error Type](#error-type)
+    - [Extract the year and day](#extract-the-year-and-day)
+- [The Advent ](#the-advent)
+- [The Hard Part](#the-hard-part)
+    - [Parsing the arguments](#parsing-the-arguments)
+    - [Handling the arguments and finding the input](#handling-the-arguments-and-finding-the-input)
+    - [Executing the parts](#executing-the-parts)
+    - [Helper functions](#helper-functions)
+        - [Print strings to stderr](#print-strings-to-stderr)
+        - [Decompose a Writer](#decompose-a-writer)
+        - [Lower logging into the IO component of the effect](#lower-logging-into-the-io-component-of-the-effect)
+- [Handle the effectful action as an IO action ](#handle-the-effectful-action-as-an-io-action)
+
+<!-- markdown-toc end -->
+
+# Advent of Code
+
+This module provides a command line interface for running the solution to a specific day for a specific year, run as `advent $YEAR $DAY`. 
+
+This runner will automatically locate the appropriate input file and then run the selected day's solution against it. See [Runner](Runner.md) for the definitions of the `Day`, `Year`, and `Advent` data types.
+
+```idris
+module Main
+
+import System
+import System.Path
+import System.File
+import System.Directory
+import System.Console.GetOpt
+import Data.String
+import Data.Vect
+
+import Control.Eff
+import Derive.Prelude
+
+import Structures.Dependent.FreshList
+
+import Runner
+import Util
+import Util.Eff
+
+import Years.Y2015;
+
+%language ElabReflection
+%default total
+```
+
+# Command Line Interface
+
+Since this is a simple application, I am using `GetOpt` from `contrib` for argument parsing. Here we define our options list, a data type to describe our flags, and the usage message header.
+
+```idris
+data Flag = UseExample | Verbose
+%runElab derive "Flag" [Eq, Show]
+
+options : List (OptDescr Flag)
+options =
+  [
+    MkOpt ['u'] ["use-example"] (NoArg UseExample) "Use example input instead of main input"
+  , MkOpt ['v'] ["verbose"] (NoArg Verbose) "Enable logging to stderr"
+  ]
+
+header : String
+header = "Usage: advent YEAR DAY [OPTION...]"
+```
+
+## Error Type
+
+We will be using one unified error type for the entire `Main` module, but we must go ahead and define it before we go any further with command line arguments parsing, as we are about to do some things that might fail.
+
+```idris
+data Error : Type where
+  OptionsError : (errs : List String) -> Error
+  ArgumentsError : (count : Nat) -> Error
+  InvalidYear : (year : String) -> Error
+  InvalidDay : (year : Nat) -> (day : String) -> Error
+  NoSuchDay : (year : Nat) -> (day : Nat) -> Error
+  NoCurrentDir : Error
+  InputRead : (path : String) -> (err : FileError) -> Error
+  SolveError : Show e => (year, day, part : Nat) -> (err : e) -> Error
+%name Error err
+```
+
+A `Show` implementation for `Error` is provided, hidden in this document for brevity.
+
+
+<!-- idris
+Show Error where
+  show (OptionsError errs) =
+    let errs = unlines . map ("  " ++) . lines . joinBy "\n" $ errs
+    in "Error parsing options:\n" ++ errs ++ "\n" ++ usageInfo header options
+  show (ArgumentsError count) =
+    "Error parsing arguments: Expected 2 positional arguments, got \{show count}. Provide only year and date.\n" ++
+    usageInfo header options
+  show (InvalidYear year) =
+    "Error parsing arguments: Unable to parse year argument: \{year}"
+  show (InvalidDay year day) =
+    "Error parsing arguments: Failed to parse day \{day} of year \{show year}"
+  show (NoSuchDay year day) =
+    "Error locating day: No such day \{show day} of year \{show year}"
+  show NoCurrentDir =
+    "Unknown error getting current working directory"
+  show (InputRead path err) =
+    let err = unlines . map ("  " ++) . lines . show $ err
+    in "Error reading input: Encountered error reading input at \{path}\n" ++ err
+  show (SolveError year day part err) =
+    let err = unlines . map ("  " ++) . lines . show $ err
+    in "Error solving day \{show day} part \{show part} of year \{show year}: \n" ++ err
+-->
+
+## Extract the year and day
+
+After peeling off our options from the arguments using `GetOpt`, we will be left with a list of non-option arguments, which we must then parse into our year number/day number pair. We perform some pattern matching to make sure the list is the correct length, and then parse the individual integers, throwing an error if anything goes wrong
+
+```idris
+||| Convert the non-option arguments into a Year/Day pair
+argumentsToPair : Has (Except Error) fs =>
+  List String -> Eff fs (Nat, Nat)
+argumentsToPair [] = throw $ ArgumentsError 0
+argumentsToPair [x] = throw $ ArgumentsError 1
+argumentsToPair [year, day] = do
+  year <- note (InvalidYear year) $ parsePositive year
+  day <- note (InvalidDay year day) $ parsePositive day
+  pure (year, day)
+argumentsToPair xs = throw $ ArgumentsError (length xs)
+```
+
+# The Advent 
+
+Construct our top-level `Advent` record from the imported `Year` modules. The argument to the `MkAdvent` constructor is a `FreshList`, with a freshness criteria ensuring that the list is in ascending order and does not include any duplicate `Year`s.
+
+```idris
+advent : Advent
+advent = MkAdvent [
+    y2015
+  ]
+```
+
+# The Hard Part
+
+Now we must glue everything together, parse our arguments, handle any supplied options, locate the relevant year and day, locate the corresponding input file, read it, and then run the selected `Day` against it.
+
+Because we are building our application around effects, the actual core of the application is the effectful `start` computation, that the `main` function will then apply `IO` based handlers to.
+
+Our reader and writer aren't ready yet, we need to do some setup first, so the top level type signature doesn't include them, so we'll add them to the effects list as they become available.
+
+```idris
+covering
+||| Actual main, as an effectful computation
+start : Eff [IO, Except Error] ()
+start = do
+```
+
+## Parsing the arguments
+
+Feed the augments from `System.getArgs` into `getOpt`, making sure to drop the name the binary was invoked with, then check for any errors in the result, throwing our own error if any are encountered.
+
+```idris
+  -- Read and parse arguments/options
+  args <- getArgs
+  let opts = getOpt Permute options (drop 1 args)
+  when (not . null $ opts.errors) $
+    throw (OptionsError opts.errors)
+```
+
+Use our `argumentsToPair` function to extract the selected year and day numbers from the positional arguments, implicitly throwing an error if there are any failures doing so.
+
+```idris
+  (year, day_n) <- argumentsToPair opts.nonOptions
+```
+
+## Handling the arguments and finding the input
+
+Handle the verbosity flag, if it is set, hook our logger up to stderr, otherwise blackhole the logs. Afterwards, use `logHandler` to introduce the logging `Writer` into the effects list.
+
+```idris
+  -- If the verbose flag is set, hook up the logging writer to stderr
+  let verbose = any (== Verbose) opts.options
+  let logHandler : Eff [IO, Except Error, WriterL "log" String] () -> Eff [IO, Except Error] () =
+    if verbose
+       then handleLog ePutStrLn
+       else handleLog (\x => pure ())
+  -- Add the logging writer to the effect
+  logHandler $ do
+```
+
+Find the current directory and append to it to find the input file. If the `--use-example/-u` flag is set, look for the input file at `inputs/examples/$year/$day`, otherwise look for it at `inputs/real/$year/$day`.
+
+After we've located it, attempt to read from it, throwing an `InputRead` error if any errors occur, then insert the contents into our `Reader` and inject it into the effects list.
+
+```idris
+  -- Locate and read in the input file
+  Just cwd <- currentDir | _ => throw NoCurrentDir
+  let cwd = parse cwd
+  let use_example = any (== UseExample) opts.options
+  let base_dir = cwd /> "inputs" /> (if use_example then "examples" else "real");
+  let input_path = show $ base_dir /> (show year) /> (show day_n)
+  info "Reading input from \{input_path}"
+  Right contents <- readFile input_path | Left err => throw $ InputRead input_path err
+  -- Now add the reader that provides the input to the effect
+  runReaderAt "input" contents {fs = PartEff Error} $ do
+```
+
+Try and locate the `Day` in our `Advent` record, throwing an error if we are unable to locate it
+
+```idris
+  -- Attempt to locate the provided day
+  Just day <- pure $ locate year day_n advent | _ => throw $ NoSuchDay year day_n
+```
+
+## Executing the parts
+
+Run the selected `Day`'s part 1, wrapping any errors that it returns in a `SolveError`. Collect both the result and the opaque context value, then print out the result.
+
+```idris
+  -- Run part 1
+  part_1 <- lift $ runExcept day.part1
+  (part_1, ctx) <- rethrow . mapLeft (SolveError year day_n 1 @{day.showErr1}) $ part_1
+  putStrLn "\{show year} day \{show day_n} part 1:"
+  putStrLn $ unlines . map ("  " ++) . lines . show @{day.showOut1} $ part_1
+```
+
+Check and see if the selected `Day` has a part 2, if it does, feed the opaque context value collected from part 1 into it, wrap any errors that it returns in a `SolveError`, then print out the result, then return, closing out the program.
+
+```idris
+  -- Run part 2 if we have it
+  case day.part2 of
+    Nothing => pure ()
+    Just part_2_f => do
+      part_2 <- lift . runExcept $ part_2_f ctx
+      part_2 <- rethrow . mapLeft (SolveError year day_n 2 @{day.showErr2}) $ part_2
+      putStrLn "\{show year} day \{show day_n} part 2:"
+      putStrLn $ unlines . map ("  " ++) . lines . show @{day.showOut2} $ part_2
+```
+
+## Helper functions
+
+```idris
+  where
+```
+
+### Print strings to stderr
+
+Putting this in its own function makes dealing with the potential error returned by `fPutStrLn` a bit eaiser. It's reasonable to ignore this error, since if we can't write to stderr we are kinda powerless to tell anyone about it.
+
+```idris
+    -- print to standard error
+    ePutStrLn : String -> IO ()
+    ePutStrLn str = do
+      _ <- fPutStrLn stderr str
+      pure ()
+```
+
+### Decompose a Writer
+
+Having this be a function keeps the `a` somewhat opaque and helps with they type checking. Only values of `Writer $TYPE ()` can actually be constructed, but the type checker gets a little bit confused about this when you try to do this by pattern matching inline.
+
+```idris
+    -- Decompose a writer, eases type inference
+    unwriter : WriterL "log" String a -> (a, String)
+    unwriter (Tell vw) = ((), vw)
+```
+
+### Lower logging into the IO component of the effect
+
+This function uses the provided `String -> IO ()` to remove the `Writer` from the effects list by translating `tell` calls to IO actions within the effect. 
+
+```idris
+    -- Lowers logging into IO within the effect using the given IO function
+    handleLog :
+      Has (WriterL "log" String) fs => Has IO (fs - WriterL "log" String) => 
+      (tell : String -> IO ()) -> Eff fs a -> Eff (fs - (WriterL "log" String)) a
+    handleLog tell x =
+      handle
+        (\msg, f =>
+            do let (val, msg) = unwriter msg
+               _ <- send $ tell msg
+               f val) x
+```
+
+# Handle the effectful action as an IO action 
+
+Use `runEff` to translate the effects in `start`'s effects list into IO actions, and return the resulting `IO ()`.
+
+The `IO` component of the effects list is handled via `id`, translating `IO` actions into themselves, and we construct a helper function to handle errors as IO actions by printing the error and crashing the program.
+
+```idris
+covering
+||| Shim main, which simply executes the effectful computation
+main : IO ()
+main = runEff start [id, handleError]
+  where
+  handleError : Except Error a -> IO a
+  handleError (Err err) = do
+    printLn err
+    exitFailure
+```
diff --git a/src/Runner.idr b/src/Runner.idr
deleted file mode 100644
index c6a2712..0000000
--- a/src/Runner.idr
+++ /dev/null
@@ -1,88 +0,0 @@
-module Runner
-
-import Control.Eff
-import Structures.Dependent.FreshList
-
-||| The effect type is the same in boths parts one and two, modulo potentially
-||| different error types, so we calucate it here
-public export
-PartEff : (err : Type) -> List (Type -> Type)
-PartEff err =
-  [IO, Except err, WriterL "log" String, ReaderL "input" String]
-
-||| Model solving a single day
-public export
-record Day where
-  constructor MkDay
-  day : Nat
-  {0 out1, out2, err1, err2 : Type}
-  {auto showOut1 : Show out1}
-  {auto showOut2 : Show out2}
-  {auto showErr1 : Show err1}
-  {auto showErr2 : Show err2}
-  part1 : Eff (PartEff err1) (out1, ctx)
-  part2 : Maybe (ctx -> Eff (PartEff err2) out2)
-%name Day day, day2, day3
-
-namespace Day
-  ||| Constructor for a day with only part one ready to run
-  public export
-  First : Show err => Show out =>
-    (day : Nat) -> (part1 : Eff (PartEff err) (out, ctx'))
-    -> Day
-  First day part1 =
-    MkDay day part1 Nothing {out2 = ()} {err2 = ()}
-
-  ||| Constructor for a day with both parts ready to run
-  public export
-  Both : Show o1 => Show o2 => Show e1 => Show e2 =>
-    (day : Nat) -> (part1 : Eff (PartEff e1) (o1, ctx')) ->
-    (part2 :ctx' -> Eff (PartEff e2) o2)
-    -> Day
-  Both day part1 part2 =
-    MkDay day part1 (Just part2)
-
-||| Freshness criteria for days
-|||
-||| A day is fresh compared to another if the day number of the former day is
-||| strictly less than the day number of the latter day
-|||
-||| This ensures that the days list is always in incrimenting sorted order
-||| (since we are consing to the front of the list) with no duplicate days
-public export
-FreshDay : Day -> Day -> Bool
-FreshDay x y = x.day < y.day
-
-||| Collect all the days in a given year
-public export
-record Year where
-  constructor MkYear
-  year : Nat
-  days : FreshList FreshDay Day
-%name Year year, year2, year3
-
-||| Freshness criteria for years
-|||
-||| A year is fresh compared to another if the year number of the former year is
-||| strictly less than the year number of the latter year
-|||
-||| This ensures that the years list is always in incrimenting sorted order
-||| (since we are consing to the front of the list) with no duplicate years
-public export
-FreshYear : Year -> Year -> Bool
-FreshYear x y = x.year < y.year
-
-||| Collect all years
-public export
-record Advent where
-  constructor MkAdvent
-  years : FreshList FreshYear Year
-%name Advent advent, advent2, advent3
-
-namespace Advent
-  ||| Attempt to locate `Day` entry corresponding to the provided day and year numbers
-  export
-  locate : (year, day : Nat) -> Advent -> Maybe Day
-  locate year day advent = do
-    year <- find (\x => x.year == year) advent.years
-    find (\x => x.day == day) year.days
diff --git a/src/Runner.md b/src/Runner.md
new file mode 100644
index 0000000..01a85c3
--- /dev/null
+++ b/src/Runner.md
@@ -0,0 +1,192 @@
+<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-refresh-toc -->
+**Table of Contents**
+
+- [Unified interface for any day from any year](#unified-interface-for-any-day-from-any-year)
+- [Effectful Parts](#effectful-parts)
+- [The `Day` Record](#the-day-record)
+    - [Smarter Constructors](#smarter-constructors)
+        - [First](#first)
+        - [Both](#both)
+    - [Freshness](#freshness)
+- [The `Year` Record](#the-year-record)
+    - [Freshness](#freshness-1)
+- [The `Advent` Record](#the-advent-record)
+    - [Methods](#methods)
+        - [locate](#locate)
+
+<!-- markdown-toc end -->
+
+# Unified interface for any day from any year
+
+This module provides some basic data types for building an application containing all my solutions to all of the parts of all the days across all of the years.
+
+This provides a defensively built API for constructing the overall `Advent` data structure that prevents registering a day/year twice or registering days/years out of order. 
+
+```idris
+module Runner
+
+import Control.Eff
+import Structures.Dependent.FreshList
+
+%default total
+```
+
+# Effectful Parts
+
+The solution to each part of a day is run as an effectful computation, and as the available effects are meant to be the same across both parts, only varying in the type of the error value in the `Except` effect, I construct a type level function to have a single source of truth for this. The `err` type can be any type with a `Show` implementation, but that constraint will be tacked on in the next step.
+
+A `Writer` effect is provided for logging, and a `Reader` effect is provided to pass in the input, just to make the top level API a little bit cleaner. `IO` is also provided, even though the part solutions themselves shouldn't really be doing any IO, this may come in handy if a part needs `IO` for performance reasons.
+
+```idris
+||| The effect type is the same in boths parts one and two, modulo potentially
+||| different error types, so we calucate it here
+public export
+PartEff : (err : Type) -> List (Type -> Type)
+PartEff err =
+  [IO, Except err, WriterL "log" String, ReaderL "input" String]
+```
+
+# The `Day` Record
+
+The `Day` type groups together an effectful `part1` computation, an optional effectful `part2` computation, the day number, and does some type wrangling to get the type system out of our way on this one.
+
+`part1` and `part2` are allowed independent output and error types, and this record captures `Show` implementations for those output and error types so that we can display them in `Main` where the `Day` is consumed without having to actually know what the types are.
+
+It is often useful to pass a bit of context, such as the data structures resulting from parsing, between `part1` and `part2`, and this is achieved by the erased `ctx` type, which is totally opaque here. The runner code in `Main` will provide the value of the `ctx` type produced as part of the output of `part1` as the input of `part2`.
+
+```idris
+||| Model solving a single day
+public export
+record Day where
+  constructor MkDay
+  day : Nat
+  {0 out1, out2, err1, err2 : Type}
+  {auto showOut1 : Show out1}
+  {auto showOut2 : Show out2}
+  {auto showErr1 : Show err1}
+  {auto showErr2 : Show err2}
+  part1 : Eff (PartEff err1) (out1, ctx)
+  part2 : Maybe (ctx -> Eff (PartEff err2) out2)
+%name Day day, day2, day3
+```
+
+## Smarter Constructors
+
+The default `MkDay` constructor is slightly cumbersome to use, always requiring _something_ for the `part2` slot, even if there isn't a part 2 yet, and requiring that `part2` be wrapped in a `Just` when there is one, so we provide a pair of constructors for the case where there is only a `part1` and for where there is a `part1` and a `part2` that handle that for us.
+
+```idris
+namespace Day
+```
+
+### First
+
+The `First` constructor only accepts a `part1`, it does the work of filling in `part2` with `Nothing` and setting all of `part2`'s type arguments to `()` for us.'
+
+```idris
+  ||| Constructor for a day with only part one ready to run
+  public export
+  First : Show err => Show out =>
+    (day : Nat) -> (part1 : Eff (PartEff err) (out, ctx'))
+    -> Day
+  First day part1 =
+    MkDay day part1 Nothing {out2 = ()} {err2 = ()}
+```
+
+### Both
+
+The `Both` constructor does a little bit less heavy lifting, the only thing it needs to do for us is wrap `part2` in a `Just`.
+
+```idris
+  ||| Constructor for a day with both parts ready to run
+  public export
+  Both : Show o1 => Show o2 => Show e1 => Show e2 =>
+    (day : Nat) -> (part1 : Eff (PartEff e1) (o1, ctx')) ->
+    (part2 :ctx' -> Eff (PartEff e2) o2)
+    -> Day
+  Both day part1 part2 =
+    MkDay day part1 (Just part2)
+```
+
+## Freshness
+
+We will be using a _Fresh List_ from the [structures](https://git.sr.ht/~thatonelutenist/Structures) package to build defensiveness into the API. A Fresh List structurally only allows you to prepend an element onto it when it satisfies some _freshness_ criteria relative to the elements already in the list.
+
+Here, we compare the day numbers of the two `Day`s using the less-than relationship. Since we are operating on the start of the list when this comparison takes place, this enforces, through type checking, that the resulting Fresh List is sorted in ascending order and that no two `Day`s have the same day number.
+
+```idris
+||| Freshness criteria for days
+|||
+||| A day is fresh compared to another if the day number of the former day is
+||| strictly less than the day number of the latter day
+|||
+||| This ensures that the days list is always in incrimenting sorted order
+||| (since we are consing to the front of the list) with no duplicate days
+public export
+FreshDay : Day -> Day -> Bool
+FreshDay x y = x.day < y.day
+```
+
+# The `Year` Record
+
+The `Year` record collects a number of `Day`s into a single Fresh List for the year, and is mostly just a simple container.
+
+```idris
+||| Collect all the days in a given year
+public export
+record Year where
+  constructor MkYear
+  year : Nat
+  days : FreshList FreshDay Day
+%name Year year, year2, year3
+```
+
+## Freshness
+
+Much like `Day`s are stored in a `FreshList` in `Year`, `Year`s will be stored in a `FreshList` in `Advent`, so we need to provide a freshness criteria for `Year` as well. We do so by applying the less-than relationship against the year number of the two `Years`, for the same reasons and with the same results as with `FreshDay`.
+
+```idris
+||| Freshness criteria for years
+|||
+||| A year is fresh compared to another if the year number of the former year is
+||| strictly less than the year number of the latter year
+|||
+||| This ensures that the years list is always in incrimenting sorted order
+||| (since we are consing to the front of the list) with no duplicate years
+public export
+FreshYear : Year -> Year -> Bool
+FreshYear x y = x.year < y.year
+```
+
+# The `Advent` Record
+
+The `Advent` record collects a number of `Year`s in much the same way that `Year` collects a number of days, sorting the `Year`s in a `FreshList` to provide API defensiveness.
+
+```idris
+||| Collect all years
+public export
+record Advent where
+  constructor MkAdvent
+  years : FreshList FreshYear Year
+%name Advent advent, advent2, advent3
+```
+
+## Methods
+
+```idris
+namespace Advent
+```
+
+### locate
+
+This is a utility function that searches the `FreshList` of `Year`s for the provided year number, then searches the resulting `Year`, if one exists, for the provided day number.
+
+We don't have to worry about potentially encountering duplicates here because of the freshness restriction. 
+
+```idris
+  ||| Attempt to locate `Day` entry corresponding to the provided day and year numbers
+  export
+  locate : (year, day : Nat) -> Advent -> Maybe Day
+  locate year day advent = do
+    year <- find (\x => x.year == year) advent.years
+    find (\x => x.day == day) year.days
+```
diff --git a/src/Util.idr b/src/Util.idr
deleted file mode 100644
index c67738a..0000000
--- a/src/Util.idr
+++ /dev/null
@@ -1,10 +0,0 @@
-module Util
-
------------------------------------
--- Standard Data Type Extensions --
------------------------------------
-namespace Either
-  export
-  mapLeft : (f : a -> b) -> Either a c -> Either b c
-  mapLeft f (Left x) = Left (f x)
-  mapLeft f (Right x) = Right x
diff --git a/src/Util.md b/src/Util.md
new file mode 100644
index 0000000..5e4db45
--- /dev/null
+++ b/src/Util.md
@@ -0,0 +1,24 @@
+# Utility functions
+
+This module contains functions that extend the functionality of standard data types, other types of utility functionality get their own module
+
+```idris
+module Util
+```
+
+## Either
+
+<!-- idris
+namespace Either
+-->
+
+### mapLeft
+
+Applies a function to the contents of a `Left` if the value of the given `Either` is actually a `Left`, otherwise, leaves `Right`s untouched.
+
+```idris
+  export
+  mapLeft : (f : a -> b) -> Either a c -> Either b c
+  mapLeft f (Left x) = Left (f x)
+  mapLeft f (Right x) = Right x
+```
diff --git a/src/Util/Eff.idr b/src/Util/Eff.md
similarity index 61%
rename from src/Util/Eff.idr
rename to src/Util/Eff.md
index 874af6f..4c6975c 100644
--- a/src/Util/Eff.idr
+++ b/src/Util/Eff.md
@@ -1,12 +1,24 @@
+# Effects utilities
+
+Contains utility functions extending the functionality of the `eff` package.
+
+```idris
 module Util.Eff
 
 import Control.Eff
 import Text.ANSI
 
------------------------
--- Logging Utilities --
------------------------
+%default total
+```
+
+## Logging
+
+Use the `WriterL "log" String` effect like a logging library. We'll provide a few "log levels" as verbs for the effect, but no filtering is done, when logging is enabled, all logs are always displayed, however the log level is indicated with a colored tag. 
+
+<!-- idris
 namespace Logging
+-->
+```idris
   export
   info : Has (WriterL "log" String) fs => String -> Eff fs ()
   info str =
@@ -24,3 +36,4 @@ namespace Logging
   warn str =
     let tag = show . bolden . show . colored Yellow $ "[WARN]"
     in tellAt "log" (tag ++ ": " ++ str ++ "\n")
+```
diff --git a/src/Years/Y2015.idr b/src/Years/Y2015.md
similarity index 63%
rename from src/Years/Y2015.idr
rename to src/Years/Y2015.md
index d534291..775cf7f 100644
--- a/src/Years/Y2015.idr
+++ b/src/Years/Y2015.md
@@ -1,3 +1,4 @@
+```idris
 module Years.Y2015
 
 import Structures.Dependent.FreshList
@@ -6,10 +7,25 @@ import Runner
 
 import Years.Y2015.Day1
 import Years.Y2015.Day2
+```
 
+# Days
+
+```idris
 export
 y2015 : Year
 y2015 = MkYear 2015 [
+```
+
+## [Day 1](./Day1.md)
+
+```idris
     day1
+```
+
+## [Day 2](./Day2.md)
+
+```idris
   , day2
   ]
+```
diff --git a/src/Years/Y2015/Day1.idr b/src/Years/Y2015/Day1.md
similarity index 50%
rename from src/Years/Y2015/Day1.idr
rename to src/Years/Y2015/Day1.md
index 405072d..352f7cd 100644
--- a/src/Years/Y2015/Day1.idr
+++ b/src/Years/Y2015/Day1.md
@@ -1,3 +1,8 @@
+# Day 1
+
+Pretty simple, basic warmup problem, nothing really novel is on display here except the effectful part computations.
+
+<!-- idris
 module Years.Y2015.Day1
 
 import Control.Eff
@@ -5,13 +10,25 @@ import Control.Eff
 import Runner
 
 %default total
+-->
 
+## Solver Functions
+
+This one implements the entirety of the logic for part 1, in a simple tail recursive manner, pattern matching on each character in the input string.
+
+We include a case for a non-paren character for totality's sake, but since we kinda trust the input here we just don't do anything in that branch.
+
+```idris
 trackFloor : (start : Integer) -> (xs : List Char) -> Integer
 trackFloor start [] = start
 trackFloor start ('(' :: xs) = trackFloor (start + 1) xs
 trackFloor start (')' :: xs) = trackFloor (start - 1) xs
 trackFloor start (x :: xs) = trackFloor start xs
+```
 
+This one is slightly more complicated, ultimately very similar to the above, but with two accumulators, one for the position in the input string in addition to the one for the current floor.
+
+```idris
 findBasement : (position : Nat) -> (currentFloor : Integer) -> (xs : List Char)
   -> Nat
 findBasement position currentFloor [] = position
@@ -23,18 +40,37 @@ findBasement position currentFloor (')' :: xs) =
     else findBasement (position + 1) (currentFloor - 1) xs
 findBasement position currentFloor (x :: xs) =
   findBasement (position + 1) currentFloor xs
+```
 
+## Part Functions
+
+Both this parts are simple application of one of our solver functions
+
+### Part 1
+
+Very uneventful, the only thing novel here is pulling the input out of the `ReaderL "input" String`, which will become very boring very quickly.
+
+```idris
 part1 : Eff (PartEff String) (Integer, ())
 part1 = do
   input <- map unpack $ askAt "input"
   let output = trackFloor 0 input
   pure (output, ())
+```
 
+### Part 2
+
+We have to be careful to start the position accumulator at 1, since the problem specifies that the input string is 1-index.
+
+```idris
 part2 : () -> Eff (PartEff String) Nat
 part2 x = do
   input <- map unpack $ askAt "input"
   pure $ findBasement 1 0 input
+```
 
+<!-- idris
 public export
 day1 : Day
 day1 = Both 1 part1 part2
+-->
diff --git a/src/Years/Y2015/Day2.idr b/src/Years/Y2015/Day2.idr
deleted file mode 100644
index 77409c6..0000000
--- a/src/Years/Y2015/Day2.idr
+++ /dev/null
@@ -1,60 +0,0 @@
-module Years.Y2015.Day2
-
-import Data.List
-import Data.List1
-import Data.String
-
-import Control.Eff
-
-import Runner
-
-%default total
-
-record Box where
-  constructor MkBox
-  length, width, height : Integer
-
-(.area) : Box -> Integer
-(.area) (MkBox length width height) =
-  2 * length * width + 2 * width * height + 2 * length * height
-
-(.slack) : Box -> Integer
-(.slack) (MkBox length width height) =
-  foldl1 min [length * width, width * height, length * height]
-
-(.ribbon) : Box -> Integer
-(.ribbon) (MkBox length width height) =
-  foldl1 min [2 * (length + width), 2 * (length + height), 2 * (width + height)]
-
-(.bow) : Box -> Integer
-(.bow) (MkBox length width height) = length * width * height
-
-totalRibbon : Box -> Integer
-totalRibbon x = x.ribbon + x.bow
-
-paperNeeded : Box -> Integer
-paperNeeded x = x.area + x.slack
-
-parseBox : Has (Except String) fs =>
-  String -> Eff fs Box
-parseBox str = do
-  l ::: [w, h] <- pure $ split (== 'x') str
-    | xs => throw "Box did not have exactly 3 components: \{show xs}"
-  length <- note "Failed parsing length: \{show l}" $ parsePositive l
-  width <- note "Failed parsing width: \{show w}" $ parsePositive w
-  height <- note "Failed parsing height: \{show h}" $ parsePositive h
-  pure $ MkBox length width height
-
-part1 : Eff (PartEff String) (Integer, List Box)
-part1 = do
-  input <- map lines $ askAt "input"
-  boxes <- traverse parseBox input
-  let output = sum . map paperNeeded $ boxes
-  pure (output, boxes)
-
-part2 : (boxes : List Box) -> Eff (PartEff String) Integer
-part2 boxes = pure . sum . map totalRibbon $ boxes
-
-public export
-day2 : Day
-day2 = Both 2 part1 part2
diff --git a/src/Years/Y2015/Day2.md b/src/Years/Y2015/Day2.md
new file mode 100644
index 0000000..733f351
--- /dev/null
+++ b/src/Years/Y2015/Day2.md
@@ -0,0 +1,126 @@
+# Day 2
+
+This day provides us our first little taste of effectful parsing
+
+<!-- idris
+module Years.Y2015.Day2
+
+import Control.Eff
+
+import Runner
+-->
+
+```idris
+import Data.List
+import Data.List1
+import Data.String
+```
+
+<!-- idris 
+%default total
+-->
+
+## Box structure
+
+A record to hold the parameters of a box and methods to operate on it
+
+```idris
+record Box where
+  constructor MkBox
+  length, width, height : Integer
+```
+
+### Box methods
+
+`.area` provides the surface area of the box, `.slack` provides the surface area of the smallest face, `.ribbon` provides the smallest perimeter of a face, and `.bow` provides the volume of the box.
+
+Names are as described in the problem
+
+```idris
+(.area) : Box -> Integer
+(.area) (MkBox length width height) =
+  2 * length * width + 2 * width * height + 2 * length * height
+
+(.slack) : Box -> Integer
+(.slack) (MkBox length width height) =
+  foldl1 min [length * width, width * height, length * height]
+
+(.ribbon) : Box -> Integer
+(.ribbon) (MkBox length width height) =
+  foldl1 min [2 * (length + width), 2 * (length + height), 2 * (width + height)]
+
+(.bow) : Box -> Integer
+(.bow) (MkBox length width height) = length * width * height
+```
+
+Provide the total amount of ribbon needed, by adding the ribbon (smallest perimeter) and the bow (volume) values together.
+
+```idris
+totalRibbon : Box -> Integer
+totalRibbon x = x.ribbon + x.bow
+```
+
+Provide the total amount of paper needed by adding the surface area and the slack (smallest side surface area) together.
+
+```idris
+paperNeeded : Box -> Integer
+paperNeeded x = x.area + x.slack
+```
+
+### Box parsing
+
+Parse a box from an input string of form `lengthxwidthxheight`.
+
+```idris
+parseBox : Has (Except String) fs =>
+  String -> Eff fs Box
+parseBox str = do
+```
+
+First, we split the string into 3 parts by pattern matching on the result of `split`, using `pure` to lift the computation into the effect, and throwing an error if the pattern match fails.
+
+```idris
+  l ::: [w, h] <- pure $ split (== 'x') str
+    | xs => throw "Box did not have exactly 3 components: \{show xs}"
+```
+
+Then try to parse each of the three integers, throwing an error if parsing fails, then construct and return our box.
+
+```idris
+  length <- note "Failed parsing length: \{show l}" $ parsePositive l
+  width <- note "Failed parsing width: \{show w}" $ parsePositive w
+  height <- note "Failed parsing height: \{show h}" $ parsePositive h
+  pure $ MkBox length width height
+```
+
+## Part Functions
+
+### Part 1
+
+Split the input into lines, effectfully traverse our box parser over the resulting list of lines, then sum the amounts of paper needed for each box.
+
+We return the list of parsed boxes as the context here to avoid needing to parse again in part 2
+
+```idris
+part1 : Eff (PartEff String) (Integer, List Box)
+part1 = do
+  input <- map lines $ askAt "input"
+  boxes <- traverse parseBox input
+  let output = sum . map paperNeeded $ boxes
+  pure (output, boxes)
+```
+
+### Part 2
+
+Much the same as part 1, except with the amount of ribbon needed instead of the amount of paper, and without the parsing, since we received the already parsed list of boxes from part 1 as our context value.
+
+```idris
+part2 : (boxes : List Box) -> Eff (PartEff String) Integer
+part2 boxes = pure . sum . map totalRibbon $ boxes
+```
+
+<!-- idris
+public export
+day2 : Day
+day2 = Both 2 part1 part2
+-->