What's new, version by version.

fill — the universal completion, as one interface.

• Computation as filling a horn — made first-class. A record Universal { Horn, Cand, Good, EqC, fill, fillGood, fillUniq } packages a partial diagram with its unique completion: fill (the completion), fillGood (existence), fillUniq (uniqueness). Universality in one type.
• Different constructions, one fill. Recursion is an instance — the fold, reusing the checked universal.kan theorem, so fill FoldUniversal (ℕ,2,suc) 5 = 7; and so is the terminal object. Two genuinely different universal constructions under the same interface, checked, all three runtimes agreeing. See examples/fill.kan.
• Next: elaborator holes ? the compiler fills by goal type, dispatching to these — "the compiler fills the horn," literally.

The universality checker — diagnostics in Kan-extension terms.

• The totality checker already is a fold checker — it accepts exactly the structural recursions, i.e. the folds (catamorphisms), i.e. the unique maps out of initial algebras. Now it says so: rejections are narrated in universal terms and paired with the canonical fix.
• Instead of a terse "not structural" (or, for a wrapped recursive call, the old cryptic unbound name 'f'), you get: "a total function is the fold — the unique Kan extension of its cases — so recurse on a constructor sub-part, cover every constructor, keep the recursion in tail position, or carry extra state as an accumulator/pair." "This isn't total" becomes "this isn't yet the canonical universal map — here's how to make it one."

"Recursion is a Kan extension" — proven in Kan.

• The philosophy as a checked theorem. In examples/universal.kan: a ℕ-algebra is the data of a fold; fold is the canonical extension (existence); fold_unique proves — by induction, not refl — that any map matching the algebra equations equals the fold. That's the universal property: the fold is the unique map extending the generators — the left Kan extension along {zero, suc} ↪ ℕ.
• And a real function is one: add_is_the_kan_extension shows ordinary recursive add is exactly that fold — so a genuine recursive function is exhibited, with a machine-checked proof, as a left Kan extension. Slogan → theorem.

The Kan lens — kan explain.

• Every program is a Kan extension — and the compiler shows you. A program is a presentation: each definition is a generator, and the program's meaning is its initial model, a left Kan extension of the generators along their inclusion. kan explain <file> renders each definition as its fiber of that one construction — folds and matches as the rich fibers (genuine (co)limits / Kan extensions), a literal as the trivial fiber.
• This turns the tagline ("a Kan program is a partial diagram awaiting universal completion") into something rendered on real code, uniformly — degenerate cases and all. See the front page.

Parametrized modules — signatures, structures, functors.

• record declarations. A record is a signature — a dependent record type. record Monoid { M : U, e : M, op : M -> M -> M, … laws … }. A value of it is a structure; a function between structures is a functor. Fields project with op m, and the checker recovers each field's (possibly dependent) type.
• Functors are just functions. Because a structure is a value, a functor Monoid -> Monoid is an ordinary function — shown with the opposite monoid (flip the op; unit laws swap, associativity reverses via sym) and monoid homomorphisms with an identity hom, all lawful and checked.
• Pure desugaring to a Σ type plus a field registry — no kernel change — and it rides the module system, so each signature lives in its own namespace. All three backends agree. See examples/functors.kan. (Values still use positional tuples; record-literal syntax is next.)

open M.

• open M — after import "x" as M, an open M brings that module's names into scope unqualified, so you can write code instead of Paint::code while M::name keeps working. Opening an alias that wasn't imported is a clear error.

A real module system.

• Every file is a module with its own namespace. Two modules can declare the same name freely — Paint::Color and Mood::Color coexist. A bare name resolves to your own module first, then to the unique imported module that provides it; a genuine clash is a clear error telling you to qualify.
• Imports are explicit — no transitive leaks. You see a module's exports, never its dependencies' names, so a file imports what it actually uses.
• Controls: import "x" as M (qualified M::name), import "x" exposing (a, b) / hiding (a, b) to filter unqualified names, and private def / private data for module-local names that importers can't see (and that different modules may reuse).
• Built in four stages, entirely in the front end — the kernel is untouched, and all three backends agree on namespaced programs. Constructor values still print their short names (the module tag shows only in type errors, where it disambiguates). Loading a file once by path also retires the v0.7.0 "same file imported twice = two copies" caveat. See examples/namespaces.kan.

Namespaces: qualified imports.

• Qualified imports — import "std/nat.kan" as Nat. A module imported as M keeps its names in their own namespace, referenced as M::add, M::Color, M::red — datatypes, constructors, and functions are all namespaced, including inside match. So two modules that each define a Color and a code now coexist happily (Paint::Color vs Mood::Color) instead of colliding. A plain import stays unqualified, so nothing existing changes. The separator is :: (. remains the lambda separator).
• It's a pure front-end feature — a parse-time namespace prefix, no kernel change — and the type checker keeps the namespaces genuinely distinct (feeding a Mood::Color to a Paint function is a type error). All three backends agree on namespaced programs. See examples/namespaces.kan.
• Still to come: export/visibility control and open M — see the design notes.

One namespace, and it's enforced.

• Duplicate top-level names are now a hard error. Kan has a single flat namespace — every def, data type, and constructor shares it. Declaring the same name twice anywhere in a program (a file or anything it imports) used to silently shadow, which hid real bugs — e.g. a constructor and an accessor sharing a name, where the constructor quietly won and the accessor became dead code. The checker now rejects it with a clear message naming the clash.
• Renamed eqInt/ltInt → eqInteger/ltInteger in std/integer.kan (the primitive-Integer comparisons), so they no longer collide with std/int.kan's eqInt on the inductive Int. If you compared primitive Integers, use the new names.

Small categories, named honestly.

• Renamed the category record Category → SmallCategory (breaking). Its objects live in universe U, so it houses exactly the small categories — finite categories, posets, a monoid as a one-object category, the terminal category One, the opposite category op, products. The accessors, Functor, NatTrans, and the Kan-extension statements all follow the new name. If you referenced Category, rename to SmallCategory.
• Charted the path to large categories (Grp, Set, Top). They don't fit SmallCategory on two counts — objects would need a higher universe, and morphism equality would need function extensionality. The fix is a universe-polymorphic, setoid-based Category (hom-equality by an explicit equivalence rather than Id), sketched in open-questions §4. It's additive to the type theory — no soundness risk — and gated only on universe polymorphism.
• Worked example: the category of Groups. Objects (groups), morphisms (group homomorphisms), identity, and composition — built and type-checked, with (ℤ, +) as a concrete object reusing the proven commutative-ring axioms from std/int.kan.

A math library on the reals.

• A small, robust math library on the constructive reals. sqrtQ (√ by Newton's method, correct for all inputs — the iteration count is derived from the argument's size), expQ (exp with argument reduction so it converges for any input), and powNatC (natural-number powers by binary exponentiation). All computed and cross-checked by three backends.
• "New version available" badge. Returning visitors to the home page see when Kan has changed since their last visit (via localStorage; nothing is sent anywhere).

Versioned; exact reals showcased.

• Versioning begins. Established the VERSION file as the single source of truth and added the prominent version + date display to the site — bumped on any public-interface change.
• Exact-reals showcase page added to the website.
• The language as it stood at this baseline: a verified integer tower (ℤ proved a commutative ring, axiom-free), type-enforced rationals with divide-by-zero a type error, constructive reals (√2, π, e to any precision), and lawful category theory + Kan extensions.