diff --git a/aoc2023.cabal b/aoc2023.cabal
new file mode 100644
index 0000000..e92f60a
--- /dev/null
+++ b/aoc2023.cabal
@@ -0,0 +1,16 @@
+cabal-version:      3.0
+name:               aoc2023
+version:            0.1.0.0
+build-type:         Simple
+
+executable day14
+    ghc-options:      -Wall -O2
+    main-is:          day14.hs
+    -- other-modules:
+    -- other-extensions:
+    build-depends:
+      base       ^>= 4.17.2.0,
+      containers ^>= 0.6.7,
+      array      ^>= 0.5.4.0
+    hs-source-dirs:   .
+    default-language: GHC2021
diff --git a/day14.hs b/day14.hs
index eab94da..3e3f5ae 100644
--- a/day14.hs
+++ b/day14.hs
@@ -1,13 +1,47 @@
 {-# options_ghc -Wall #-}
-{-# language BlockArguments #-}
+{-# language BlockArguments, LambdaCase #-}
 import Data.List
 import System.Environment
 import qualified Data.Map as M
 import Data.Maybe
+import qualified Data.Array as A
 
 
 data Block = Rock | Space | Wall deriving (Eq, Ord, Show)
 
+
+data Rotation = U | L | D | R deriving (Eq, Ord, Show, Bounded, Enum)
+
+left, right, opp :: Rotation -> Rotation
+left  = \case U -> L; L -> D; D -> R; R -> U
+right = \case U -> R; R -> D; D -> L; L -> U
+opp   = \case U -> D; D -> U; L -> R; R -> L
+
+instance Semigroup Rotation where
+  U <> r = r
+  L <> r = left r
+  R <> r = right r
+  D <> r = opp r
+
+instance Monoid Rotation where mempty = U
+
+type I2 = (Int, Int)
+
+data RArray e = RA !Rotation !(A.Array I2 e)
+
+rotateI :: Rotation -> (I2, I2) -> I2 -> I2
+rotateI U _                        i      = i
+rotateI L (_, (xhi, _))   (x, y) = (y, xhi - x - 1)
+rotateI D (_, (xhi, yhi)) (x, y) = (xhi - x - 1, yhi - y - 1)
+rotateI R (_, (_,   yhi)) (x, y) = (yhi - y - 1, x)
+
+(!) :: RArray e -> I2 -> e
+RA r arr ! i = arr A.! rotateI r (A.bounds arr) i
+
+rotate :: Rotation -> RArray e -> RArray e
+rotate r1 (RA r2 arr) = RA (r1 <> r2) arr
+
+
 block :: Char -> Maybe Block
 block 'O' = Just Rock
 block '.' = Just Space
@@ -100,15 +134,15 @@ main = do
     "2" -> print $ part2 ℓs
     _   -> error "usage: $0 <part> <file>"
 
-example1 :: [String]
-example1 =
-  ["O....#....",
-   "O.OO#....#",
-   ".....##...",
-   "OO.#O....O",
-   ".O.....O#.",
-   "O.#..O.#.#",
-   "..O..#O..O",
-   ".......O..",
-   "#....###..",
-   "#OO..#...."]
+-- example1 :: [String]
+-- example1 =
+--   ["O....#....",
+--    "O.OO#....#",
+--    ".....##...",
+--    "OO.#O....O",
+--    ".O.....O#.",
+--    "O.#..O.#.#",
+--    "..O..#O..O",
+--    ".......O..",
+--    "#....###..",
+--    "#OO..#...."]
diff --git a/day15.quox b/day15.quox
new file mode 100644
index 0000000..53be585
--- /dev/null
+++ b/day15.quox
@@ -0,0 +1,27 @@
+load "bool.quox"
+load "nat.quox"
+load "string.quox"
+load "list.quox"
+load "io.quox"
+
+
+def hash : ω.String → ℕ =
+  letω hash1 : ω.ℕ → ω.Char → ℕ =
+    λ n c ⇒ case char.ws? c return ℕ of {
+      'true  ⇒ n;
+      'false ⇒ nat.mod (nat.times 17 (nat.plus (char.to-ℕ c) n)) 256
+    } in
+  string.foldlω ℕ 0 hash1
+
+def split : ω.String → List String =
+  letω comma = char.from-ℕ 0x2C in
+  string.split (char.eq comma)
+
+#[main]
+def part1 =
+  io.bindω String True
+    (io.read-fileω "in/day15")
+    (λ s ⇒ io.dump ℕ (list.sum (list.mapω String ℕ hash (split s))))
+
+
+def0 ShittyHashMap = Vec 8 (Vec 8 (Vec 8 (List (String × ℕ))))
diff --git a/day19.pl b/day19.pl
new file mode 100644
index 0000000..7d14e49
--- /dev/null
+++ b/day19.pl
@@ -0,0 +1,84 @@
+:- use_module(library(dcg/basics)).
+:- use_module(library(dcg/high_order)).
+
+file(W, I) --> sequence(workflow, W), blanks, sequence(item, I).
+
+workflow(w(L,I)) --> name(L), "{", sequence(instruction, ",", I), "}", blanks.
+name(N) --> sequence(alpha_to_lower, Cs), {Cs \= [], atom_codes(N, Cs)}.
+
+instruction(accept) --> "A", !.
+instruction(reject) --> "R", !.
+instruction(goto(X)) --> name(X).
+instruction(if(A, R, N, T)) -->
+  attr(A), relation(R), number(N), ":", instruction(T).
+  % e.g. if(x, >, 420, goto(label)) or if(x, >, 420, accept)
+
+attr(A)     --> oneof([x,m,a,s], A).
+relation(R) --> oneof([<,>], R).
+
+oneof(Xs, X) --> {member(X, Xs)}, atom(X).
+
+item(i(X, M, A, S)) -->
+  "{", field(x, X), ",", field(m, M), ",", field(a, A), ",", field(s, S), "}",
+  blanks.
+field(L, X) --> atom(L), "=", number(X).
+
+
+field(i(X,_,_,_), x, X).
+field(i(_,M,_,_), m, M).
+field(i(_,_,A,_), a, A).
+field(i(_,_,_,S), s, S).
+
+goto([w(L, W)|_],  L, W) :- !.
+goto([_      |Ws], L, W) :- goto(Ws, L, W).
+
+run(_,  [accept|_],  _, accept) :- !.
+run(_,  [reject|_],  _, reject) :- !.
+run(Ws, [goto(L)|_], I, Res) :-
+  goto(Ws, L, W),
+  run(Ws, W, I, Res).
+run(Ws, [if(F, R, N, T)|W], I, Res) :-
+  field(I, F, Val),
+  compare(R0, Val, N),
+  (R = R0 -> run(Ws, [T|W], I, Res) ; run(Ws, W, I, Res)).
+
+score(_,          reject, 0).
+score(i(X,M,A,S), accept, T) :- T is X + M + A + S.
+total(Is, Rs, T) :- maplist(score, Is, Rs, Ts), foldl(plus, Ts, 0, T).
+
+part1(File) :-
+  once(phrase_from_file(file(Ws, Is), File)),
+  maplist(run(Ws, [goto(in)]), Is, Rs),
+  total(Is, Rs, T),
+  writeln(T), !.
+
+
+:- use_module(library(clpfd)).
+
+run2(Ws, [goto(L)|_],        I) :- goto(Ws, L, W),  run2(Ws, W, I).
+run2(Ws, [if(F, R, N, T)|_], I) :- yes(F, R, N, I), run2(Ws, [T], I).
+run2(Ws, [if(F, R, N, _)|W], I) :- no(F, R, N, I),  run2(Ws, W,   I).
+run2(_,  [accept|_],         i(X,M,A,S)) :-
+  X in 1..4000, M in 1..4000, A in 1..4000, S in 1..4000.
+
+yes(F, R, N, I) :- field(I, F, Val), constrain(yes, R, Val, N).
+no(F, R, N, I)  :- field(I, F, Val), constrain(no,  R, Val, N).
+
+constrain(yes, <, X, Y) :- X #< Y.
+constrain(yes, >, X, Y) :- X #> Y.
+constrain(no,  <, X, Y) :- X #>= Y.
+constrain(no,  >, X, Y) :- X #=< Y.
+
+comb_size(i(X,M,A,S), Size) :-
+  fd_size(X, XN), fd_size(M, MN), fd_size(A, AN), fd_size(S, SN),
+  Size is XN * MN * AN * SN.
+
+part2(File) :-
+  once(phrase_from_file(file(Ws, _), File)),
+  findall(I, run2(Ws, [goto(in)], I), Is),
+  maplist(comb_size, Is, Ns),
+  foldl(plus, Ns, 0, N),
+  writeln(N).
+
+
+% vim: set ft=prolog :
diff --git a/lib/fin.quox b/lib/fin.quox
new file mode 100644
index 0000000..1e68c1f
--- /dev/null
+++ b/lib/fin.quox
@@ -0,0 +1,207 @@
+load "nat.quox"
+load "either.quox"
+load "maybe.quox"
+
+
+namespace fin {
+
+def0 LT : ℕ → ℕ → ★ =
+  λ m n ⇒
+    nat.elim-pairω¹ (λ _ _ ⇒ ★)
+      False             -- 0      ≮ 0
+      (λ n   p ⇒ True)  -- 0      < succ n
+      (λ m   p ⇒ False) -- succ m ≮ 0
+      (λ m n p ⇒ p)     -- succ m < succ n ⇔ m < n
+      m n
+
+
+def0 lt-irr : (m n : ℕ) → (p q : LT m n) → p ≡ q : LT m n =
+  λ m n ⇒
+    nat.elim-pairω (λ m n ⇒ (p q : LT m n) → p ≡ q : LT m n)
+      false.irr (λ _ _ ⇒ true.irr) (λ _ _ ⇒ false.irr) (λ _ _ p ⇒ p) m n
+
+def0 lt-irr-het :
+    (m m' n n' : ℕ) → (mm : m ≡ m' : ℕ) → (nn : n ≡ n' : ℕ) →
+    (p : LT m n) → (q : LT m' n') →
+    Eq (𝑖 ⇒ LT (mm @𝑖) (nn @𝑖)) p q =
+  λ m m' n n' mm nn p q ⇒ δ 𝑖 ⇒
+    lt-irr (mm @𝑖) (nn @𝑖)
+           (coe (𝑗 ⇒ LT (mm @𝑗) (nn @𝑗)) @0 @𝑖 p)
+           (coe (𝑗 ⇒ LT (mm @𝑗) (nn @𝑗)) @1 @𝑖 q) @𝑖
+
+def0 lt-irr-het-left :
+    (m m' n : ℕ) → (mm : m ≡ m' : ℕ) → (p : LT m n) → (q : LT m' n) →
+    Eq (𝑖 ⇒ LT (mm @𝑖) n) p q =
+  λ m m' n mm ⇒ lt-irr-het m m' n n mm (δ _ ⇒ n)
+
+
+def0 lt-true : (m n : ℕ) → LT m n → LT m n ≡ True : ★ =
+  λ m n p ⇒
+    nat.elim-pairω¹ (λ m n ⇒ LT m n → LT m n ≡ True : ★)
+      (λ       ff ⇒ void¹ (False ≡ True : ★) ff)
+      (λ   n p tt ⇒ δ _ ⇒ True)
+      (λ m   p ff ⇒ void¹ (False ≡ True : ★) ff)
+      (λ n m p tf ⇒ p tf)
+      m n p
+
+
+#[compile-scheme "(lambda% (m n) (if (< m n) dec.Yes dec.No))"]
+def lt? : ω.(m n : ℕ) → Dec (LT m n) =
+  nat.elim-pairω (λ m n ⇒ Dec (LT m n))
+    (No (LT 0 0) (λ v ⇒ v))
+    (λ n p ⇒ Yes (LT 0 (succ n)) 'true)
+    (λ m p ⇒ No  (LT (succ m) 0) (λ v ⇒ v))
+    (λ m n p ⇒
+      dec.elim (LT m n) (λ _ ⇒ Dec (LT (succ m) (succ n)))
+        (λ yes ⇒ Yes (LT (succ m) (succ n)) yes)
+        (λ no  ⇒ No  (LT (succ m) (succ n)) no) p)
+
+
+def0 Fin : ℕ → ★ =
+  λ n ⇒ (i : ℕ) × [0.LT i n]
+
+
+def to-ℕ : 0.(n : ℕ) → Fin n → ℕ =
+  λ n i ⇒ case i return ℕ of { (i, p) ⇒ drop0 (LT i n) ℕ p i }
+
+def0 to-ℕ-fst : (n : ℕ) → (i : Fin n) → to-ℕ n i ≡ fst i : ℕ =
+  λ n i ⇒ drop0-eq (LT (fst i) n) ℕ (snd i) (fst i)
+
+def0 to-ℕ-eq : (n : ℕ) → (i j : Fin n) →
+               to-ℕ n i ≡ to-ℕ n j : ℕ → i ≡ j : Fin n =
+  λ n i' j' ij' ⇒
+    let i = fst i'; ilt = get0 (LT i n) (snd i');
+        j = fst j'; jlt = get0 (LT j n) (snd j');
+        ij : (i ≡ j : ℕ) =
+          coe (𝑘 ⇒ to-ℕ-fst n i' @𝑘 ≡ j : ℕ)
+            (coe (𝑘 ⇒ to-ℕ n i' ≡ to-ℕ-fst n j' @𝑘 : ℕ) ij');
+        ltt : Eq (𝑘 ⇒ LT (ij @𝑘) n) ilt jlt =
+          lt-irr-het-left i j n ij ilt jlt in
+    δ 𝑘 ⇒ (ij @𝑘, [ltt @𝑘])
+
+
+def fin? : ω.(n i : ℕ) → Maybe (Fin n) =
+  λ n i ⇒
+    dec.elim (LT i n) (λ _ ⇒ Maybe (Fin n))
+      (λ yes ⇒ Just (Fin n) (i, [yes]))
+      (λ no  ⇒ Nothing (Fin n))
+      (lt? i n)
+
+
+def F0 : 0.(n : ℕ) → Fin (succ n) = λ _ ⇒ (0, ['true])
+def FS : 0.(n : ℕ) → Fin n → Fin (succ n) =
+  λ n i ⇒ case i return Fin (succ n) of { (i, p) ⇒ (succ i, p) }
+
+def dup! : 0.(n : ℕ) → (i : Fin n) → Dup (Fin n) i =
+  λ n ilt ⇒
+    case ilt        return ilt' ⇒ Dup (Fin n) ilt'     of { (i, lt0) ⇒
+    case lt0        return ilt' ⇒ Dup (Fin n) (i, lt0) of { [lt] ⇒
+    case nat.dup! i return        Dup (Fin n) (i, lt0) of { (iω, ii0) ⇒
+      case iω
+      return iω' ⇒ 0.(iω' ≡ iω : [ω.ℕ]) → Dup (Fin n) (i, lt0)
+      of { [i!] ⇒ λ iiω ⇒
+        let 0.iωi : iω ≡ [i] : [ω.ℕ] = get0 (iω ≡ [i] : [ω.ℕ]) ii0;
+        in
+        0
+      } (δ _ ⇒ iω)
+    }}}
+
+{-
+    case ilt return ilt' ⇒ Dup (Fin n) ilt'      of { (i, lt0) ⇒
+    case lt0 return lt0' ⇒ Dup (Fin n) (i, lt0') of { [lt] ⇒
+    case nat.dup! i return Dup (Fin n) (i, [lt]) of { (iω, eq0) ⇒
+      let ω.i! = fst ieq!;
+          0.ii  : i! ≡ i : ℕ = get0 (i! ≡ i : ℕ) (snd ieq!);
+          0.lt! : LT i! n    = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt;
+          0.ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt =
+            lt-irr-het-left i! i n ii lt! lt;
+          ω.ilt! : Fin n = (i!, [lt!]);
+          0.iltt : ilt! ≡ ilt : Fin n =
+            δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])];
+      in
+      ([ilt!], [iltt])
+      -- [((i!, [lt!]), [δ 𝑘 ⇒ (ii @𝑘, [ltt @𝑘])])]
+    }}}
+-}
+
+{-
+def dup : 0.(n : ℕ) → Fin n → [ω.Fin n] =
+  λ n i ⇒ appω (Sing (Fin n) i) (Fin n) (λ p ⇒ fst p) (dup! n i)
+-}
+
+{-
+def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
+  λ n i ⇒
+
+    appω (Sing (Fin n) i) [0.dup n i ≡ [i] : [ω.Fin n]]
+         (λ p ⇒ snd p) (dup! n i)
+-}
+
+{-
+def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
+  λ n i ⇒
+    case dup! n i return i' ⇒ fst i' ≡ [i] : 
+-}
+
+{-
+def dup : 0.(n : ℕ) → Fin n → [ω.Fin n] =
+  λ n ilt ⇒
+  case ilt return [ω.Fin n] of { (i, lt0) ⇒
+  case lt0 return [ω.Fin n] of { [lt] ⇒
+    case nat.dup i
+    return i' ⇒ 0.(i' ≡ [i] : [ω.ℕ]) → [ω.Fin n]
+    of { [i!] ⇒ λ iiω ⇒
+      let0 ii  : i! ≡ i : ℕ = boxω-inj ℕ i! i iiω;
+           lt! : LT i! n    = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt in
+      [(i!, [lt!])]
+    } (nat.dup-ok i)
+  }}
+-}
+
+{-
+def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
+  λ n ilt ⇒ δ 𝑘 ⇒
+    let i = fst ilt; lt = get0 (LT i n) (snd ilt);
+    in
+-}
+
+{-
+def dup-ok : 0.(n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
+  λ n i ⇒
+  case i return i' ⇒ dup n i' ≡ [i'] : [ω.Fin n] of { (i, lt0) ⇒
+  case lt0 return lt' ⇒ dup n (i, lt') ≡ [(i, lt')] : [ω.Fin n] of { [lt] ⇒
+    case nat.dup i
+    return i' ⇒ (i' ≡ [i] : [ω.ℕ]) →
+                dup n (i, [lt]) ≡ [(i, [lt])] : [ω.Fin n]
+    of { [i!] ⇒ λ iiω ⇒
+      let0 ii  : i! ≡ i : ℕ = boxω-inj ℕ i! i iiω;
+           lt! : LT i! n    = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt;
+           ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt =
+             lt-irr-het i! i n n ii (δ _ ⇒ n) lt! lt
+      in
+      δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])]
+    } (nat.dup-ok i)
+  }}
+-}
+
+
+{-
+def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
+  λ n ilt ⇒
+    case ilt return i' ⇒ dup n i' ≡ [i'] : [ω.Fin n] of { (i, lt0) ⇒
+    case lt0 return lt' ⇒ dup n (i, lt') ≡ [(i, lt')] : [ω.Fin n] of { [lt] ⇒
+      let i! = getω ℕ (nat.dup i);
+          ii  : i! ≡ i : ℕ = δ 𝑘 ⇒ getω ℕ (nat.dup-ok i @𝑘);
+          lt! : LT i! n = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt;
+          ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt =
+            lt-irr-het i! i n n ii (δ _ ⇒ n) lt! lt
+      in
+      δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])]
+  }}
+-}
+
+}
+
+def0 Fin = fin.Fin
+def  F0  = fin.F0
+def  FS  = fin.FS
diff --git a/lib/misc.quox b/lib/misc.quox
index f43adc4..8f239ab 100644
--- a/lib/misc.quox
+++ b/lib/misc.quox
@@ -1,23 +1,41 @@
-def0 True : ★ = {true}
-
 namespace true {
+  def0 True : ★ = {true}
+
   def drop : 0.(A : ★) → True → A → A =
     λ A t x ⇒ case t return A of { 'true ⇒ x }
+
+  def0 eta : (s : True) → s ≡ 'true : True =
+    λ s ⇒ case s return s' ⇒ s' ≡ 'true : True of { 'true ⇒ δ 𝑖 ⇒ 'true }
+
+  def0 irr : (s t : True) → s ≡ t : True =
+    λ s t ⇒
+      coe (𝑖 ⇒ eta s @𝑖 ≡ t : True) @1 @0
+        (coe (𝑖 ⇒ 'true ≡ eta t @𝑖 : True) @1 @0 (δ _ ⇒ 'true))
 }
+def0 True = true.True
+
+namespace false {
+  def0 False : ★ = {}
+
+  def void : 0.(A : ★) → 0.False → A =
+    λ A v ⇒ case0 v return A of { }
+
+  def0 irr : (u v : False) → u ≡ v : False =
+    λ u v ⇒ void (u ≡ v : False) u
+}
+def0 False = false.False
+def void = false.void
+
 
-def0 False : ★ = {}
 def0 Not : ★ → ★ = λ A ⇒ ω.A → False
 
-def void : 0.(A : ★) → 0.False → A =
-  λ A v ⇒ case0 v return A of { }
-
 def0 Iff : ★ → ★ → ★ = λ A B ⇒ (A → B) × (B → A)
 
-def0 All : (A : ★) → (0.A → ★) → ★ =
+def0 All : (A : ★) → (A → ★) → ★ =
   λ A P ⇒ (x : A) → P x
 
 def0 cong :
-    (A : ★) → (P : 0.A → ★) → (p : All A P) →
+    (A : ★) → (P : A → ★) → (p : All A P) →
     (x y : A) → (xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) =
   λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖)
 
@@ -33,26 +51,31 @@ def0 coherence :
     δ 𝑗 ⇒ coe (𝑖 ⇒ AB @𝑖) @0 @𝑗 x
 
 
-def0 eq-f :
-    0.(A : ★) → 0.(P : 0.A → ★) →
-    0.(p : All A P) → 0.(q : All A P) →
-    0.A → ★ =
+def0 eq-f : (A : ★) → (P : A → ★) → (p : All A P) → (q : All A P) → A → ★ =
   λ A P p q x ⇒ p x ≡ q x : P x
 
 def funext :
-    0.(A : ★) → 0.(P : 0.A → ★) → 0.(p q : All A P) →
+    0.(A : ★) → 0.(P : A → ★) → 0.(p q : All A P) →
     (All A (eq-f A P p q)) → p ≡ q : All A P =
   λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖
 
 def refl : 0.(A : ★) → (x : A) → x ≡ x : A = λ A x ⇒ δ _ ⇒ x
 
 def sym : 0.(A : ★) → 0.(x y : A) → (x ≡ y : A) → y ≡ x : A =
-  λ A x y eq ⇒ δ 𝑖 ⇒ comp A (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 }
+  λ A x y eq ⇒ coe (𝑗 ⇒ eq @𝑗 ≡ x : A) (δ _ ⇒ eq @0)
+    -- btw this uses eq @0 instead of just x because of the quantities
+
+def trans10 : 0.(A : ★) → 0.(x y z : A) →
+              1.(x ≡ y : A) → 0.(y ≡ z : A) → x ≡ z : A =
+  λ A x y z eq1 eq2 ⇒ coe (𝑗 ⇒ x ≡ eq2 @𝑗 : A) eq1
+
+def trans01 : 0.(A : ★) → 0.(x y z : A) →
+              0.(x ≡ y : A) → 1.(y ≡ z : A) → x ≡ z : A =
+  λ A x y z eq1 eq2 ⇒ coe (𝑗 ⇒ eq1 @𝑗 ≡ z : A) @1 @0 eq2
 
 def trans : 0.(A : ★) → 0.(x y z : A) →
             ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A =
-  λ A x y z eq1 eq2 ⇒ δ 𝑖 ⇒
-    comp A (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 }
+  λ A x y z eq1 eq2 ⇒ trans01 A x y z eq1 eq2
 
 def appω : 0.(A B : ★) → ω.(f : ω.A → B) → [ω.A] → [ω.B] =
   λ A B f x ⇒
@@ -70,16 +93,22 @@ def getω : 0.(A : ★) → [ω.A] → A =
 def0 get0 : (A : ★) → [0.A] → A =
   λ A x ⇒ case x return A of { [x] ⇒ x }
 
-def drop0 : 0.(A B : ★) → [0.B] → A → A =
-  λ A B x y ⇒ case x return A of { [_] ⇒ y }
+def drop0 : 0.(A B : ★) → [0.A] → B → B =
+  λ A B x y ⇒ case x return B of { [_] ⇒ y }
 
-def0 drop0-eq : (A B : ★) → (x : [0.B]) → (y : A) → drop0 A B x y ≡ y : A =
+def0 drop0-eq : (A B : ★) → (x : [0.A]) → (y : B) → drop0 A B x y ≡ y : B =
   λ A B x y ⇒
-  case x return x' ⇒ drop0 A B x' y ≡ y : A of { [_] ⇒ δ 𝑖 ⇒ y }
+  case x return x' ⇒ drop0 A B x' y ≡ y : B of { [_] ⇒ δ 𝑖 ⇒ y }
 
 def0 HEq : (A B : ★) → A → B → ★¹ =
   λ A B x y ⇒ (AB : A ≡ B : ★) × Eq (𝑖 ⇒ AB @𝑖) x y
 
+def0 boxω-inj : (A : ★) → (x y : A) → [x] ≡ [y] : [ω.A] → x ≡ y : A =
+  λ A x y xy ⇒ δ 𝑖 ⇒ getω A (xy @𝑖)
+
+def revive0 : 0.(A : ★) → 0.[0.A] → [0.A] =
+  λ A s ⇒ [get0 A s]
+
 
 def0 Sing : (A : ★) → A → ★ =
   λ A x ⇒ (val : A) × [0. val ≡ x : A]
@@ -88,36 +117,39 @@ def sing : 0.(A : ★) → (x : A) → Sing A x =
   λ A x ⇒ (x, [δ _ ⇒ x])
 
 def0 Dup : (A : ★) → A → ★ =
-  λ A x ⇒ [ω. Sing A x]
+  λ A x ⇒ (x! : [ω.A]) × [0. x! ≡ [x] : [ω.A]]
 
 def dup-from-parts :
     0.(A : ★) →
     (dup : A → [ω.A]) →
     0.(prf : (x : A) → dup x ≡ [x] : [ω.A]) →
     (x : A) → Dup A x =
-  λ A dup prf x ⇒
-    case dup x return x! ⇒ 0.(x! ≡ dup x : [ω.A]) → [ω. Sing A x] of {
-      [x'] ⇒ λ eq ⇒
-        let0 prf'-ω : [x'] ≡ [x] : [ω.A] =
-               trans [ω.A] [x'] (dup x) [x] eq (prf x);
-             prf' : x' ≡ x : A =
-               δ 𝑖 ⇒ getω A (prf'-ω @𝑖) in
-        [(x', [prf'])]
-    } (δ 𝑖 ⇒ dup x)
+  λ A dup prf x ⇒ (dup x, [prf x])
 
 def drop-from-dup :
     0.(A : ★) → (A → [ω.A]) → 0.(B : ★) → A → B → B =
   λ A dup B x y ⇒ case dup x return B of { [_] ⇒ y }
 
 
+def dup0 : 0.(A : ★) → [0.A] → [ω.[0.A]] =
+  λ A x ⇒ case x return [ω.[0.A]] of { [x] ⇒ [[x]] }
+
+def0 dup0-ok : (A : ★) → (x : [0.A]) → dup0 A x ≡ [x] : [ω.[0.A]] =
+  λ A x ⇒
+  case x return x' ⇒ dup0 A x' ≡ [x'] : [ω.[0.A]] of { [x] ⇒ δ 𝑖 ⇒ [[x]] }
+
+def dup0! : 0.(A : ★) → (x : [0.A]) → Dup [0.A] x =
+  λ A ⇒ dup-from-parts [0.A] (dup0 A) (dup0-ok A)
+
+
 namespace sing {
 
 def val : 0.(A : ★) → 0.(x : A) → Sing A x → A =
   λ A x sg ⇒
-  case sg return A of { (x', eq) ⇒ drop0 A (x' ≡ x : A) eq x' }
+  case sg return A of { (x', eq) ⇒ drop0 (x' ≡ x : A) A eq x' }
 
 def0 val-fst : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ fst sg : A =
-  λ A x sg ⇒ drop0-eq A (fst sg ≡ x : A) (snd sg) (fst sg)
+  λ A x sg ⇒ drop0-eq (fst sg ≡ x : A) A (snd sg) (fst sg)
 
 def0 proof : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ x : A =
   λ A x sg ⇒
@@ -131,5 +163,4 @@ def app : 0.(A B : ★) → 0.(x : A) →
     case eq return Sing B (f x) of { [eq] ⇒ (f x_, [δ 𝑖 ⇒ f (eq @𝑖)]) }
   }
 
-
 }
diff --git a/lib/nat.quox b/lib/nat.quox
index be2a178..d548213 100644
--- a/lib/nat.quox
+++ b/lib/nat.quox
@@ -75,7 +75,7 @@ def0 dup-ok : (n : ℕ) → dup n ≡ [n] : [ω.ℕ] =
     succ _, ih ⇒ δ 𝑖 ⇒ succ-boxω (ih @𝑖)
   }
 
-def dup! : (n : ℕ) → [ω. Sing ℕ n] =
+def dup! : (n : ℕ) → Dup ℕ n =
   dup-from-parts ℕ dup dup-ok
 
 
@@ -152,6 +152,38 @@ def0 not-succ-self : (m : ℕ) → Not (m ≡ succ m : ℕ) =
   }
 
 
+def divmod : ℕ → ℕ → ℕ × ℕ =
+  -- https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Init.Nat.html#divmod
+  letω divmod' : ℕ → ω.ℕ → ℕ → ℕ → ℕ × ℕ =
+    λ x ⇒
+    case x return ω.ℕ → ℕ → ℕ → ℕ × ℕ of {
+      0          ⇒ λ y q u ⇒ (q, u);
+      succ _, 1.f' ⇒ λ y q u ⇒
+        case u return ℕ × ℕ of {
+          0       ⇒ f' y (succ q) y;
+          succ u' ⇒ f' y q u'
+        }
+    } in
+  λ x y ⇒
+  case y return ℕ × ℕ of {
+    0       ⇒ drop (ℕ × ℕ) x (0, 0);
+    succ y' ⇒
+      case dup y' return ℕ × ℕ of { [y'] ⇒
+        case divmod' x y' 0 y' return ℕ × ℕ of { (d, m) ⇒ (d, minus y' m) }
+      }
+  }
+
+def div : ℕ → ℕ → ℕ =
+  λ x y ⇒ case divmod x y return ℕ of { (d, m) ⇒ drop ℕ m d }
+
+def mod : ℕ → ℕ → ℕ =
+  λ x y ⇒ case divmod x y return ℕ of { (d, m) ⇒ drop ℕ d m }
+
+
+def0 div-5-2 : div 5 2 ≡ 2 : ℕ = δ 𝑖 ⇒ 2
+def0 mod-5-2 : mod 5 2 ≡ 1 : ℕ = δ 𝑖 ⇒ 1
+
+
 #[compile-scheme "(lambda% (m n) (if (= m n) Yes No))"]
 def eq? : DecEq ℕ =
   λ m n ⇒
diff --git a/lib/pair.quox b/lib/pair.quox
index 4bf33c6..9f93009 100644
--- a/lib/pair.quox
+++ b/lib/pair.quox
@@ -1,54 +1,49 @@
 namespace pair {
 
-def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x;
-
-{-
--- now builtins
-def fst : 0.(A : ★) → 0.(B : A → ★) → ω.(Σ A B) → A =
-  λ A B p ⇒ caseω p return A of { (x, _) ⇒ x };
-
-def snd : 0.(A : ★) → 0.(B : A → ★) → ω.(p : Σ A B) → B (fst A B p) =
-  λ A B p ⇒ caseω p return p' ⇒ B (fst A B p') of { (_, y) ⇒ y };
--}
+def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x
 
 def uncurry :
     0.(A : ★) → 0.(B : A → ★) → 0.(C : (x : A) → (B x) → ★) →
     (f : (x : A) → (y : B x) → C x y) →
     (p : Σ A B) → C (fst p) (snd p) =
   λ A B C f p ⇒
-    case p return p' ⇒ C (fst p') (snd p') of { (x, y) ⇒ f x y };
+    case p return p' ⇒ C (fst p') (snd p') of { (x, y) ⇒ f x y }
 
 def uncurry' :
     0.(A B C : ★) → (A → B → C) → (A × B) → C =
-  λ A B C ⇒ uncurry A (λ _ ⇒ B) (λ _ _ ⇒ C);
+  λ A B C ⇒ uncurry A (λ _ ⇒ B) (λ _ _ ⇒ C)
 
 def curry :
     0.(A : ★) → 0.(B : A → ★) → 0.(C : (Σ A B) → ★) →
     (f : (p : Σ A B) → C p) → (x : A) → (y : B x) → C (x, y) =
-  λ A B C f x y ⇒ f (x, y);
+  λ A B C f x y ⇒ f (x, y)
 
 def curry' :
     0.(A B C : ★) → (A × B → C) → A → B → C =
-  λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C);
+  λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C)
 
 def0 fst-snd :
     (A : ★) → (B : A → ★) →
     (p : Σ A B) → p ≡ (fst p, snd p) : Σ A B =
-  λ A B p ⇒
-    case p
-    return p' ⇒ p' ≡ (fst p', snd p') : Σ A B
-    of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) };
+  λ A B p ⇒ δ 𝑖 ⇒ p -- η
 
 def0 fst-eq :
     (A : ★) → (B : A → ★) →
     (p q : Σ A B) → p ≡ q : Σ A B → fst p ≡ fst q : A =
-  λ A B p q eq ⇒ δ 𝑖 ⇒ fst (eq @𝑖);
+  λ A B p q eq ⇒ δ 𝑖 ⇒ fst (eq @𝑖)
 
 def0 snd-eq :
     (A : ★) → (B : A → ★) →
     (p q : Σ A B) → (eq : p ≡ q : Σ A B) →
     Eq (𝑖 ⇒ B (fst-eq A B p q eq @𝑖)) (snd p) (snd q) =
-  λ A B p q eq ⇒ δ 𝑖 ⇒ snd (eq @𝑖);
+  λ A B p q eq ⇒ δ 𝑖 ⇒ snd (eq @𝑖)
+
+def0 pair-eq :
+    (A : ★) → (B : A → ★) →
+    (x0 x1 : A) → (y0 : B x0) → (y1 : B x1) →
+    (xx : x0 ≡ x1 : A) → (yy : Eq (𝑖 ⇒ B (xx @𝑖)) y0 y1) →
+    (x0, y0) ≡ (x1, y1) : ((x : A) × B x) =
+  λ A B x0 x1 y0 y1 xx yy ⇒ δ 𝑖 ⇒ (xx @𝑖, yy @𝑖)
 
 def map :
     0.(A A' : ★) →
@@ -56,19 +51,17 @@ def map :
     (f : A → A') → (g : 0.(x : A) → (B x) → B' (f x)) →
     Σ A B → Σ A' B' =
   λ A A' B B' f g p ⇒
-    case p return Σ A' B' of { (x, y) ⇒ (f x, g x y) };
+    case p return Σ A' B' of { (x, y) ⇒ (f x, g x y) }
 
 def map' : 0.(A A' B B' : ★) → (A → A') → (B → B') → (A × B) → A' × B' =
-  λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g);
+  λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g)
 
 def map-fst : 0.(A A' B : ★) → (A → A') → A × B → A' × B =
-  λ A A' B f ⇒ map' A A' B B f (λ x ⇒ x);
+  λ A A' B f ⇒ map' A A' B B f (λ x ⇒ x)
 
 def map-snd : 0.(A B B' : ★) → (B → B') → A × B → A × B' =
-  λ A B B' f ⇒ map' A A B B' (λ x ⇒ x) f;
+  λ A B B' f ⇒ map' A A B B' (λ x ⇒ x) f
 
 }
 
-def0 Σ   = pair.Σ;
--- def  fst = pair.fst;
--- def  snd = pair.snd;
+def0 Σ   = pair.Σ
diff --git a/lib/string.quox b/lib/string.quox
index ec49fb7..f59c799 100644
--- a/lib/string.quox
+++ b/lib/string.quox
@@ -73,6 +73,9 @@ def from-list : List Char → String =
 def foldl : 0.(A : ★) → A → ω.(A → Char → A) → String → A =
   λ A z f str ⇒ list.foldl Char A z f (to-list str)
 
+def foldlω : 0.(A : ★) → ω.A → ω.(ω.A → ω.Char → A) → ω.String → A =
+  λ A z f str ⇒ list.foldlω Char A z f (to-list str)
+
 def split : ω.(ω.Char → Bool) → ω.String → List String =
   λ p str ⇒
     list.map (List Char) String from-list
@@ -86,8 +89,9 @@ def break : ω.(ω.Char → Bool) → ω.String → String × String =
 def reverse : String → String =
   λ str ⇒ from-list (list.reverse Char (to-list str))
 
-#[compile-scheme "(lambda% (a b) (if (string=? a b) 'true 'false))"]
-postulate eq : ω.String → ω.String → Bool
+#[compile-scheme "(lambda% (y n a b) (if (string=? a b) y n))"]
+postulate eq' : 0.(A : ★) → A → A → ω.String → ω.String → A
+def eq : ω.String → ω.String → Bool = eq' Bool 'true 'false
 
 def null : ω.String → Bool = eq ""
 def not-null : ω.String → Bool = λ s ⇒ bool.not (null s)
@@ -134,7 +138,7 @@ def to-ℕ-or-0 : String → ℕ =
 postulate uncons' : 0.(A : ★) → ω.A → ω.(Char → String → A) → String → A
 
 def uncons : String → Maybe (Char × String) =
-  let0 Ret : ★ = Char × String in
-  uncons' (Maybe Ret) (Nothing Ret) (λ c s ⇒ Just Ret (c, s))
+  let0 Pair : ★ = Char × String in
+  uncons' (Maybe Pair) (Nothing Pair) (λ c s ⇒ Just Pair (c, s))
 
 }
diff --git a/lib/sub.quox b/lib/sub.quox
new file mode 100644
index 0000000..922df34
--- /dev/null
+++ b/lib/sub.quox
@@ -0,0 +1,66 @@
+load "maybe.quox"
+
+namespace sub {
+
+def0 Irr : ★ → ★ =
+  λ A ⇒ (x y : A) → x ≡ y : A
+
+def0 Irr1 : (A : ★) → (A → ★) → ★ =
+  λ A P ⇒ (x : A) → Irr (P x)
+
+def0 Sub : (A : ★) → (P : A → ★) → ★ =
+  λ A P ⇒ (x : A) × [0. P x]
+
+def sub : 0.(A : ★) → 0.(P : A → ★) → (x : A) → 0.(P x) → Sub A P =
+  λ A P x p ⇒ (x, [p])
+
+def sub? : 0.(A : ★) → 0.(P : A → ★) → (ω.(x : A) → Dec (P x)) →
+           ω.(x : A) → Maybe (Sub A P) =
+  λ A P p? x ⇒
+    dec.elim (P x) (λ _ ⇒ Maybe (Sub A P))
+      (λ yes ⇒ Just (Sub A P) (sub A P x yes))
+      (λ no  ⇒ Nothing (Sub A P))
+      (p? x)
+
+def0 sub-eq : (A : ★) → (P : A → ★) → (Irr1 A P) → (x y : Sub A P) →
+              (fst x ≡ fst y : A) → (x ≡ y : Sub A P) =
+  λ A P pirr x y xy0 ⇒
+    let x1 = get0 (P (fst x)) (snd x); y1 = get0 (P (fst y)) (snd y) in
+    let xy1 : Eq (𝑖 ⇒ P (xy0 @𝑖)) x1 y1 =
+      δ 𝑖 ⇒ pirr (xy0 @𝑖)
+        (coe (𝑗 ⇒ P (xy0 @𝑗)) @0 @𝑖 x1)
+        (coe (𝑗 ⇒ P (xy0 @𝑗)) @1 @𝑖 y1) @𝑖 in
+    δ 𝑖 ⇒ (xy0 @𝑖, [xy1 @𝑖])
+
+
+def0 SubDup : (A : ★) → (P : A → ★) → Sub A P → ★ =
+  λ A P s ⇒ (x! : [ω.A]) × [0. x! ≡ [fst s] : [ω.A]]
+
+def subdup : 0.(A : ★) → 0.(P : A → ★) →
+             ((x : A) → Dup A x) → (s : Sub A P) → SubDup A P s =
+  λ A P dupA s ⇒
+    case s return s' ⇒ SubDup A P s' of { (x, p) ⇒
+      drop0 (P x) (SubDup A P (x, p)) p (dupA x)
+    }
+
+
+{-
+type checker loop?????????????????? :(
+def subdup-to-dup :
+    0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
+    0.(s : Sub A P) → SubDup A P s → Dup (Sub A P) s =
+  λ A P pirr s sd ⇒
+    case sd return Dup (Sub A P) s of { (sω, ss0) ⇒
+      case sω
+      return sω' ⇒ 0.(sω' ≡ [fst s] : [ω.A]) → Dup (Sub A P) s
+      of { [s!] ⇒ λ ss' ⇒
+        let ω.p  : [0.P (fst s)] = revive0 (P (fst s)) (snd s);
+            0.ss : s! ≡ fst s : A = boxω-inj A s! (fst s) ss';
+            0.pss : [0.P s!] ≡ [0.P (fst s)] : ★ = (δ 𝑖 ⇒ [0.P (ss @𝑖)]) in
+        ([(s!, coe (𝑖 ⇒ pss @𝑖) @1 @0 p)],
+         [δ 𝑖 ⇒ [(ss @𝑖, coe (𝑗 ⇒ pss @𝑗) @1 @𝑖 p)]])
+      } (δ _ ⇒ sω)
+    }
+-}
+
+}
diff --git a/unfinished/day13.bqn b/unfinished/day13.bqn
new file mode 100644
index 0000000..5edd1c3
--- /dev/null
+++ b/unfinished/day13.bqn
@@ -0,0 +1,13 @@
+Tails ⇐ (1⊸↓)⍟(↕∘≠⊢)
+
+Sym ⇐ ∧´∘⥊ ⌽=⊢
+
+Centers ⇐ { ⌊ (↕≠𝕩) { 𝕨+ 2÷˜ 𝕨-˜ ≠𝕩} 𝕩 }
+
+VC ⇐ (⊑/˜) Centers×Sym¨∘Tails
+HC ⇐ VC⍉
+
+VCenter ⇐ VC⌈(VC⌽˘)
+HCenter ⇐ HC⌈(HC⌽)
+
+Score ⇐ (100×VCenter) + HCenter