address remaining TODO, fix issues with left-nesting for for and ext, add motivation blurb to the readme

1 files changed, 16 insertions, 9 deletions

diff --git a/README.md b/README.md
index a6cf033..1ff5a86 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,22 @@
 
 A simple type theory.
 
+## Motivation
+
+There's a pleasant story here about categorical semantics in `Alg(Fam(Lex))^op`, but the real impetus for developing and implementing this particular fragment was the exercise: i had never implemented a dependent type theory before, and wanted to know whether i could deduce how to do so by trying. You, the reader, may be the judge of those efforts.
+
+As a consequence, this code is 100% artisanal, hand-crafted, guaranteed-cruft-and-hacks human written (by me).
+
+Credit goes to [David Jaz](https://www.davidjaz.com/) for developing the fragment and its semantics. Credit goes to me for introducing errors.
+
+## Rust implementation
+
+Usage `makkai [--debug] file1.makkai ... fileN.makkai`
+
+See the [grammar](grammar.txt) for details, and the examples in `examples/`.
+
+Note: the checker does not presently support η-equivalence in all cases and so has some known errors, and likely therefore, some unknown errors.
+
 ## Type Theory
 
 ### Judgements
@@ -74,15 +90,6 @@ A construction admitting an instance of any signature, given an element of a var
 - **Intro.** `C ⊢ case m of { v0. x0 => I0 | ... | vn. xn => In } :: S` when `C ⊢ S signature`, `C ⊢ m : variant { v0. : X0 | ... | vn. : Xn }`, and, for each `i`, `C, xi : Xi ⊢ Ii :: S`.
 - **β.** `case vi. m of { ... | vi. xi => Ii | ... }=Ii[m/xi]`.
 
-
-## Rust implementation
-
-Usage `makkai [--debug] file1.makkai ... fileN.makkai`
-
-See the [grammar](grammar.txt) for details, and the examples in `examples/`.
-
-Note: the checker does not presently support η-equivalence in all cases.
-
 # License
 
 Copyright tslil clingman 2026, this programme is free software and is made available under the terms of the GPL v3 or later. See LICENSE for details.