Roadmap

Completed (0.7.0)

  • Phases 1–11: Core functor hierarchy, comonads, arrows, free constructions, recursion schemes, optics, abstract algebra, adjunctions, effect system, proof system
  • Phase 12: External verification (SMT-LIB2, Lean 4, Kani, GPU obligations)
  • Phase 13: Monoidal categories and string diagrams with coherence witnesses
  • Phase 14 A–D: Schubert intersection type system with LR-enriched category
  • Phase 15: 2-categories, enriched categories, bicategories, FFunctor/FMonad
  • Phase 16A: Heyting algebra (foundation for structured emptiness)
  • RichCat: Contentful 2-morphisms with provenance tracking
  • karpal-index: AI-agent library discovery CLI with JSON output

Near-term

  • Phase 16B–D: Presheaves, sieves, subobject classifier, Grothendieck topologies, sheaves
  • Phase 17: End-to-end validation harness across all crates
  • Phase 18: Ecosystem verification integrations (Schubert, Borsalino, ShaperOS)

Research Direction

  • Structured emptiness as a position paper
  • ∞-category encoding feasibility
  • Topos-theoretic grounding for Schubert intersection

Full roadmap: ROADMAP.md