From dcce966637a310afd6b31d0367af96b29d7dac27 Mon Sep 17 00:00:00 2001
From: Matthew Toohey <contact@mtoohey.com>
Date: Thu, 8 May 2025 17:16:21 -0400
Subject: [PATCH] add examples

---
 TabularTypeInterpreter/Theorems/Generic.lean  |  0
 .../b2t2/access-subcomponents/getColumn2.tt   |  3 +
 examples/b2t2/access-subcomponents/getRow.tt  |  1 +
 .../b2t2/access-subcomponents/getValue.tt     |  3 +
 examples/b2t2/aggregate/bin.tt                | 19 ++++++
 examples/b2t2/aggregate/count.tt              |  5 ++
 examples/b2t2/aggregate/groupBy.tt            |  5 ++
 examples/b2t2/aggregate/pivotTable.tt         |  9 +++
 examples/b2t2/constructors/addColumn.tt       |  3 +
 examples/b2t2/constructors/addRows.tt         |  2 +
 examples/b2t2/constructors/buildColumn.tt     |  3 +
 examples/b2t2/constructors/crossJoin.tt       |  3 +
 examples/b2t2/constructors/emptyTable.tt      |  1 +
 examples/b2t2/constructors/hcat.tt            |  2 +
 examples/b2t2/constructors/leftJoin.tt        | 13 ++++
 examples/b2t2/constructors/values.tt          |  1 +
 examples/b2t2/constructors/vcat.tt            |  2 +
 examples/b2t2/data-cleaning/pivotLonger.tt    |  7 ++
 examples/b2t2/data-cleaning/pivotWider.tt     | 29 ++++++++
 examples/b2t2/missing-values/completeCases.tt |  3 +
 examples/b2t2/missing-values/dropna.tt        | 10 +++
 examples/b2t2/missing-values/fillna.tt        |  4 ++
 examples/b2t2/ordering/orderBy.tt             | 25 +++++++
 examples/b2t2/ordering/sortByColumns.tt       | 14 ++++
 examples/b2t2/ordering/tsort.tt               |  7 ++
 examples/b2t2/properties/header.tt            |  2 +
 examples/b2t2/properties/ncols.tt             |  2 +
 examples/b2t2/properties/nrows.tt             |  1 +
 examples/b2t2/subtable/distinct.tt            |  2 +
 examples/b2t2/subtable/dropColumn.tt          |  2 +
 examples/b2t2/subtable/dropColumns.tt         |  3 +
 examples/b2t2/subtable/head.tt                |  5 ++
 examples/b2t2/subtable/selectColumns3.tt      |  3 +
 examples/b2t2/subtable/selectRows1.tt         |  2 +
 examples/b2t2/subtable/selectRows2.tt         |  3 +
 examples/b2t2/subtable/tfilter.tt             |  2 +
 examples/b2t2/utilities/find.tt               |  2 +
 examples/b2t2/utilities/flatten.tt            | 14 ++++
 examples/b2t2/utilities/groupByRetentive.tt   |  5 ++
 examples/b2t2/utilities/groupBySubtractive.tt |  7 ++
 examples/b2t2/utilities/groupJoin.tt          |  8 +++
 examples/b2t2/utilities/join.tt               |  8 +++
 examples/b2t2/utilities/renameColumn.tt       |  4 ++
 examples/b2t2/utilities/select.tt             |  2 +
 examples/b2t2/utilities/selectMany.tt         |  8 +++
 examples/b2t2/utilities/transformColumn.tt    |  4 ++
 examples/b2t2/utilities/update.tt             |  4 ++
 examples/core/And.tt                          |  1 +
 examples/core/Bool.tt                         | 14 ++++
 examples/core/Const.tt                        |  1 +
 examples/core/Eq.tt                           |  8 +++
 examples/core/LE.tt                           |  5 ++
 examples/core/Labels.tt                       |  5 ++
 examples/core/LabelsMatch.tt                  |  4 ++
 examples/core/List.tt                         | 68 +++++++++++++++++++
 examples/core/Option.tt                       | 22 ++++++
 examples/core/Unit.tt                         |  1 +
 examples/core/flip.tt                         |  1 +
 examples/core/is.tt                           |  3 +
 59 files changed, 400 insertions(+)
 create mode 100644 TabularTypeInterpreter/Theorems/Generic.lean
 create mode 100644 examples/b2t2/access-subcomponents/getColumn2.tt
 create mode 100644 examples/b2t2/access-subcomponents/getRow.tt
 create mode 100644 examples/b2t2/access-subcomponents/getValue.tt
 create mode 100644 examples/b2t2/aggregate/bin.tt
 create mode 100644 examples/b2t2/aggregate/count.tt
 create mode 100644 examples/b2t2/aggregate/groupBy.tt
 create mode 100644 examples/b2t2/aggregate/pivotTable.tt
 create mode 100644 examples/b2t2/constructors/addColumn.tt
 create mode 100644 examples/b2t2/constructors/addRows.tt
 create mode 100644 examples/b2t2/constructors/buildColumn.tt
 create mode 100644 examples/b2t2/constructors/crossJoin.tt
 create mode 100644 examples/b2t2/constructors/emptyTable.tt
 create mode 100644 examples/b2t2/constructors/hcat.tt
 create mode 100644 examples/b2t2/constructors/leftJoin.tt
 create mode 100644 examples/b2t2/constructors/values.tt
 create mode 100644 examples/b2t2/constructors/vcat.tt
 create mode 100644 examples/b2t2/data-cleaning/pivotLonger.tt
 create mode 100644 examples/b2t2/data-cleaning/pivotWider.tt
 create mode 100644 examples/b2t2/missing-values/completeCases.tt
 create mode 100644 examples/b2t2/missing-values/dropna.tt
 create mode 100644 examples/b2t2/missing-values/fillna.tt
 create mode 100644 examples/b2t2/ordering/orderBy.tt
 create mode 100644 examples/b2t2/ordering/sortByColumns.tt
 create mode 100644 examples/b2t2/ordering/tsort.tt
 create mode 100644 examples/b2t2/properties/header.tt
 create mode 100644 examples/b2t2/properties/ncols.tt
 create mode 100644 examples/b2t2/properties/nrows.tt
 create mode 100644 examples/b2t2/subtable/distinct.tt
 create mode 100644 examples/b2t2/subtable/dropColumn.tt
 create mode 100644 examples/b2t2/subtable/dropColumns.tt
 create mode 100644 examples/b2t2/subtable/head.tt
 create mode 100644 examples/b2t2/subtable/selectColumns3.tt
 create mode 100644 examples/b2t2/subtable/selectRows1.tt
 create mode 100644 examples/b2t2/subtable/selectRows2.tt
 create mode 100644 examples/b2t2/subtable/tfilter.tt
 create mode 100644 examples/b2t2/utilities/find.tt
 create mode 100644 examples/b2t2/utilities/flatten.tt
 create mode 100644 examples/b2t2/utilities/groupByRetentive.tt
 create mode 100644 examples/b2t2/utilities/groupBySubtractive.tt
 create mode 100644 examples/b2t2/utilities/groupJoin.tt
 create mode 100644 examples/b2t2/utilities/join.tt
 create mode 100644 examples/b2t2/utilities/renameColumn.tt
 create mode 100644 examples/b2t2/utilities/select.tt
 create mode 100644 examples/b2t2/utilities/selectMany.tt
 create mode 100644 examples/b2t2/utilities/transformColumn.tt
 create mode 100644 examples/b2t2/utilities/update.tt
 create mode 100644 examples/core/And.tt
 create mode 100644 examples/core/Bool.tt
 create mode 100644 examples/core/Const.tt
 create mode 100644 examples/core/Eq.tt
 create mode 100644 examples/core/LE.tt
 create mode 100644 examples/core/Labels.tt
 create mode 100644 examples/core/LabelsMatch.tt
 create mode 100644 examples/core/List.tt
 create mode 100644 examples/core/Option.tt
 create mode 100644 examples/core/Unit.tt
 create mode 100644 examples/core/flip.tt
 create mode 100644 examples/core/is.tt

diff --git a/TabularTypeInterpreter/Theorems/Generic.lean b/TabularTypeInterpreter/Theorems/Generic.lean
new file mode 100644
index 0000000..e69de29
diff --git a/examples/b2t2/access-subcomponents/getColumn2.tt b/examples/b2t2/access-subcomponents/getColumn2.tt
new file mode 100644
index 0000000..931e494
--- /dev/null
+++ b/examples/b2t2/access-subcomponents/getColumn2.tt
@@ -0,0 +1,3 @@
+def getColumn :
+  ∀ r : R *, l : L, t : *. ⟨l ▹ t⟩ ≲(C) r ⇒ List (Π(C) r) → ⌊l⌋ → List t =
+  \tb l. map (\r. (prj r)/l) tb
diff --git a/examples/b2t2/access-subcomponents/getRow.tt b/examples/b2t2/access-subcomponents/getRow.tt
new file mode 100644
index 0000000..a28fe86
--- /dev/null
+++ b/examples/b2t2/access-subcomponents/getRow.tt
@@ -0,0 +1 @@
+def getRow : ∀ r : R *, u : U. List (Π(u) r) → Int → Option (Π(u) r) = get
diff --git a/examples/b2t2/access-subcomponents/getValue.tt b/examples/b2t2/access-subcomponents/getValue.tt
new file mode 100644
index 0000000..e3fdd02
--- /dev/null
+++ b/examples/b2t2/access-subcomponents/getValue.tt
@@ -0,0 +1,3 @@
+def getValue : ∀ r : R *, l : L, t : *.
+    ⟨l ▹ t⟩ ≲(C) r ⇒ List (Π(C) r) → Int → ⌊l⌋ → Option t =
+  \tb n l. omap (\r. (prj r)/l) (get tb n)
diff --git a/examples/b2t2/aggregate/bin.tt b/examples/b2t2/aggregate/bin.tt
new file mode 100644
index 0000000..74e6438
--- /dev/null
+++ b/examples/b2t2/aggregate/bin.tt
@@ -0,0 +1,19 @@
+def bin : ∀ r : R *, l : L. ⟨l ▹ Int⟩ ≲(C) r ⇒ List (Π(C) r) → ⌊l⌋ → Int →
+    List (Π(N) ⟨'lower' ▹ Int, 'upper' ▹ Int, 'count' ▹ Int⟩) =
+  \tb l n.
+    if n == 0 then
+      nil
+    else
+      let values = map (\r. (prj r)/l) tb in
+      let count = \lower upper. lcount (\v. and (lower <= v) (v < upper)) values
+      in
+      let lower = min values in
+      let upper = max values + 1 in
+      let diff = max - min in
+      let preBins = map
+        (\i. {'lower' ▹ min + diff * i, 'upper' ▹ min + diff * (i + 1)})
+        (range (n - 1))
+      in
+      let bins = snoc preBins {'lower' ▹ min + diff * (n - 1), 'upper' ▹ upper}
+      in
+      map (\b. b ++ {'count' ▹ count (prj b)/'lower' (prj b)/'upper'}) bins
diff --git a/examples/b2t2/aggregate/count.tt b/examples/b2t2/aggregate/count.tt
new file mode 100644
index 0000000..fd3eb57
--- /dev/null
+++ b/examples/b2t2/aggregate/count.tt
@@ -0,0 +1,5 @@
+def count : ∀ r : R *, l : L, t : *. Eq t, ⟨l ▹ t⟩ ≲(C) r ⇒
+    List (Π(C) r) → ⌊l⌋ → List (Π(N) ⟨'value' ▹ t, 'count' ▹ Int⟩) =
+  \tb l.
+    let ks = unique (map (\r. (prj r)/l) tb) in
+    map (\k. lcount (\r. eq k (prj r)/l) tb) ks
diff --git a/examples/b2t2/aggregate/groupBy.tt b/examples/b2t2/aggregate/groupBy.tt
new file mode 100644
index 0000000..78ada14
--- /dev/null
+++ b/examples/b2t2/aggregate/groupBy.tt
@@ -0,0 +1,5 @@
+def groupBy : ∀ r r' : R *, tk tv : *, u u' : U. Eq tk ⇒ List (Π(u) r) →
+    (Π(u) r → tk) → (Π(u) r → tv) → (tk → tv → Π(u') r') → List (Π(u') r') =
+  \tb kf pf af.
+    let ks = unique (map kf tb) in
+    map (\k. af k (map pf (filter (\r. kf r == k) tb))) ks
diff --git a/examples/b2t2/aggregate/pivotTable.tt b/examples/b2t2/aggregate/pivotTable.tt
new file mode 100644
index 0000000..b55295e
--- /dev/null
+++ b/examples/b2t2/aggregate/pivotTable.tt
@@ -0,0 +1,9 @@
+def pivotTable : ∀ r rg r' : R *, li lo : L, ti to : *, u : U.
+    All Eq rg, rg ≲(C) r, ⟨li ▹ ti⟩ ≲(C) r, rg ⊙(u) ⟨lo ▹ to⟩ ~ r' ⇒
+    List (Π(C) r) → Labels u rg → ⌊li⌋ → ⌊lo⌋ → (List ti → to) →
+	List (Π(u) r') =
+  \tb _ li lo f.
+    let groups = unique (map (\r. prj r : Π(C) rg) tb) in
+    map (\g. orderₚ rg g ++
+          {lo ▹ f (map (\r. (prj r)/li) 5)})
+      groups
diff --git a/examples/b2t2/constructors/addColumn.tt b/examples/b2t2/constructors/addColumn.tt
new file mode 100644
index 0000000..9781161
--- /dev/null
+++ b/examples/b2t2/constructors/addColumn.tt
@@ -0,0 +1,3 @@
+def addColumn : ∀ r r' : R *, l : L, t : *. r ⊙(N) ⟨l ▹ t⟩ ~ r' ⇒
+    List (Π(N) r) → ⌊l⌋ → List t → List (Π(N) r') =
+  \tb l col. zip (\o e. o ++ {l ▹ e}) tb col
diff --git a/examples/b2t2/constructors/addRows.tt b/examples/b2t2/constructors/addRows.tt
new file mode 100644
index 0000000..d843967
--- /dev/null
+++ b/examples/b2t2/constructors/addRows.tt
@@ -0,0 +1,2 @@
+def addRows : ∀ r : R *, u : U. List (Π(u) r) → List (Π(u) r) → List (Π(u) r) =
+  append
diff --git a/examples/b2t2/constructors/buildColumn.tt b/examples/b2t2/constructors/buildColumn.tt
new file mode 100644
index 0000000..194d059
--- /dev/null
+++ b/examples/b2t2/constructors/buildColumn.tt
@@ -0,0 +1,3 @@
+def buildColumn : ∀ r r' : R *, l : L, t : *. r ⊙(N) ⟨l ▹ t⟩ ~ r' ⇒
+    List (Π(N) r) → ⌊l⌋ → (Π(N) r → t) → List (Π(N) r') =
+  \tb l f. map (\o. o ++ {l ▹ f o}) tb
diff --git a/examples/b2t2/constructors/crossJoin.tt b/examples/b2t2/constructors/crossJoin.tt
new file mode 100644
index 0000000..d268db3
--- /dev/null
+++ b/examples/b2t2/constructors/crossJoin.tt
@@ -0,0 +1,3 @@
+def crossJoin : ∀ rl rr r : R *. rl ⊙(N) rr ~ r ⇒
+    List (Π(N) rl) → List (Π(N) rr) → List (Π(N) r) =
+  \tbl tbr. map (\l. map (\r. l ++ r) tbr) tbl
diff --git a/examples/b2t2/constructors/emptyTable.tt b/examples/b2t2/constructors/emptyTable.tt
new file mode 100644
index 0000000..bcdf535
--- /dev/null
+++ b/examples/b2t2/constructors/emptyTable.tt
@@ -0,0 +1 @@
+def emptyTable : List Unit = nil
diff --git a/examples/b2t2/constructors/hcat.tt b/examples/b2t2/constructors/hcat.tt
new file mode 100644
index 0000000..e0cccf2
--- /dev/null
+++ b/examples/b2t2/constructors/hcat.tt
@@ -0,0 +1,2 @@
+def hcat : ∀ rl rr r : R *. rl ⊙(N) rr ~ r ⇒
+    List (Π(N) rl) → List (Π(N) rr) → List (Π(N) r) = zip (\l r. l ++ r)
diff --git a/examples/b2t2/constructors/leftJoin.tt b/examples/b2t2/constructors/leftJoin.tt
new file mode 100644
index 0000000..bf14c7e
--- /dev/null
+++ b/examples/b2t2/constructors/leftJoin.tt
@@ -0,0 +1,13 @@
+def leftJoin : ∀ rc rl' rr' rl rr r : R *, u : U.
+    All Eq rc, rc ⊙(u) rl' ~ rl, rc ⊙(u) rr' ~ rr, rl ⊙(u) Lift Option rr' ~ r ⇒
+    List (Π(u) rl) → List (Π(u) rr) → LabelSet rc → List (Π(u) r) =
+  \tbl tbr _. map (\r.
+    let eqr = filter (\r'. eq (prj r : Π(u) rc) (prj r' : Π(u) rc)) tbr in
+    if length eqr > 0 then
+      map (\r'. r ++ prj r') eqr
+    else
+      let nones = ind (\a : R *. Π(C) (Lift Option a)) rr' (\l acc.
+        acc ++ {l ▹ none}
+      ) {} in
+      singleton (r ++ nones)
+  ) tbl
diff --git a/examples/b2t2/constructors/values.tt b/examples/b2t2/constructors/values.tt
new file mode 100644
index 0000000..2dfb488
--- /dev/null
+++ b/examples/b2t2/constructors/values.tt
@@ -0,0 +1 @@
+def values : ∀ r : R *, u : U. List (Π(u) r) → List (Π(u) r) = \tb. tb
diff --git a/examples/b2t2/constructors/vcat.tt b/examples/b2t2/constructors/vcat.tt
new file mode 100644
index 0000000..6448376
--- /dev/null
+++ b/examples/b2t2/constructors/vcat.tt
@@ -0,0 +1,2 @@
+def vcat : ∀ r : R *, u : U. List (Π(u) r) → List (Π(u) r) → List (Π(u) r) =
+  append
diff --git a/examples/b2t2/data-cleaning/pivotLonger.tt b/examples/b2t2/data-cleaning/pivotLonger.tt
new file mode 100644
index 0000000..2729b1d
--- /dev/null
+++ b/examples/b2t2/data-cleaning/pivotLonger.tt
@@ -0,0 +1,7 @@
+def pivotLonger : ∀ r rk rr r' : R *, lk lv : L, t : *.
+    rr ⊙(C) Lift (Const t) rk ~ r,
+    rr ⊙(C) ⟨lk ▹ Σ(C) (Lift (Const Unit) rk), lv ▹ t⟩ ~ r' ⇒
+    List (Π(C) r) → LabelSet rk → ⌊lk⌋ → ⌊lv⌋ → List (Π(C) r') =
+  \tb _ lk lv. lflatten (map (\r. map (\kv. (prj r : Π(C) rr) ++ kv)
+    (ind (\_ : *. List (Π(N) ⟨lk ▹ Σ(C) (Lift (Const Unit) rk), lv ▹ t⟩)) rk
+      (\l acc. {lk ▹ inj [l ▹ {}], lv ▹ (prj r)/l} :: acc) nil)) tb)
diff --git a/examples/b2t2/data-cleaning/pivotWider.tt b/examples/b2t2/data-cleaning/pivotWider.tt
new file mode 100644
index 0000000..af7c61e
--- /dev/null
+++ b/examples/b2t2/data-cleaning/pivotWider.tt
@@ -0,0 +1,29 @@
+def pivotWider : ∀ r rk rr r' : R *, lk lv : L, t : *, u : U. All Eq rr,
+    rr ⊙(u) ⟨lk ▹ Σ(u) (Lift (Const Unit) rk), lv ▹ t⟩ ~ r,
+    rr ⊙(u) Lift (Const (Option t)) rk ~ r' ⇒
+    List (Π(u) r) → ⌊lk⌋ → ⌊lv⌋ → List (Π(u) r') =
+  \tb lk lv.
+    let groups = fold (\r acc.
+      let res = fold (\group acc.
+        if and (not acc/'found') (rowEq group/'shared' (prj r)) then
+          {
+            'updated' ▹ {
+              'shared' ▹ group/'shared',
+              'kvs' ▹ prj r ++ group/'kvs'
+            } :: acc/'updated',
+            'found' ▹ true
+          }
+        else
+          {'updated' ▹ group :: acc/'updated', 'found' ▹ acc/'found'}
+      ) {'updated' ▹ nil, 'found' ▹ false} acc in
+      if res/'found' then
+        res/'updated'
+      else
+        {'shared' ▹ prj r, 'shared' ▹ singleton (prj r)} :: acc
+    ) tb in
+    map (\group.
+      group/'shared' ++ ind (\a : R *. Π(u) (Lift (Const (Option t)) a)) rk
+        (\l acc. acc ++ {l ▹ fold (\kv acc.
+          if and (isNone acc) (is l kv/lk) then some kv/lv else acc
+        ) none group/'kvs'}) {}
+    ) groups
diff --git a/examples/b2t2/missing-values/completeCases.tt b/examples/b2t2/missing-values/completeCases.tt
new file mode 100644
index 0000000..d618690
--- /dev/null
+++ b/examples/b2t2/missing-values/completeCases.tt
@@ -0,0 +1,3 @@
+def completeCases : ∀ r : R *, l : L, t : *. ⟨l ▹ Option t⟩ ≲(C) r ⇒
+    List (Π(C) r) → ⌊l⌋ → List Bool =
+  \tb l. map (\r. isSome (prj r)/l) tb
diff --git a/examples/b2t2/missing-values/dropna.tt b/examples/b2t2/missing-values/dropna.tt
new file mode 100644
index 0000000..f55b18b
--- /dev/null
+++ b/examples/b2t2/missing-values/dropna.tt
@@ -0,0 +1,10 @@
+def dropna : ∀ r rm rr r' : R *. Split Option rm rr r, rm ⊙(C) rr ~ r' ⇒
+    List (Π(C) r) → List (Π(C) r') =
+  filterMap (\r.
+    let s = splitₚ Option r in
+    let m = (prj s)/'match' in
+    omap (\unwrapped. unwrapped ++ (prj s)/'rest')
+      (ind (\a : R *. Option (Π(C) a)) rm (\l.
+        bind (\acc. map (\x. acc ++ {l ▹ x}) (prj m)/l)
+      ) (some {}))
+  )
diff --git a/examples/b2t2/missing-values/fillna.tt b/examples/b2t2/missing-values/fillna.tt
new file mode 100644
index 0000000..2f15b22
--- /dev/null
+++ b/examples/b2t2/missing-values/fillna.tt
@@ -0,0 +1,4 @@
+def fillna : ∀ r ro r' : R *, l : L, t : *.
+    ⟨l ▹ Option t⟩ ⊙(C) ro ~ r, ⟨l ▹ t⟩ ⊙(C) ro ~ r' ⇒
+    List (Π(C) r) → ⌊l⌋ → t → List (Π(C) r') =
+  \tb l default. map (\r. prj r ++ {l ▹ ogetD (prj r)/l default}) tb
diff --git a/examples/b2t2/ordering/orderBy.tt b/examples/b2t2/ordering/orderBy.tt
new file mode 100644
index 0000000..99fc141
--- /dev/null
+++ b/examples/b2t2/ordering/orderBy.tt
@@ -0,0 +1,25 @@
+type Compare =
+  \r : R *, u : U, a : *. Π(N) ⟨'getKey' ▹ Π(u) r → a, 'compare' ▹ a → a → Bool⟩
+
+def orderBy : ∀ r rk : R *, u : U.
+    List (Π(u) r) → Π(N) (Lift (Compare r u)) rk → List (Π(u) r) =
+  \tb cs.
+    let rowsAndKeys = map (\r. {
+      'row' ▹ r,
+      'keys' ▹ ind Π(N) rk (\l acc. acc ++ {l ▹ (prj (prj cs)/l)/'getKey' r}) {}
+    }) tb in
+    let cs' = ind (\a : R *. Π(N) (Lift (\a : *. a → a → Bool) a)) rk
+      (\l acc. acc ++ {l ▹ (prj (prj cs)/l)/'compare'}) {} in
+    let rowLe : Π(N) rk → Π(N) rk → Bool =
+      \r0 r1. ogetD (ind (Const (Option Bool)) rk (\l acc.
+        if isSome acc then
+          acc
+        else if and ((prj cs')/l (prj r0)/l (prj r1)/l)
+                  (le (prj r1)/l (prj r0)/l) then
+          none
+        else
+          some (le (prj r0)/l (prj r1)/l)
+      ) none) true
+    in
+    map (\rk. (prj rk)/'row')
+      (sortBy (\r0 r1. rowLe (prj r0) (prj r1)) tb)
diff --git a/examples/b2t2/ordering/sortByColumns.tt b/examples/b2t2/ordering/sortByColumns.tt
new file mode 100644
index 0000000..7155876
--- /dev/null
+++ b/examples/b2t2/ordering/sortByColumns.tt
@@ -0,0 +1,14 @@
+def sortByColumns : ∀ r r' : R *, u : U. r' ≲(u) r, All LE r' ⇒
+    List (Π(u) r) → LabelList r' → List (Π(u) r) =
+  \tb _.
+    let rowLe : Π(N) r' → Π(N) r' → Bool =
+      \r0 r1. ogetD (ind (Const (Option Bool)) r' (\l acc.
+        if isSome acc then
+          acc
+        else if and (le (prj r0)/l (prj r1)/l) (le (prj r1)/l (prj r0)/l) then
+          none
+        else
+          some (le (prj r0)/l (prj r1)/l)
+      ) none) true
+    in
+    sortBy (\r0 r1. rowLe (prj r0) (prj r1)) tb
diff --git a/examples/b2t2/ordering/tsort.tt b/examples/b2t2/ordering/tsort.tt
new file mode 100644
index 0000000..123ba24
--- /dev/null
+++ b/examples/b2t2/ordering/tsort.tt
@@ -0,0 +1,7 @@
+def tsort : ∀ r : R *, l : L, t : *, u : U.
+    ⟨l ▹ t⟩ ≲(C) r, LE t ⇒ List (Π(u) r) → ⌊l⌋ → Bool → List (Π(u) r) =
+  \tb l asc.
+    if asc then
+      sortBy (\r0 r1. le (prj (r0 : Π(C) r))/l (prj (r1 : Π(C) r))/l) tb
+    else
+      sortBy (\r0 r1. le (prj (r1 : Π(C) r))/l (prj (r0 : Π(C) r))/l) tb
diff --git a/examples/b2t2/properties/header.tt b/examples/b2t2/properties/header.tt
new file mode 100644
index 0000000..2770f12
--- /dev/null
+++ b/examples/b2t2/properties/header.tt
@@ -0,0 +1,2 @@
+def header : ∀ r : R *, u : U. List (Π(u) r) → Labels u r =
+  \_. ind (Labels u) r (\l acc. acc ++ {l ▹ {}}) {}
diff --git a/examples/b2t2/properties/ncols.tt b/examples/b2t2/properties/ncols.tt
new file mode 100644
index 0000000..185537f
--- /dev/null
+++ b/examples/b2t2/properties/ncols.tt
@@ -0,0 +1,2 @@
+def ncols : ∀ r : R *. List (Π(C) r) → Int =
+  ind (Const Int) r (\_ acc. acc + 1) 0
diff --git a/examples/b2t2/properties/nrows.tt b/examples/b2t2/properties/nrows.tt
new file mode 100644
index 0000000..fc9f034
--- /dev/null
+++ b/examples/b2t2/properties/nrows.tt
@@ -0,0 +1 @@
+def nrows : ∀ r : R *, u : U. List (Π(u) r) → Int = length
diff --git a/examples/b2t2/subtable/distinct.tt b/examples/b2t2/subtable/distinct.tt
new file mode 100644
index 0000000..936ff4c
--- /dev/null
+++ b/examples/b2t2/subtable/distinct.tt
@@ -0,0 +1,2 @@
+def distinct : ∀ r : R *, u : U. All Eq r ⇒ List (Π(u) r) → List (Π(u) r) =
+  unique
diff --git a/examples/b2t2/subtable/dropColumn.tt b/examples/b2t2/subtable/dropColumn.tt
new file mode 100644
index 0000000..406dd13
--- /dev/null
+++ b/examples/b2t2/subtable/dropColumn.tt
@@ -0,0 +1,2 @@
+def dropColumn : ∀ r r' : R *, l : L, t : *. r' ⊙(C) ⟨l ▹ t⟩ ~ r ⇒
+    List (Π(C) r) → ⌊l⌋ → List (Π(C) r') = \tb _. map (\r. prj r) tb
diff --git a/examples/b2t2/subtable/dropColumns.tt b/examples/b2t2/subtable/dropColumns.tt
new file mode 100644
index 0000000..bb36621
--- /dev/null
+++ b/examples/b2t2/subtable/dropColumns.tt
@@ -0,0 +1,3 @@
+def dropColumns : ∀ r rd r' : R *, u : U. r' ⊙(C) rd ~ r ⇒
+    List (Π(u) r) → LabelSet rd → List (Π(u) r') =
+  \tb _. map (\r. orderₚ r' (prj (r : Π(C) r))) tb
diff --git a/examples/b2t2/subtable/head.tt b/examples/b2t2/subtable/head.tt
new file mode 100644
index 0000000..84c7249
--- /dev/null
+++ b/examples/b2t2/subtable/head.tt
@@ -0,0 +1,5 @@
+def head : ∀ r : R *, u : U. List (Π(u) r) → Int → List (Π(u) r) =
+  \tb i. if i >= 0 then
+    take (0 - i) tb
+  else
+    drop (length tb + i) tb
diff --git a/examples/b2t2/subtable/selectColumns3.tt b/examples/b2t2/subtable/selectColumns3.tt
new file mode 100644
index 0000000..b02edf5
--- /dev/null
+++ b/examples/b2t2/subtable/selectColumns3.tt
@@ -0,0 +1,3 @@
+def selectColumns : ∀ r r' : R *, u : U. r' ≲(C) r ⇒
+    List (Π(C) r) → LabelList r' → List (Π(N) r') =
+  \tb _. map (\r. orderₚ r' (prj r)) tb
diff --git a/examples/b2t2/subtable/selectRows1.tt b/examples/b2t2/subtable/selectRows1.tt
new file mode 100644
index 0000000..d9cfda5
--- /dev/null
+++ b/examples/b2t2/subtable/selectRows1.tt
@@ -0,0 +1,2 @@
+def selectRows1 : ∀ r : R *, l : L, t : *, u : U.
+    List (Π(u) r) → List Int → List (Π(u) r) = \tb. map (get tb)
diff --git a/examples/b2t2/subtable/selectRows2.tt b/examples/b2t2/subtable/selectRows2.tt
new file mode 100644
index 0000000..c5e8814
--- /dev/null
+++ b/examples/b2t2/subtable/selectRows2.tt
@@ -0,0 +1,3 @@
+def selectRows2 :
+  ∀ r : R *, l : L, t : *, u : U. List (Π(u) r) → List Bool → List (Π(u) r) =
+  \tb bs. filter (\x. x) (zip (\r b. if b then some r else none) tb bs)
diff --git a/examples/b2t2/subtable/tfilter.tt b/examples/b2t2/subtable/tfilter.tt
new file mode 100644
index 0000000..88df32e
--- /dev/null
+++ b/examples/b2t2/subtable/tfilter.tt
@@ -0,0 +1,2 @@
+def tfilter : ∀ r : R *, u : U.
+  List (Π(u) r) → (Π(u) r → Bool) → List (Π(u) r) = flip filter
diff --git a/examples/b2t2/utilities/find.tt b/examples/b2t2/utilities/find.tt
new file mode 100644
index 0000000..77baa0a
--- /dev/null
+++ b/examples/b2t2/utilities/find.tt
@@ -0,0 +1,2 @@
+def find : ∀ r : R *. All Eq r ⇒ List (Π(C) r) → Π(C) r → Option Int =
+  \tb r. foldIdx (\r' i. orElse (if rowEq r r' then some i else none)) none tb
diff --git a/examples/b2t2/utilities/flatten.tt b/examples/b2t2/utilities/flatten.tt
new file mode 100644
index 0000000..9be04f6
--- /dev/null
+++ b/examples/b2t2/utilities/flatten.tt
@@ -0,0 +1,14 @@
+def flatten :
+  ∀ r rs rr r' : R *. Lift (\a : *. List a) rs ⊙(C) rr ~ r, rs ⊙(C) rr ~ r' ⇒
+    List (Π(C) r) → LabelSet rs → List (Π(C) r') =
+  \tb _. lflatten (map (\r.
+    let s : Π(C) (Lift List rs) = prj r in
+    let rr : Π(C) rr = prj r in
+    let s' = ind (\a : R *. Σ(N) ⟨'many' ▹ List (Π(C) rs), 'one' ▹ Π(C) rs⟩) rs
+      (\l.
+        (\x. ['many' ▹ map (\y. x/'one' ++ {l ▹ y}) s/l]) ▿
+          (\xs. ['many' ▹ zip (\v r'. r' ++ {l ▹ v}) s/l xs/'many'])
+      ) ['one' ▹ {}]
+    in
+    (\x. singleton x/'one') ▿ (\x. x/'many') s' ++ rr
+  ) tb)
diff --git a/examples/b2t2/utilities/groupByRetentive.tt b/examples/b2t2/utilities/groupByRetentive.tt
new file mode 100644
index 0000000..9259734
--- /dev/null
+++ b/examples/b2t2/utilities/groupByRetentive.tt
@@ -0,0 +1,5 @@
+def groupByRetentive : ∀ r : R *, l : L, t : *, u : U. Eq t, ⟨l ▹ t⟩ ≲(C) r ⇒
+    List (Π(u) r) → ⌊l⌋ → ⟨'key' ▹ t, 'groups' ▹ List (Π(u) r)⟩ =
+  \tb l.
+    let keys = unique (map (\r. (prj r)/l) tb) in
+	map (\k. {'key' ▹ k, 'groups' ▹ filter (\r. eq (prj r)/l k) tb}) keys
diff --git a/examples/b2t2/utilities/groupBySubtractive.tt b/examples/b2t2/utilities/groupBySubtractive.tt
new file mode 100644
index 0000000..1b384e5
--- /dev/null
+++ b/examples/b2t2/utilities/groupBySubtractive.tt
@@ -0,0 +1,7 @@
+def groupBySubtractive : ∀ r r' : R *, l : L, t : *. Eq t, r' ⊙(C) ⟨l ▹ t⟩ ~ r ⇒
+    List (Π(C) r) → ⌊l⌋ → ⟨'key' ▹ t, 'groups' ▹ List (Π(C) r')⟩ =
+  \tb l.
+    let keys = unique (map (\r. (prj r)/l) tb) in
+	map (\k.
+	  {'key' ▹ k, 'groups' ▹ map (\r. prj r) (filter (\r. eq (prj r)/l k) tb)}
+	) keys
diff --git a/examples/b2t2/utilities/groupJoin.tt b/examples/b2t2/utilities/groupJoin.tt
new file mode 100644
index 0000000..d7d9382
--- /dev/null
+++ b/examples/b2t2/utilities/groupJoin.tt
@@ -0,0 +1,8 @@
+def groupJoin : ∀ r0 r1 r : R *, t : *, u0 u1 u : U. Eq t ⇒
+    List (Π(u0) r0) → List (Π(u1) r1) → (Π(u0) r0 → t) → (Π(u1) r1 → t) →
+    (Π(u0) r0 → List (Π(u1) r1) → Π(u) r) → List (Π(u) r) =
+  \tb0 tb1 k0f k1f af.
+    map (\r0.
+      let k0 : t = k0f r0 in
+      af r0 (filter (\r1. eq k0 (k1f r1)) tb1)
+    ) tb0
diff --git a/examples/b2t2/utilities/join.tt b/examples/b2t2/utilities/join.tt
new file mode 100644
index 0000000..d0e7838
--- /dev/null
+++ b/examples/b2t2/utilities/join.tt
@@ -0,0 +1,8 @@
+def join : ∀ r0 r1 r : R *, t : *, u0 u1 u : U. Eq t ⇒
+    List (Π(u0) r0) → List (Π(u1) r1) → (Π(u0) r0 → t) → (Π(u1) r1 → t) →
+    (Π(u0) r0 → Π(u1) r1 → Π(u) r) → List (Π(u) r) =
+  \tb0 tb1 k0f k1f cf.
+    map (\r0.
+      let k0 : t = k0f r0 in
+      filterMap (\r1. if eq k0 (k1f r1) then some (cf r0 r1) else none) tb1
+    ) tb0
diff --git a/examples/b2t2/utilities/renameColumn.tt b/examples/b2t2/utilities/renameColumn.tt
new file mode 100644
index 0000000..d2dbb9f
--- /dev/null
+++ b/examples/b2t2/utilities/renameColumn.tt
@@ -0,0 +1,4 @@
+def renameColumn :
+  ∀ r rr r' : R *, l l' : L, t : *. rr ⊙(C) ⟨l ▹ t⟩ ~ r, rr ⊙(C) ⟨l' ▹ t⟩ ~ r' ⇒
+    List (Π(C) r) → ⌊l⌋ → ⌊l'⌋ → List (Π(C) r') =
+  \tb l l'. map (\r. prj r ++ {l' ▹ (prj r)/l}) tb
diff --git a/examples/b2t2/utilities/select.tt b/examples/b2t2/utilities/select.tt
new file mode 100644
index 0000000..28a1139
--- /dev/null
+++ b/examples/b2t2/utilities/select.tt
@@ -0,0 +1,2 @@
+def select : ∀ r r' : R *, u u' : U.
+    List (Π(u) r) → (Π(u) r → Int → Π(u') r') → List (Π(u') r') = flip mapIdx
diff --git a/examples/b2t2/utilities/selectMany.tt b/examples/b2t2/utilities/selectMany.tt
new file mode 100644
index 0000000..079d2ff
--- /dev/null
+++ b/examples/b2t2/utilities/selectMany.tt
@@ -0,0 +1,8 @@
+def selectMany : ∀ r r' r'' : R *, u u' u'' : U. List (Π(u) r) →
+    (Π(u) r → Int → List (Π(u') r')) → (Π(u) r → Π(u') r' → Π(u'') r'') →
+    List (Π(u'') r'') =
+  \tb pf rf.
+    let pairs : List (Π(N) ⟨'orig' ▹ Π(u) r, 'prj' ▹ Π(u') r'⟩) =
+      flatten (mapIdx (\r idx. map (\p. {'orig' ▹ r, 'prj' ▹ p}) (pf r idx)) tb)
+    in
+    map (\op. rf (prj op)/'orig' (prj op)/'prj') pairs
diff --git a/examples/b2t2/utilities/transformColumn.tt b/examples/b2t2/utilities/transformColumn.tt
new file mode 100644
index 0000000..60fc123
--- /dev/null
+++ b/examples/b2t2/utilities/transformColumn.tt
@@ -0,0 +1,4 @@
+def transformColumn :
+  ∀ r rr r' : R *, l : L, t t' : *. rr ⊙(C) ⟨l ▹ t⟩ ~ r, rr ⊙(C) ⟨l ▹ t'⟩ ~ r' ⇒
+    List (Π(C) r) → ⌊l⌋ → (t → t') → List (Π(C) r') =
+  \tb l f. map (\r. prj r ++ {l ▹ f (prj r)/l}) tb
diff --git a/examples/b2t2/utilities/update.tt b/examples/b2t2/utilities/update.tt
new file mode 100644
index 0000000..ac29865
--- /dev/null
+++ b/examples/b2t2/utilities/update.tt
@@ -0,0 +1,4 @@
+def update : ∀ r rs rd rn r' : R *, u : U.
+    rs ⊙(C) rd ~ r, rs ⊙(C) rn ~ r', LabelsMatch rs rn ⇒
+    List (Π(u) r) → (Π(u) r → Π(C) rn) → List (Π(C) r') =
+  \tb f. map (\r. (prj r : Π(C) rs) ++ (f r)) tb
diff --git a/examples/core/And.tt b/examples/core/And.tt
new file mode 100644
index 0000000..f963e05
--- /dev/null
+++ b/examples/core/And.tt
@@ -0,0 +1 @@
+type And = \r : R C. All (\c : C. c) r
diff --git a/examples/core/Bool.tt b/examples/core/Bool.tt
new file mode 100644
index 0000000..e1c2757
--- /dev/null
+++ b/examples/core/Bool.tt
@@ -0,0 +1,14 @@
+type Bool = Σ(N) ⟨'false' ▹ Unit, 'true' ▹ Unit⟩
+
+def false : Bool = inj ['false' ▹ {}]
+
+def true : Bool = inj ['true' ▹ {}]
+
+def not : Bool → Bool =
+  ((\_. true) : Σ(N) ⟨'false' ▹ Unit⟩ → Bool) ▿ (\_. false)
+
+def and : Bool → Bool → Bool =
+  \x. ((\_. false) : Σ(N) ⟨'false' ▹ Unit⟩ → Bool) ▿ (\_. x)
+
+def or : Bool → Bool → Bool =
+  \x. ((\_. x) : Σ(N) ⟨'false' ▹ Unit⟩ → Bool) ▿ (\_. false)
diff --git a/examples/core/Const.tt b/examples/core/Const.tt
new file mode 100644
index 0000000..82af912
--- /dev/null
+++ b/examples/core/Const.tt
@@ -0,0 +1 @@
+type Const = \a b : *. b
diff --git a/examples/core/Eq.tt b/examples/core/Eq.tt
new file mode 100644
index 0000000..99cba09
--- /dev/null
+++ b/examples/core/Eq.tt
@@ -0,0 +1,8 @@
+class Eq a : * where
+  eq : a → a → Bool
+
+instance Eq Int where
+  eq = \x y. x == y
+
+def rowEq : ∀ r : R *. All Eq r ⇒ Π(C) r → Π(C) r → Bool =
+  \x y. ind (\_ : R *. Bool) r (\l acc. and acc (eq (prj x)/l (prj y)/l)) true
diff --git a/examples/core/LE.tt b/examples/core/LE.tt
new file mode 100644
index 0000000..75e82f5
--- /dev/null
+++ b/examples/core/LE.tt
@@ -0,0 +1,5 @@
+class LE a : * where
+  le : a → a → Bool
+
+instance LE Int where
+  le = \x y. x <= y
diff --git a/examples/core/Labels.tt b/examples/core/Labels.tt
new file mode 100644
index 0000000..e41e037
--- /dev/null
+++ b/examples/core/Labels.tt
@@ -0,0 +1,5 @@
+type Labels = \u : U, r : R *. Σ(u) (Lift (Const Unit) r)
+
+type LabelSet = Labels C
+
+type LabelList = Labels N
diff --git a/examples/core/LabelsMatch.tt b/examples/core/LabelsMatch.tt
new file mode 100644
index 0000000..64275a8
--- /dev/null
+++ b/examples/core/LabelsMatch.tt
@@ -0,0 +1,4 @@
+def LabelsMatch = \r0 r1 : R *. And ⟨
+    Lift (\_ : *. ⟨ : * ⟩) r0 ≲(C) Lift (\_ : *. ⟨ : * ⟩) r1,
+    Lift (\_ : *. ⟨ : * ⟩) r1 ≲(C) Lift (\_ : *. ⟨ : * ⟩) r0
+  ⟩
diff --git a/examples/core/List.tt b/examples/core/List.tt
new file mode 100644
index 0000000..62421dd
--- /dev/null
+++ b/examples/core/List.tt
@@ -0,0 +1,68 @@
+def append : ∀ t : *. List t → List t → List t = fold (\x acc. x :: acc)
+
+def contains : ∀ t : *. Eq t ⇒ List t → t → Bool =
+  \xs x. fold (\x' acc. or acc (eq x x')) false xs
+
+def filter : ∀ t : *. (t → Bool) → List t → List t =
+  \f. fold (\x acc. if f x then x :: acc else acc) nil
+
+def filterMap : ∀ t t' : *. (t → Option t') → List t → List t' =
+  \f. fold (\x acc. (\y. y/'some' :: acc) ▿ (\_. acc) (f x)) nil
+
+def foldIdx : ∀ t t' : *. (t → Int → t') → t' → List t = \f init xs.
+  (fold
+    (\x acc. {'i' ▹ (prj acc)/'i' + 1, 'v' ▹ f x (prj acc)/'i' (prj acc)/'v'})
+    {'i' ▹ 0, 'v' ▹ init} xs)/'v'
+
+def get : ∀ t : *. List t → Int → t =
+  \xs i.
+    if i < 0 then
+      throw "get of negative index"
+    else
+      let acc = fold (\x.
+        (\i. if i/'idx' == 0 then inj ['val' ▹ x] else ['idx' ▹ i/'idx' - 1]) ▿
+          (\y. y)) (inj ['idx' ▹ i]) xs
+      in
+      (\x. x/'val') ▿ (\_. throw "index out of range") acc
+
+def lcount : ∀ t : *. (t → Bool) → List t → Int =
+  \xs f. fold (\x acc. if f x then acc + 1 else acc) 0 xs
+
+def length : ∀ t : *. List t → Int = fold (\_ acc. acc + 1) 0
+
+def lflatten : ∀ t : *. List (List t) → List t = fold append nil
+
+def drop : ∀ t : *. Int → List t → List t = \i xs.
+  fold (\x acc. if (length xs - length acc) < i then x :: acc else acc) nil xs
+
+def map : ∀ t t' : *. (t → t') → List t → List t' =
+  \f. fold (\x acc. f x :: acc) nil
+
+def mapIdx : ∀ t t' : *. (t → Int → t') → List t → List t' =
+  \f. foldIdx (\x i acc. f x i :: acc) nil
+
+def max : List Int → Int = fold (\x acc. if x > acc then x else acc) minInt
+
+def min : List Int → Int = fold (\x acc. if x < acc then x else acc) maxInt
+
+def singleton : ∀ t : *. t → List t = \x. x :: nil
+
+def snoc : ∀ t : *. List t → t → List t = \xs x. append xs (singleton x)
+
+def sortBy : ∀ t : *. List t → (t → t → Bool) → List t =
+  \xs lt.
+    let merge : t → List t → List t =
+      -- TODO: Finish this
+      \new rest. fold (\other acc. (((\_. 5) : ⟨'ipr' ▹ List _⟩) ▿ (5)) ) rest
+        ['ipr' ▹ nil]
+    in
+    fold merge xs nil
+
+def take : ∀ t : *. Int → List t → List t =
+  \i. fold (\x acc. if length acc < i then x :: acc else acc) nil
+
+def unique : ∀ t : *. Eq t ⇒ List t → List t =
+  fold (\x acc. if contains acc x then acc else x :: acc) nil
+
+def zip : ∀ t t' t'' : *. (t' → t'' → t) → List t' → List t'' → List t =
+  \f ll lr. map (\i. f (get ll i) (get lr i)) range (length ll)
diff --git a/examples/core/Option.tt b/examples/core/Option.tt
new file mode 100644
index 0000000..1c66ce2
--- /dev/null
+++ b/examples/core/Option.tt
@@ -0,0 +1,22 @@
+type Option = \a : *. Σ(N) ⟨'some' ▹ a, 'none' ▹ Unit⟩
+
+def some : ∀ t : *. t → Option t = \x. inj ['some' ▹ x]
+
+def none : ∀ t : *. Option t = inj ['none' ▹ {}]
+
+def isSome : ∀ t : *. Option t → Bool =
+  ((\_. false) : Σ(N) ⟨'none' ▹ Unit⟩) ▿ (\_. true)
+
+def isNone : ∀ t : *. Option t → Bool = \o. not (isSome o)
+
+def bind : ∀ t t' : *. (t → Option t') → Option t → Option t' =
+  \f. (\x. f x/'some') ▿ (\_. none)
+
+def ogetD : ∀ t t' : *. Option t → t → t =
+  \o default. (\x. x/'some') ▿ (\_. default) o
+
+def omap : ∀ t t' : *. (t → t') → Option t → Option t' =
+  \f. bind (\x. some (f x))
+
+def orElse : ∀ t : *. Option t → Option t → Option t =
+  \x y. ((\_. y) : Σ(N) ⟨'none' ▹ Unit⟩) ▿ (\_. x) x
diff --git a/examples/core/Unit.tt b/examples/core/Unit.tt
new file mode 100644
index 0000000..c959d02
--- /dev/null
+++ b/examples/core/Unit.tt
@@ -0,0 +1 @@
+type Unit = Π(N) ⟨ : * ⟩
diff --git a/examples/core/flip.tt b/examples/core/flip.tt
new file mode 100644
index 0000000..3db928d
--- /dev/null
+++ b/examples/core/flip.tt
@@ -0,0 +1 @@
+def flip : ∀ t t' t'' : *. (t → t' → t'') → t' → t → t'' = \f y x. f x y
diff --git a/examples/core/is.tt b/examples/core/is.tt
new file mode 100644
index 0000000..bd13cbe
--- /dev/null
+++ b/examples/core/is.tt
@@ -0,0 +1,3 @@
+def is : ∀ r r' : R *, l : L, t : *, u : U.
+    ⟨l ▹ t⟩ ⊙(C) r' ~ r ⇒ ⌊l⌋ → Σ(u) r → Bool =
+  \_. ((\_. true) : Σ(C) ⟨l ▹ t⟩ → Bool) ▿ ((\_. false) : Σ(C) r' → Bool)