ai: rewrite 2ltt skill against original papers and reference impl

.opencode/skills/2ltt/CREDITS.md

@@ -1,35 +1,49 @@
 # Credits / sources
 
-This skill is derived from (and intended to be read alongside) the following papers.
+This skill is derived from (and intended to be read alongside) the following sources.
 
 ## Primary sources
 
 1. András Kovács.
    *Staged Compilation with Two-Level Type Theory.*
    Proc. ACM Program. Lang. 6, ICFP, Article 110 (August 2022), 30 pages.
    DOI: 10.1145/3547641
-   Source PDF (original URL): https://andraskovacs.github.io/pdfs/2ltt.pdf
+   PDF: https://andraskovacs.github.io/pdfs/2ltt.pdf
+   (LaTeX source: `icfp22paper/` in the repository below.)
 
 2. András Kovács.
    *Closure-Free Functional Programming in a Two-Level Type Theory.*
    Proc. ACM Program. Lang. 8, ICFP, Article 259 (August 2024), 34 pages.
    DOI: 10.1145/3674648
-   Source PDF (original URL): https://andraskovacs.github.io/pdfs/2ltt_icfp24.pdf
+   PDF: https://andraskovacs.github.io/pdfs/2ltt_icfp24.pdf
+   (LaTeX source and Agda/Haskell supplements: `icfp24paper/` in the repository below.)
 
 3. Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg.
    *Kinds Are Calling Conventions.*
    Proc. ACM Program. Lang. 4, ICFP, Article 104 (August 2020), 51 pages.
    DOI: 10.1145/3408986
-   Source PDF (original URL): https://pauldownen.com/publications/kacc.pdf
+   PDF: https://pauldownen.com/publications/kacc.pdf
 
 4. András Kovács.
    *ICFP 2022 presentation slides: Staged Compilation with Two-Level Type Theory.*
    Presented 12 September 2022, ICFP Ljubljana.
-   Source PDF (original URL):
    https://github.com/AndrasKovacs/staged/blob/main/icfp22prez/ICFP-Kov%C3%A1cs-StagedCompilationwithTwoLevelTypeTheory.pdf
+   (Content folded into [`kovacs-2022-staged-compilation-2ltt.md`](kovacs-2022-staged-compilation-2ltt.md); no separate notes file.)
 
-## Reference implementation
+## Reference implementations
 
-5. András Kovács.
-   *staged* demo implementation.
-   GitHub repository: https://github.com/AndrasKovacs/staged
+5. András Kovács. *staged* — demo implementation, paper sources, Agda embeddings.
+   https://github.com/AndrasKovacs/staged
+   (The `demo/` directory and its `README.md` are the basis of [`demo-implementation.md`](demo-implementation.md).)
+
+6. András Kovács. *elaboration-zoo* — minimal NbE / bidirectional elaboration
+   references (see branch `01-eval-closures-debruijn` and later branches for
+   metavariables and implicits).
+   https://github.com/AndrasKovacs/elaboration-zoo
+
+## Background
+
+7. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler.
+   *Two-Level Type Theory and Applications.* (origin of 2LTT; homotopy-type-theory
+   motivation, cofibrancy)
+   https://arxiv.org/abs/1705.03307

.opencode/skills/2ltt/SKILL.md

@@ -1,59 +1,72 @@
 ---
 name: 2ltt
-description: Implement (or typecheck + unstage) a practical two-level type theory (2LTT) / staged dependent type system, including a closure-free object language variant and optional representation/calling-convention indexing.
+description: Implement (or typecheck + stage) a practical two-level type theory (2LTT) / staged dependent type system, including a closure-free object language variant and optional representation/calling-convention indexing.
 compatibility: opencode
 ---
 
 ## What I do
 
-I'm a project-local reference for implementing a **two-level type theory (2LTT)**: a dependently typed meta-language with a staged object-language, connected via **lift/quote/splice**.
+I'm a reference for implementing a **two-level type theory (2LTT)**: a dependently typed
+meta-language over a staged object-language, connected via **lift/quote/splice**
+(`⇑A` / `⟨t⟩` / `∼t`). I cover syntax, typing, definitional-equality design, elaboration,
+and the staging algorithm that runs metaprograms to produce splice-free object code.
 
-I focus on implementation details: syntax, typing, definitional equality choices, and an *unstaging* (staging) algorithm that runs metaprograms to produce splice-free object code.
+## Files (each owns its topic; minimal overlap)
 
-## Files to read (in order)
+1. **[`implementation-guide.md`](implementation-guide.md)** — start here. Pipeline architecture, the up-front
+   design decisions (object-equality strength, stage repair vs. reject), NbE core,
+   elaboration guardrails, staging-pass essentials, pitfalls checklist.
 
-1. **`implementation-guide.md`**
-   - Practical "how to build it" plan: core judgments, AST design, typechecker structure, definitional equality strategy, and an executable unstager.
-   - Includes pseudocode and implementation checklists.
+2. **[`demo-implementation.md`](demo-implementation.md)** — code-level walkthrough of the reference Haskell
+   implementation (https://github.com/AndrasKovacs/staged): core syntax, conversion
+   evaluator with stuck splices, two-domain staging evaluator, coercive-subtyping
+   elaboration, unification extensions, what to copy vs. reconsider.
 
-2. **`demo-implementation.md`**
-   - Code snippets from the reference Haskell implementation at https://github.com/AndrasKovacs/staged
-   - Syntax, semantic values, meta evaluation, and staging algorithm.
-   - Useful for seeing how the theory maps to actual code.
+3. **[`kovacs-2022-staged-compilation-2ltt.md`](kovacs-2022-staged-compilation-2ltt.md)** — the core theory (*Staged Compilation
+   with Two-Level Type Theory*): rules, programming patterns, binding-time improvement
+   and inference, staging-by-evaluation with soundness/stability/strictness,
+   object-language variations (monomorphization, representation polymorphism),
+   intensional-analysis options. Also covers the ICFP'22 slides' examples.
 
-3. **`kovacs-2022-staged-compilation-2ltt.md`**
-   - Rewrites the main content of *Staged Compilation with Two-Level Type Theory* (Kovács 2022):
-     universes-by-stage, lift/quote/splice rules, and *staging-by-evaluation* (presheaf-model-inspired) as an algorithmic blueprint.
+4. **[`kovacs-2024-closure-free-2ltt.md`](kovacs-2024-closure-free-2ltt.md)** — the CFTT deltas (*Closure-Free Functional
+   Programming in a 2LTT*): first-order object language with `ValTy`/`CompTy`, weak
+   object equality, `Gen`/let-insertion, `Improve` monad library, join points + SOP,
+   stream fusion, generativity axiom.
 
-4. **`kovacs-2024-closure-free-2ltt.md`**
-   - Rewrites the main content of *Closure-Free Functional Programming in a Two-Level Type Theory* (Kovács 2024):
-     a closure-free object language split into **value types vs computation types**, call-saturation idea, let-insertion via a codegen monad, and the "no intensional code analysis" / generativity theme.
+5. **[`downen-2020-kinds-are-calling-conventions.md`](downen-2020-kinds-are-calling-conventions.md)** — optional layout/arity control:
+   `TYPE ρ ν` kinds, levity, `mono-rep`/`mono-conv` restrictions, closure boxing,
+   lowering to machine language; how it composes with a 2LTT.
 
-5. **`downen-2020-kinds-are-calling-conventions.md`**
-   - Rewrites the parts of *Kinds Are Calling Conventions* (Downen et al. 2020) that are useful when you want the staged object language to control **representation**, **arity**, and **evaluation order** via kind/index information.
-   - Treat this as an optional extension for "layout control" / low-level compilation friendliness.
-
-6. **`kovacs-2022-icfp22-slides.md`**
-   - Deduplicated implementation notes extracted from the ICFP’22 presentation slides (rules, examples: Vec3, and the inference/isomorphism trick for reducing quote/splice annotations).
+6. **[`glossary.md`](glossary.md)** — shared terminology (stage, lift/quote/splice,
+   NbE, read-back, neutral, closure, zonk, binding-time improvement, generativity).
 
 ## When to use me
 
-Use me when you are:
-- implementing a 2LTT core calculus (or a prototype) with **compile-time evaluation** and **typed splicing**;
-- designing an object language meant to compile efficiently (optionally closure-free);
-- adding representation/calling-convention indices to types/kinds for lower-level codegen.
+- implementing or debugging a 2LTT core calculus with compile-time evaluation and
+  typed splicing;
+- designing an object language meant to compile predictably (optionally closure-free);
+- adding representation/calling-convention indices for low-level codegen;
+- reasoning about staging correctness (soundness/stability/strictness) or about what
+  metaprograms can and cannot observe.
 
 ## Guardrails (important)
 
-- Prefer an object-level definitional equality that is **simple and syntax-directed** (often: *no* β/η for object lambdas), so typechecking and unstaging stay predictable.
-- Unstaging should be an evaluation procedure: **run meta**, construct **object AST**, eliminate splices.
-- Avoid "intensional analysis of object code" (pattern matching on AST) if you want the semantic/parametricity properties these papers rely on.
-
-## Elaboration guardrails
-
-These invariants prevent whole classes of bugs; see `implementation-guide.md §13` for detail.
-
-- **`infer` returns `(Term, VTy)`** — always return the elaborated term *and* its type. Never recover types after the fact by pattern-matching on the elaborated term (`typeOf`-style helpers are a red flag).
-- **`checkU` / `check_universe`** — when a term must be a type, check it against the appropriate universe directly (`check t (VU s)`). Don't infer and then ad-hoc test whether the returned type is a universe.
-- **Stuck splices are a neutral** — `Value` needs a `Splice(v)` neutral alongside `Rigid`. Without it, `eval(Quote(Splice(v)))` silently drops the splice. Cancellation rules: `eval(Quote(Splice(v))) = v` and `eval(Splice(Quote(v))) = v`.
-- **Stage-check variables** — record each binding's stage in the context; check it against the current elaboration stage on lookup (`guardStage` in the reference). Otherwise meta variables leak into object code and produce confusing type errors instead of clear stage errors.
+- **Conversion vs. staging are different evaluators.** Staging never β-reduces object
+  code (strictness). Whether *conversion checking* computes object redexes depends on
+  the chosen object theory: full-MLTT object level (2022) — yes; CFTT-style first-order
+  object level — no β/η/let-unfolding at all. Pick one coherently
+  ([`implementation-guide.md`](implementation-guide.md) §2.1).
+- **`infer` returns `(Term, VTy, Stage)`** — never reconstruct types (or stages) from
+  elaborated terms afterwards.
+- **`checkU`** — when a term must be a type, check it against `U s` directly; don't
+  infer-and-test.
+- **Stuck splices need a representation** in the semantic domain (spine entry or
+  neutral), with cancellation in both directions: `∼⟨t⟩ = t` and `⟨∼n⟩ = n`. Otherwise
+  splices are silently dropped or crash on neutrals.
+- **Track a stage for every binding**; on mismatch either *repair* via coercive
+  subtyping (`A ≤ ⇑A`, `⇑A ≤ A` — what the reference implementation does) or *reject*
+  with a clear stage error — but decide explicitly. Keep `let` stages explicit; avoid
+  stage metavariables.
+- **Keep object code opaque** (build/compose/insert only — no pattern-matching on code)
+  unless you deliberately adopt a weakening-only or closed-modality setup; opacity is
+  what makes the standard semantics and the generativity axiom work.