diff --git a/src/catdata/cql/EDTest.java b/src/catdata/cql/EDTest.java
new file mode 100644
index 0000000..270f87e
--- /dev/null
+++ b/src/catdata/cql/EDTest.java
@@ -0,0 +1,573 @@
+package catdata.cql;
+
+import static org.junit.jupiter.api.Assertions.assertDoesNotThrow;
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertNotEquals;
+import static org.junit.jupiter.api.Assertions.assertSame;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+import catdata.Chc;
+import catdata.Pair;
+import catdata.cql.Collage.CCollage;
+import catdata.cql.exp.Att;
+import catdata.cql.exp.Fk;
+import catdata.cql.exp.Sym;
+import org.junit.jupiter.api.Nested;
+import org.junit.jupiter.api.Test;
+
+class EDTest {
+
+  private static final String EN = "Employee";
+  private static final String DEPT = "Department";
+  private static final String TY = "Varchar";
+
+  private static AqlOptions ops() {
+    return AqlOptions.initialOptions;
+  }
+
+  /**
+   * A two-entity acyclic schema over {@link SqlTypeSide}: Employee.worksIn : Employee -> Department,
+   * with a Varchar attribute on each. Built once and shared; constructing a typeside spins up the
+   * JS engine and a prover, which is slow.
+   */
+  private static Schema<String, String, Sym, Fk, Att> schema() {
+    return SchemaHolder.INSTANCE;
+  }
+
+  private static final class SchemaHolder {
+    private static final Schema<String, String, Sym, Fk, Att> INSTANCE = build();
+
+    private static Schema<String, String, Sym, Fk, Att> build() {
+      TypeSide<String, Sym> ts = SqlTypeSide.SqlTypeSide(ops());
+      Collage<String, String, Sym, Fk, Att, Void, Void> col = new CCollage<>();
+      col.tys().addAll(ts.tys);
+      col.syms().putAll(ts.syms);
+      col.java_tys().putAll(ts.js.java_tys);
+      col.getEns().add(EN);
+      col.getEns().add(DEPT);
+      col.atts().put(Att.Att(EN, "name"), new Pair<>(EN, TY));
+      col.atts().put(Att.Att(DEPT, "label"), new Pair<>(DEPT, TY));
+      col.fks().put(Fk.Fk(EN, "worksIn"), new Pair<>(EN, DEPT));
+      return new Schema<>(ts, col, ops());
+    }
+  }
+
+  private static Chc<String, String> dept() {
+    return Chc.inRight(DEPT);
+  }
+
+  /** An entity-sorted variable, i.e. one ranging over rows rather than over type values. */
+  private static Chc<String, String> en() {
+    return Chc.inRight(EN);
+  }
+
+  /** A type-sorted variable, i.e. one ranging over the typeside. */
+  private static Chc<String, String> ty() {
+    return Chc.inLeft(TY);
+  }
+
+  private static Term<String, String, Sym, Fk, Att, Void, Void> v(String name) {
+    return Term.Var(name);
+  }
+
+  private static Map<String, Chc<String, String>> ctx(String var, Chc<String, String> sort) {
+    Map<String, Chc<String, String>> m = new HashMap<>();
+    m.put(var, sort);
+    return m;
+  }
+
+  @SafeVarargs
+  private static Set<Pair<
+          Term<String, String, Sym, Fk, Att, Void, Void>,
+          Term<String, String, Sym, Fk, Att, Void, Void>>>
+      eqs(
+          Pair<
+                  Term<String, String, Sym, Fk, Att, Void, Void>,
+                  Term<String, String, Sym, Fk, Att, Void, Void>>...
+              ps) {
+    Set<Pair<
+            Term<String, String, Sym, Fk, Att, Void, Void>,
+            Term<String, String, Sym, Fk, Att, Void, Void>>>
+        s = new HashSet<>();
+    Collections.addAll(s, ps);
+    return s;
+  }
+
+  /** The trivial ED: no hypotheses, no conclusion. */
+  private static ED empty() {
+    return new ED(
+        Collections.emptyMap(),
+        Collections.emptyMap(),
+        Collections.emptySet(),
+        Collections.emptySet(),
+        false,
+        ops());
+  }
+
+  /** forall a:Employee -> exists e:Employee. */
+  private static ED forallExists() {
+    return new ED(ctx("a", en()), ctx("e", en()), eqs(), eqs(), false, ops());
+  }
+
+  @Nested
+  class Construction {
+
+    @Test
+    void copiesItsInputsDefensively() {
+      Map<String, Chc<String, String>> as = ctx("a", en());
+      Map<String, Chc<String, String>> es = ctx("e", en());
+      Set<Pair<
+              Term<String, String, Sym, Fk, Att, Void, Void>,
+              Term<String, String, Sym, Fk, Att, Void, Void>>>
+          awh = eqs(new Pair<>(v("a"), v("a")));
+      Set<Pair<
+              Term<String, String, Sym, Fk, Att, Void, Void>,
+              Term<String, String, Sym, Fk, Att, Void, Void>>>
+          ewh = eqs(new Pair<>(v("e"), v("e")));
+
+      ED ed = new ED(as, es, awh, ewh, false, ops());
+
+      as.put("intruder", en());
+      es.put("intruder", en());
+      awh.clear();
+      ewh.clear();
+
+      assertEquals(1, ed.As.size(), "As must not alias the caller's map");
+      assertEquals(1, ed.Es.size(), "Es must not alias the caller's map");
+      assertEquals(1, ed.Awh.size(), "Awh must not alias the caller's set");
+      assertEquals(1, ed.Ewh.size(), "Ewh must not alias the caller's set");
+    }
+
+    @Test
+    void retainsTheDeclaredContexts() {
+      ED ed = forallExists();
+      assertEquals(en(), ed.As.get("a"));
+      assertEquals(en(), ed.Es.get("e"));
+      assertTrue(!ed.isUnique);
+    }
+
+    @Test
+    void uniqueWithNoExistentialsIsAnAnomaly() {
+      // "exists unique" with an empty exists clause is not expressible; Util.anomaly rejects it.
+      RuntimeException e =
+          assertThrows(
+              RuntimeException.class,
+              () ->
+                  new ED(
+                      ctx("a", en()),
+                      Collections.emptyMap(),
+                      Collections.emptySet(),
+                      Collections.emptySet(),
+                      true,
+                      ops()));
+      assertTrue(e.getMessage().contains("Anomaly"));
+    }
+
+    @Test
+    void uniqueWithExistentialsIsAccepted() {
+      ED ed = new ED(ctx("a", en()), ctx("e", en()), eqs(), eqs(), true, ops());
+      assertTrue(ed.isUnique);
+    }
+
+    @Test
+    void acceptsTypeSortedVariables() {
+      ED ed = new ED(ctx("x", ty()), ctx("y", ty()), eqs(), eqs(), false, ops());
+      assertTrue(ed.As.get("x").left, "type-sorted variables land on the left of the Chc");
+      assertTrue(ed.Es.get("y").left);
+    }
+  }
+
+  @Nested
+  class ToString {
+
+    @Test
+    void theTrivialEdIsJustTheImplicationArrow() {
+      assertEquals("->\n", empty().toString());
+    }
+
+    @Test
+    void rendersTheForallClause() {
+      ED ed = new ED(ctx("a", en()), Collections.emptyMap(), eqs(), eqs(), false, ops());
+      String s = ed.toString();
+      assertTrue(s.startsWith("\tforall"), s);
+      assertTrue(s.contains("a:" + EN), s);
+      assertTrue(s.contains("->"), s);
+    }
+
+    @Test
+    void rendersTheExistsClause() {
+      String s = forallExists().toString();
+      assertTrue(s.contains("\texists"), s);
+      assertTrue(s.contains("e:" + EN), s);
+    }
+
+    @Test
+    void marksUniqueExistentials() {
+      ED plain = new ED(ctx("a", en()), ctx("e", en()), eqs(), eqs(), false, ops());
+      ED uniq = new ED(ctx("a", en()), ctx("e", en()), eqs(), eqs(), true, ops());
+      assertTrue(!plain.toString().contains("exists unique"), plain.toString());
+      assertTrue(uniq.toString().contains("exists unique"), uniq.toString());
+    }
+
+    @Test
+    void rendersBothWhereClauses() {
+      ED ed =
+          new ED(
+              ctx("a", en()),
+              ctx("e", en()),
+              eqs(new Pair<>(v("a"), v("a"))),
+              eqs(new Pair<>(v("e"), v("e"))),
+              false,
+              ops());
+      String s = ed.toString();
+      assertEquals(2, s.split("\twhere", -1).length - 1, "one where per clause: " + s);
+      assertTrue(s.contains("a = a"), s);
+      assertTrue(s.contains("e = e"), s);
+    }
+
+    @Test
+    void putsTheForallClauseBeforeTheArrowAndTheExistsClauseAfter() {
+      ED ed =
+          new ED(
+              ctx("a", en()),
+              ctx("e", en()),
+              eqs(new Pair<>(v("a"), v("a"))),
+              eqs(new Pair<>(v("e"), v("e"))),
+              false,
+              ops());
+      String s = ed.toString();
+      int arrow = s.indexOf("->");
+      assertTrue(s.indexOf("\tforall") < arrow, s);
+      assertTrue(s.indexOf("\texists") > arrow, s);
+      assertTrue(s.indexOf("a = a") < arrow, "the forall where-clause precedes the arrow: " + s);
+      assertTrue(s.indexOf("e = e") > arrow, "the exists where-clause follows the arrow: " + s);
+    }
+
+    @Test
+    void omitsEmptyClauses() {
+      String s = forallExists().toString();
+      assertTrue(!s.contains("\twhere"), "no where clause when both are empty: " + s);
+    }
+  }
+
+  @Nested
+  class EqualsAndHashCode {
+
+    @Test
+    void isReflexive() {
+      ED ed = forallExists();
+      assertEquals(ed, ed);
+    }
+
+    @Test
+    void isSymmetricOnEqualValues() {
+      ED a = forallExists();
+      ED b = forallExists();
+      assertEquals(a, b);
+      assertEquals(b, a);
+      assertEquals(a.hashCode(), b.hashCode(), "equal EDs must agree on hashCode");
+    }
+
+    @Test
+    void rejectsNullAndForeignTypes() {
+      ED ed = forallExists();
+      assertNotEquals(null, ed);
+      assertNotEquals(ed, new Object());
+      assertNotEquals("not an ED", ed);
+    }
+
+    @Test
+    void distinguishesOnTheForallContext() {
+      ED a = new ED(ctx("a", en()), ctx("e", en()), eqs(), eqs(), false, ops());
+      ED b = new ED(ctx("b", en()), ctx("e", en()), eqs(), eqs(), false, ops());
+      assertNotEquals(a, b);
+    }
+
+    @Test
+    void distinguishesOnTheExistsContext() {
+      ED a = new ED(ctx("a", en()), ctx("e", en()), eqs(), eqs(), false, ops());
+      ED b = new ED(ctx("a", en()), ctx("f", en()), eqs(), eqs(), false, ops());
+      assertNotEquals(a, b);
+    }
+
+    @Test
+    void distinguishesOnTheForallWhereClause() {
+      ED a =
+          new ED(
+              ctx("a", en()), ctx("e", en()), eqs(new Pair<>(v("a"), v("a"))), eqs(), false, ops());
+      ED b = new ED(ctx("a", en()), ctx("e", en()), eqs(), eqs(), false, ops());
+      assertNotEquals(a, b);
+    }
+
+    @Test
+    void distinguishesOnTheExistsWhereClause() {
+      ED a =
+          new ED(
+              ctx("a", en()), ctx("e", en()), eqs(), eqs(new Pair<>(v("e"), v("e"))), false, ops());
+      ED b = new ED(ctx("a", en()), ctx("e", en()), eqs(), eqs(), false, ops());
+      assertNotEquals(a, b);
+    }
+
+    @Test
+    void distinguishesOnUniqueness() {
+      ED a = new ED(ctx("a", en()), ctx("e", en()), eqs(), eqs(), false, ops());
+      ED b = new ED(ctx("a", en()), ctx("e", en()), eqs(), eqs(), true, ops());
+      assertNotEquals(a, b);
+      assertNotEquals(a.hashCode(), b.hashCode(), "isUnique participates in hashCode");
+    }
+
+    @Test
+    void ignoresOptions() {
+      // options is deliberately absent from both equals and hashCode: two EDs asserting the same
+      // sentence are the same constraint regardless of the prover settings used to check it.
+      ED a = new ED(ctx("a", en()), ctx("e", en()), eqs(), eqs(), false, AqlOptions.initialOptions);
+      ED b =
+          new ED(
+              ctx("a", en()),
+              ctx("e", en()),
+              eqs(),
+              eqs(),
+              false,
+              new AqlOptions(Collections.emptyMap(), AqlOptions.initialOptions));
+      assertEquals(a, b);
+      assertEquals(a.hashCode(), b.hashCode());
+    }
+  }
+
+  @Nested
+  class Unfreeze {
+
+    private final ED ed = empty();
+
+    @Test
+    void turnsGeneratorsIntoPrefixedVariables() {
+      assertEquals(v("Ag"), ed.unfreeze("A", Term.Gen("g")));
+    }
+
+    @Test
+    void turnsSkolemsIntoPrefixedVariables() {
+      assertEquals(v("Es"), ed.unfreeze("E", Term.Sk("s")));
+    }
+
+    @Test
+    void distinguishesGeneratorsAndSkolemsOnlyByName() {
+      // Both collapse to variables, so a gen and an sk sharing a name unfreeze identically.
+      assertEquals(ed.unfreeze("A", Term.Gen("x")), ed.unfreeze("A", Term.Sk("x")));
+    }
+
+    @Test
+    void recursesThroughForeignKeys() {
+      Fk fk = Fk.Fk(EN, "manager");
+      Term<String, String, Sym, Fk, Att, String, String> t = Term.Fk(fk, Term.Gen("g"));
+      assertEquals(Term.Fk(fk, v("Ag")), ed.unfreeze("A", t));
+    }
+
+    @Test
+    void recursesThroughAttributes() {
+      Att att = Att.Att(EN, "name");
+      Term<String, String, Sym, Fk, Att, String, String> t = Term.Att(att, Term.Gen("g"));
+      assertEquals(Term.Att(att, v("Ag")), ed.unfreeze("A", t));
+    }
+
+    @Test
+    void recursesThroughNestedForeignKeys() {
+      Fk fk = Fk.Fk(EN, "manager");
+      Term<String, String, Sym, Fk, Att, String, String> t = Term.Fk(fk, Term.Fk(fk, Term.Gen("g")));
+      assertEquals(Term.Fk(fk, Term.Fk(fk, v("Ag"))), ed.unfreeze("A", t));
+    }
+
+    @Test
+    void rejectsTermsThatAreAlreadyVariables() {
+      // unfreeze is the inverse of freeze, so its input must not contain variables already.
+      Term<String, String, Sym, Fk, Att, String, String> t = Term.Var("x");
+      RuntimeException e = assertThrows(RuntimeException.class, () -> ed.unfreeze("A", t));
+      assertTrue(e.getMessage().contains("Anomaly"), e.getMessage());
+    }
+
+    @Test
+    void appliesThePrefixVerbatim() {
+      assertEquals(v("g"), ed.unfreeze("", Term.Gen("g")));
+      assertEquals(v("prefix_g"), ed.unfreeze("prefix_", Term.Gen("g")));
+    }
+  }
+
+  @Nested
+  class Constants {
+
+    @Test
+    void theUnitForeignKeyPointsFromBackToFront() {
+      assertEquals("front", ED.FRONT);
+      assertEquals("back", ED.BACK);
+      assertEquals(ED.BACK, ED.UNIT.en, "unit is declared on the back entity");
+      assertEquals("unit", ED.UNIT.str);
+    }
+  }
+
+  /**
+   * Tests for the methods that need a real schema to interpret the ED against. The schema is
+   * deliberately acyclic: a cyclic one with generators and no equations trips the divergence
+   * check in {@link catdata.cql.fdm.InitialAlgebra}.
+   */
+  @Nested
+  class WithSchema {
+
+    private final Schema<String, String, Sym, Fk, Att> sch = schema();
+    private final Att name = Att.Att(EN, "name");
+    private final Att label = Att.Att(DEPT, "label");
+
+    /** forall a:Employee -> exists e:Department. */
+    private ED simple() {
+      return new ED(ctx("a", en()), ctx("e", dept()), eqs(), eqs(), false, ops());
+    }
+
+    @Test
+    void validateAcceptsAWellTypedEd() {
+      assertDoesNotThrow(() -> simple().validate(sch));
+    }
+
+    @Test
+    void validateRejectsAVariableMissingFromTheForallContext() {
+      ED ed =
+          new ED(
+              ctx("a", en()),
+              ctx("e", dept()),
+              eqs(new Pair<>(v("undeclared"), v("undeclared"))),
+              eqs(),
+              false,
+              ops());
+      RuntimeException e = assertThrows(RuntimeException.class, () -> ed.validate(sch));
+      assertTrue(e.getMessage().contains("is not a variable in type context"), e.getMessage());
+    }
+
+    @Test
+    void validateIgnoresTheExistsWhereClause() {
+      // validate only types Awh; an unbound variable in Ewh is not caught here.
+      ED ed =
+          new ED(
+              ctx("a", en()),
+              ctx("e", dept()),
+              eqs(),
+              eqs(new Pair<>(v("undeclared"), v("undeclared"))),
+              false,
+              ops());
+      assertDoesNotThrow(() -> ed.validate(sch));
+    }
+
+    @Test
+    void frontHasAGeneratorPerUniversalVariable() {
+      assertEquals(1, simple().front(sch).gens().size());
+    }
+
+    @Test
+    void backExtendsFrontWithTheExistentialVariables() {
+      ED ed = simple();
+      assertEquals(1, ed.front(sch).gens().size());
+      assertEquals(2, ed.back(sch).gens().size(), "back carries both the forall and exists gens");
+    }
+
+    @Test
+    void frontQAgreesWithFrontOnGenerators() {
+      ED ed = simple();
+      assertEquals(ed.front(sch).gens().size(), ed.frontQ(sch).gens().size());
+    }
+
+    @Test
+    void typeSortedVariablesBecomeSkolemsNotGenerators() {
+      ED ed = new ED(ctx("x", ty()), ctx("e", dept()), eqs(), eqs(), false, ops());
+      assertEquals(0, ed.front(sch).gens().size(), "a type-sorted forall variable is not a gen");
+      assertEquals(1, ed.front(sch).sks().size(), "it is a skolem instead");
+    }
+
+    @Test
+    void asTransformGoesFromFrontToBack() {
+      ED ed = simple();
+      var t = ed.asTransform(sch);
+      assertEquals(ed.front(sch).gens().size(), t.src().gens().size());
+      assertEquals(ed.back(sch).gens().size(), t.dst().gens().size());
+    }
+
+    @Test
+    void getQIsCachedPerSchema() {
+      ED ed = simple();
+      assertSame(ed.getQ(sch), ed.getQ(sch), "getQ memoizes on the schema");
+    }
+
+    @Test
+    void toSqlEmitsAnInsertPerExistentialEntity() {
+      ED ed =
+          new ED(
+              ctx("a", en()),
+              ctx("e", dept()),
+              eqs(),
+              eqs(new Pair<>(Term.Att(label, v("e")), Term.Att(name, v("a")))),
+              false,
+              ops());
+      String sql = ed.toSql(sch);
+      assertTrue(sql.contains("INSERT INTO " + DEPT), sql);
+      assertTrue(sql.contains("SELECT a.name AS [label]"), sql);
+      assertTrue(sql.contains("FROM Employee AS [a]"), sql);
+    }
+
+    @Test
+    void toSqlSkipsTypeSortedExistentials() {
+      // Only entity-sorted existentials become tables to insert into.
+      ED ed = new ED(ctx("a", en()), ctx("x", ty()), eqs(), eqs(), false, ops());
+      assertEquals("", ed.toSql(sch));
+    }
+
+    @Test
+    void toSqlFillsUnconstrainedAttributesWithNull() {
+      String sql = simple().toSql(sch);
+      assertTrue(sql.contains("NULL AS [label]"), "label is unconstrained, so it inserts NULL: " + sql);
+    }
+
+    @Test
+    void toSqlEmitsAWhereClauseForTheForallEquations() {
+      ED ed =
+          new ED(
+              ctx("a", en()),
+              ctx("e", dept()),
+              eqs(new Pair<>(Term.Att(name, v("a")), Term.Att(name, v("a")))),
+              eqs(),
+              false,
+              ops());
+      assertTrue(ed.toSql(sch).contains("WHERE"), ed.toSql(sch));
+    }
+
+    @Test
+    void tptpXSortedRendersAUniversalOverAnExistential() {
+      String tptp = simple().tptpXSorted(sch);
+      assertTrue(tptp.startsWith("(! ["), "opens with a universal quantifier: " + tptp);
+      assertTrue(tptp.contains("? ["), "contains an existential quantifier: " + tptp);
+      assertTrue(tptp.contains("=>"), "the ED is an implication: " + tptp);
+    }
+
+    @Test
+    void tptpXSortedUsesTrueForAnEmptyConclusion() {
+      ED ed = new ED(ctx("a", en()), Collections.emptyMap(), eqs(), eqs(), false, ops());
+      assertTrue(ed.tptpXSorted(sch).contains("$true"), ed.tptpXSorted(sch));
+    }
+
+    @Test
+    void tptpXSortedRejectsUniqueEds() {
+      // tptpXSorted has no encoding for "exists unique" and bails out.
+      ED ed = new ED(ctx("a", en()), ctx("e", dept()), eqs(), eqs(), true, ops());
+      RuntimeException e = assertThrows(RuntimeException.class, () -> ed.tptpXSorted(sch));
+      assertTrue(e.getMessage().contains("Anomaly"), e.getMessage());
+    }
+
+    @Test
+    void sigmaRenamesEntitiesAlongTheMapping() {
+      // sigma with no mapping applied is exercised by the examples; here we check that an ED
+      // over entity-sorted variables keeps its type-sorted ones untouched.
+      ED ed = new ED(ctx("x", ty()), ctx("e", dept()), eqs(), eqs(), false, ops());
+      assertTrue(ed.As.get("x").left, "type-sorted variables are not remapped by sigma");
+    }
+  }
+}
diff --git a/src/catdata/cql/SqlTypeSideSkolemTest.java b/src/catdata/cql/SqlTypeSideSkolemTest.java
new file mode 100644
index 0000000..1cf5cdf
--- /dev/null
+++ b/src/catdata/cql/SqlTypeSideSkolemTest.java
@@ -0,0 +1,409 @@
+package catdata.cql;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertNotNull;
+import static org.junit.jupiter.api.Assertions.assertSame;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+import java.math.BigDecimal;
+import java.sql.Types;
+import java.util.List;
+import java.util.Map;
+import java.util.Optional;
+import java.util.Set;
+import catdata.Pair;
+import catdata.cql.exp.Sym;
+import org.junit.jupiter.api.Nested;
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.CsvSource;
+import org.junit.jupiter.params.provider.ValueSource;
+
+class SqlTypeSideSkolemTest {
+
+  private static final Optional<Boolean> T = Optional.of(true);
+  private static final Optional<Boolean> F = Optional.of(false);
+  private static final Optional<Boolean> U = Optional.empty();
+
+  @Nested
+  class GetSqlType {
+
+    @ParameterizedTest
+    @CsvSource({
+      "varbinary, " + Types.VARBINARY,
+      "longvarbinary, " + Types.LONGVARBINARY,
+      "binary, " + Types.BINARY,
+      "date, " + Types.DATE,
+      "time, " + Types.TIME,
+      "timestamp, " + Types.TIMESTAMP,
+      "bigint, " + Types.BIGINT,
+      "boolean, " + Types.BOOLEAN,
+      "char, " + Types.CHAR,
+      "double, " + Types.DOUBLE,
+      "double precision, " + Types.DOUBLE,
+      "numeric, " + Types.NUMERIC,
+      "decimal, " + Types.DECIMAL,
+      "real, " + Types.REAL,
+      "float, " + Types.FLOAT,
+      "integer, " + Types.INTEGER,
+      "tinyint, " + Types.TINYINT,
+      "bit, " + Types.BIT,
+      "smallint, " + Types.SMALLINT,
+      "nvarchar, " + Types.NVARCHAR,
+      "longvarchar, " + Types.LONGVARCHAR,
+      "text, " + Types.VARCHAR,
+      "varchar, " + Types.VARCHAR,
+      "string, " + Types.VARCHAR,
+      "blob, " + Types.BLOB,
+      "other, " + Types.OTHER,
+      "clob, " + Types.CLOB
+    })
+    void mapsEveryKnownNameToItsJdbcType(String name, int expected) {
+      assertEquals(expected, SqlTypeSideSkolem.getSqlType(name));
+    }
+
+    @ParameterizedTest
+    @ValueSource(strings = {"VARCHAR", "VarChar", "Double Precision", "BIGINT"})
+    void isCaseInsensitive(String name) {
+      assertEquals(
+          SqlTypeSideSkolem.getSqlType(name.toLowerCase()), SqlTypeSideSkolem.getSqlType(name));
+    }
+
+    @Test
+    void collapsesTextAndStringOntoVarchar() {
+      assertEquals(Types.VARCHAR, SqlTypeSideSkolem.getSqlType("text"));
+      assertEquals(Types.VARCHAR, SqlTypeSideSkolem.getSqlType("string"));
+      assertEquals(Types.VARCHAR, SqlTypeSideSkolem.getSqlType("varchar"));
+    }
+
+    @ParameterizedTest
+    @ValueSource(strings = {"unknown", "", "long", "int"})
+    void rejectsUnknownNames(String name) {
+      RuntimeException e =
+          assertThrows(RuntimeException.class, () -> SqlTypeSideSkolem.getSqlType(name));
+      assertTrue(e.getMessage().contains("Unknown sql type"));
+    }
+
+    @Test
+    void rejectsCustomEvenThoughItIsADeclaredType() {
+      // "Custom" is a key of jts(), so it is a legal type of this typeside, but getSqlType has
+      // no case for it. Documents the gap rather than endorsing it.
+      assertTrue(SqlTypeSideSkolem.jts().containsKey("Custom"));
+      assertThrows(RuntimeException.class, () -> SqlTypeSideSkolem.getSqlType("Custom"));
+    }
+  }
+
+  @Nested
+  class Mediate {
+
+    @ParameterizedTest
+    @ValueSource(strings = {"varchar", "string", "VARCHAR", "String"})
+    void lengthQualifiesTheStringTypes(String ty) {
+      assertEquals("varchar(42)", SqlTypeSideSkolem.mediate(42, ty));
+    }
+
+    @ParameterizedTest
+    @ValueSource(strings = {"integer", "Bigint", "date", "blob"})
+    void passesOtherTypesThroughUnchanged(String ty) {
+      assertEquals(ty, SqlTypeSideSkolem.mediate(42, ty));
+    }
+
+    @Test
+    void preservesTheCaseOfPassedThroughTypes() {
+      assertEquals("Timestamp", SqlTypeSideSkolem.mediate(1, "Timestamp"));
+    }
+  }
+
+  @Nested
+  class JavaTypes {
+
+    @Test
+    void tysIsExactlyTheKeySetOfJts() {
+      assertEquals(SqlTypeSideSkolem.jts().keySet(), SqlTypeSideSkolem.tys());
+    }
+
+    @Test
+    void tysIsUnmodifiable() {
+      Set<String> tys = SqlTypeSideSkolem.tys();
+      assertThrows(UnsupportedOperationException.class, () -> tys.add("Nonesuch"));
+    }
+
+    @Test
+    void everyTypeHasAJavaBacking() {
+      Map<String, String> jts = SqlTypeSideSkolem.jts();
+      assertEquals(28, jts.size());
+      for (Map.Entry<String, String> e : jts.entrySet()) {
+        assertNotNull(e.getValue(), e.getKey() + " has no java type");
+        assertTrue(e.getValue().startsWith("java."), e.getKey() + " -> " + e.getValue());
+      }
+    }
+
+    @ParameterizedTest
+    @CsvSource({
+      "Bigint, java.lang.Long",
+      "Bit, java.lang.Boolean",
+      "Double, java.lang.Double",
+      "Double precision, java.lang.Double",
+      "Real, java.lang.Double",
+      "Float, java.lang.Float",
+      "Integer, java.lang.Integer",
+      "Smallint, java.lang.Integer",
+      "Tinyint, java.lang.Integer",
+      "Decimal, java.math.BigDecimal",
+      "Numeric, java.math.BigDecimal",
+      "Varchar, java.lang.String",
+      "Text, java.lang.String",
+      "String, java.lang.String"
+    })
+    void bindsScalarTypesToTheirJavaClasses(String ty, String java) {
+      assertEquals(java, SqlTypeSideSkolem.jts().get(ty));
+    }
+
+    @Test
+    void jtsIsAFreshMapEachCall() {
+      Map<String, String> first = SqlTypeSideSkolem.jts();
+      first.put("Nonesuch", "java.lang.Void");
+      assertTrue(!SqlTypeSideSkolem.jts().containsKey("Nonesuch"));
+    }
+  }
+
+  @Nested
+  class Conjunction {
+
+    @Test
+    void agreesWithTwoValuedLogicOnKnownOperands() {
+      assertEquals(T, SqlTypeSideSkolem.and(T, T));
+      assertEquals(F, SqlTypeSideSkolem.and(T, F));
+      assertEquals(F, SqlTypeSideSkolem.and(F, T));
+      assertEquals(F, SqlTypeSideSkolem.and(F, F));
+    }
+
+    @Test
+    void falseAnnihilatesUnknown() {
+      assertEquals(F, SqlTypeSideSkolem.and(U, F));
+      assertEquals(F, SqlTypeSideSkolem.and(F, U));
+    }
+
+    @Test
+    void trueAndUnknownIsUnknown() {
+      assertEquals(U, SqlTypeSideSkolem.and(U, T));
+      assertEquals(U, SqlTypeSideSkolem.and(T, U));
+    }
+
+    @Test
+    void unknownAndUnknownIsUnknown() {
+      assertEquals(U, SqlTypeSideSkolem.and(U, U));
+    }
+
+    @Test
+    void isCommutative() {
+      List<Optional<Boolean>> vals = List.of(T, F, U);
+      for (Optional<Boolean> x : vals) {
+        for (Optional<Boolean> y : vals) {
+          assertEquals(
+              SqlTypeSideSkolem.and(x, y), SqlTypeSideSkolem.and(y, x), x + " and " + y);
+        }
+      }
+    }
+  }
+
+  @Nested
+  class Disjunction {
+
+    @Test
+    void agreesWithTwoValuedLogicOnKnownOperands() {
+      assertEquals(T, SqlTypeSideSkolem.or(T, T));
+      assertEquals(T, SqlTypeSideSkolem.or(T, F));
+      assertEquals(T, SqlTypeSideSkolem.or(F, T));
+      assertEquals(F, SqlTypeSideSkolem.or(F, F));
+    }
+
+    @Test
+    void trueAnnihilatesUnknown() {
+      assertEquals(T, SqlTypeSideSkolem.or(U, T));
+      assertEquals(T, SqlTypeSideSkolem.or(T, U));
+    }
+
+    @Test
+    void falseOrUnknownIsUnknown() {
+      assertEquals(U, SqlTypeSideSkolem.or(U, F));
+      assertEquals(U, SqlTypeSideSkolem.or(F, U));
+    }
+
+    @Test
+    void unknownOrUnknownIsUnknown() {
+      assertEquals(U, SqlTypeSideSkolem.or(U, U));
+    }
+
+    @Test
+    void isCommutative() {
+      List<Optional<Boolean>> vals = List.of(T, F, U);
+      for (Optional<Boolean> x : vals) {
+        for (Optional<Boolean> y : vals) {
+          assertEquals(SqlTypeSideSkolem.or(x, y), SqlTypeSideSkolem.or(y, x), x + " or " + y);
+        }
+      }
+    }
+  }
+
+  @Nested
+  class Negation {
+
+    @Test
+    void invertsKnownValuesAndFixesUnknown() {
+      assertEquals(F, SqlTypeSideSkolem.not(T));
+      assertEquals(T, SqlTypeSideSkolem.not(F));
+      assertEquals(U, SqlTypeSideSkolem.not(U));
+    }
+
+    @Test
+    void isAnInvolution() {
+      for (Optional<Boolean> x : List.of(T, F, U)) {
+        assertEquals(x, SqlTypeSideSkolem.not(SqlTypeSideSkolem.not(x)), "not not " + x);
+      }
+    }
+
+    @Test
+    void satisfiesDeMorgan() {
+      List<Optional<Boolean>> vals = List.of(T, F, U);
+      for (Optional<Boolean> x : vals) {
+        for (Optional<Boolean> y : vals) {
+          assertEquals(
+              SqlTypeSideSkolem.not(SqlTypeSideSkolem.and(x, y)),
+              SqlTypeSideSkolem.or(SqlTypeSideSkolem.not(x), SqlTypeSideSkolem.not(y)),
+              "not(" + x + " and " + y + ")");
+          assertEquals(
+              SqlTypeSideSkolem.not(SqlTypeSideSkolem.or(x, y)),
+              SqlTypeSideSkolem.and(SqlTypeSideSkolem.not(x), SqlTypeSideSkolem.not(y)),
+              "not(" + x + " or " + y + ")");
+        }
+      }
+    }
+  }
+
+  @Nested
+  class IsFalse {
+
+    @Test
+    void holdsOnlyOfFalse() {
+      assertEquals(T, SqlTypeSideSkolem.isFalse(F));
+      assertEquals(F, SqlTypeSideSkolem.isFalse(T));
+    }
+
+    @Test
+    void isTotalOnUnknown() {
+      // SQL's IS FALSE predicate is a total function: it never yields UNKNOWN, so an unknown
+      // operand answers FALSE rather than propagating. This is what separates it from not().
+      assertEquals(F, SqlTypeSideSkolem.isFalse(U));
+      assertEquals(U, SqlTypeSideSkolem.not(U));
+    }
+  }
+
+  @Nested
+  class Equality {
+
+    @Test
+    void comparesPresentValues() {
+      assertEquals(T, SqlTypeSideSkolem.eq(Optional.of(1), Optional.of(1)));
+      assertEquals(F, SqlTypeSideSkolem.eq(Optional.of(1), Optional.of(2)));
+      assertEquals(T, SqlTypeSideSkolem.eq(Optional.of("a"), Optional.of("a")));
+    }
+
+    @Test
+    void isUnknownWheneverEitherSideIsUnknown() {
+      assertEquals(U, SqlTypeSideSkolem.eq(Optional.empty(), Optional.of(1)));
+      assertEquals(U, SqlTypeSideSkolem.eq(Optional.of(1), Optional.empty()));
+      assertEquals(U, SqlTypeSideSkolem.eq(Optional.empty(), Optional.empty()));
+    }
+
+    @Test
+    void isNullDetectsAbsenceAndNeverReturnsUnknown() {
+      assertEquals(T, SqlTypeSideSkolem.isNull(Optional.empty()));
+      assertEquals(F, SqlTypeSideSkolem.isNull(Optional.of(1)));
+    }
+  }
+
+  @Nested
+  class Arithmetic {
+
+    @Test
+    void addsEachNumericType() {
+      assertEquals(Integer.valueOf(5), SqlTypeSideSkolem.plusInteger(2, 3));
+      assertEquals(Float.valueOf(5.5f), SqlTypeSideSkolem.plusFloat(2.5f, 3.0f));
+      assertEquals(Double.valueOf(5.5), SqlTypeSideSkolem.plusDouble(2.5, 3.0));
+      assertEquals(
+          new BigDecimal("5.5"),
+          SqlTypeSideSkolem.plusBigDecimal(new BigDecimal("2.5"), new BigDecimal("3.0")));
+    }
+
+    @Test
+    void bigDecimalAdditionPreservesScale() {
+      assertEquals(
+          new BigDecimal("1.50"),
+          SqlTypeSideSkolem.plusBigDecimal(new BigDecimal("1.00"), new BigDecimal("0.50")));
+    }
+  }
+
+  @Nested
+  class Symbols {
+
+    @Test
+    void boolConstantsShareTheNullarySort() {
+      assertEquals(List.of(), SqlTypeSideSkolem.boolSort.first);
+      assertEquals("Boolean", SqlTypeSideSkolem.boolSort.second);
+      assertEquals(SqlTypeSideSkolem.boolSort, SqlTypeSideSkolem.t.ty);
+      assertEquals(SqlTypeSideSkolem.boolSort, SqlTypeSideSkolem.f.ty);
+      assertEquals(SqlTypeSideSkolem.boolSort, SqlTypeSideSkolem.n.ty);
+    }
+
+    @Test
+    void boolConstantsAreDistinctAndNamed() {
+      assertEquals("true", SqlTypeSideSkolem.t.str);
+      assertEquals("false", SqlTypeSideSkolem.f.str);
+      assertEquals("null", SqlTypeSideSkolem.n.str);
+      assertTrue(!SqlTypeSideSkolem.t.equals(SqlTypeSideSkolem.f));
+    }
+
+    @Test
+    void symsAreInterned() {
+      assertSame(
+          SqlTypeSideSkolem.t, Sym.Sym("true", SqlTypeSideSkolem.boolSort), "Sym.Sym caches");
+    }
+
+    @Test
+    void boolSortArities() {
+      assertEquals(1, SqlTypeSideSkolem.boolSort1.first.size());
+      assertEquals(2, SqlTypeSideSkolem.boolSort2.first.size());
+      assertEquals("Boolean", SqlTypeSideSkolem.boolSort1.second);
+      assertEquals("Boolean", SqlTypeSideSkolem.boolSort2.second);
+    }
+
+    @Test
+    void declaresBothBoolConstants() {
+      Map<Sym, Pair<List<String>, String>> syms = SqlTypeSideSkolem.syms();
+      assertEquals(SqlTypeSideSkolem.boolSort, syms.get(SqlTypeSideSkolem.t));
+      assertEquals(SqlTypeSideSkolem.boolSort, syms.get(SqlTypeSideSkolem.f));
+    }
+
+    @Test
+    void everySymbolReturnsADeclaredType() {
+      Set<String> tys = SqlTypeSideSkolem.tys();
+      for (Map.Entry<Sym, Pair<List<String>, String>> e : SqlTypeSideSkolem.syms().entrySet()) {
+        assertTrue(
+            tys.contains(e.getValue().second),
+            e.getKey() + " returns undeclared type " + e.getValue().second);
+        for (String arg : e.getValue().first) {
+          assertTrue(tys.contains(arg), e.getKey() + " takes undeclared type " + arg);
+        }
+      }
+    }
+
+    @Test
+    void symKeysAgreeWithTheirDeclaredSignature() {
+      for (Map.Entry<Sym, Pair<List<String>, String>> e : SqlTypeSideSkolem.syms().entrySet()) {
+        assertEquals(e.getKey().ty, e.getValue(), e.getKey() + " signature disagrees with key");
+      }
+    }
+  }
+}