diff --git a/syntax.ebnf b/syntax.ebnf
new file mode 100644
index 0000000..c17444f
--- /dev/null
+++ b/syntax.ebnf
@@ -0,0 +1,72 @@
+input = {top level}.
+
+top level = load | decl.
+
+decl = namespace | def.
+
+(* top level semicolons are optional because all decls start with a
+   special word. like in ocaml *)
+
+load = "load", STRING, [";"].
+
+namespace = "namespace", "{", {decl}, "}", [";"].
+
+def       = def intro, NAME, [":", term], "=", term, [";"].
+def intro = "def0" | "defω" | "def", [qty, "."].
+  (* "def" with no qty defaults to ω *)
+
+qty = "0" | "1" | "ω".
+
+dim = dim const | name.
+dim const = "0" | "1".
+dim arg = "@", dim.
+
+
+pat var = NAME | "_".
+
+term = lambda | case | pi | sigma.
+
+lambda = ("λ" | "δ"), {pat var}+, "⇒", term.
+
+case        = case intro, term, "return", case return, "of", case body.
+case intro  = "case0" | "case1" | "caseω" | "case", qty, ".".
+case return = [pat var, "⇒"], term.
+case body   = "{", {pattern, "⇒", term / ";"}, [";"], "}".
+
+pattern = "zero" | "0"
+        | "succ", pat var, [",", qty, ".", pat var]
+        | TAG
+        | "[", pat var, "]"
+        | "(", pat var, ",", pat var, ")".
+
+pi = qty, ".", (binder | term arg), "→", term.
+binder = "(", {NAME}+, ":", term, ")".
+
+sigma = (binder | ann), "×", (sigma | ann).
+
+ann = infix eq, ["∷", term].
+
+infix eq = app term, ["≡", term, ":", app term]. (* dependent is below *)
+
+app term       = coe | comp | split universe | dep eq | succ | normal app.
+split universe = "★", NAT.
+dep eq         = "Eq", type line, term arg, term arg.
+succ           = "succ", term arg.
+normal app     = term arg, {term arg | dim arg}.
+
+coe       = "coe", type line, dim arg, dim arg, term arg.
+type line = "[", [pat var, "⇒"], term, "]".
+
+comp        = "comp", type line, dim arg, dim arg, term arg, dim arg, comp body.
+comp body   = "{", comp branch, ";", comp branch, [";"], "}".
+comp branch = dim const, name, "⇒", term.
+
+term arg = "{", {BARE TAG}, "}"
+         | TAG
+         | "(", {term / ","}+, ")"
+         | "[", [qty, "."], term, "]"
+         | UNIVERSE
+         | "ℕ"
+         | "zero"
+         | NAT
+         | QNAME.