Changelog
Kan's version number is bumped on every change to its public interface — the
canonical value lives in VERSION.
This page says what each bump changed, newest first.
One namespace, and it's enforced.
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.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.
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.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.std/int.kan.A math library on the 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.localStorage; nothing is sent anywhere).Versioned; exact reals showcased.
VERSION file as the single source of truth and
added the prominent version + date display to the site — bumped on any public-interface change.