emdash — Functorial Type Theory

Read the book: Functorial Type Theory: Univalent Foundations for Mathematics · Zenodo record and DOI · Live integrated reviewer

emdash is a research programme and executable formalization for functorial type theory: categorical action is part of the computational language rather than an external structure added after the fact. The development combines dependent type theory with categories, directed families, functors, transfors, and higher cells, using cut-elimination-inspired operations so that functoriality and naturality can compute.

The active development now carries that calculus into local geometry: Cat-valued presheaves, ordinary sieves and sites, a direct fixed-site sheafification construction, universal-property commutative algebra, affine geometry organized by the invertibility sieve $D_R(f)$, site-relative schemes, and a supplied projective-line presentation. These layers keep representability, locality, and construction hypotheses explicit.

Its groupoidal layer now also contains an opaque Circle HIT and a checked encode--decode equivalence between its based loop space and the integers, together with the concrete WalkingEnd-to-Circle nonnegative comparison and a coherent product-transport closure theorem. The same generic lax compositor, when realized in a path category, is now checked as an invertible equality between paths with the usual ap/path-composition presentation and a retained higher action. A classified computational truncation reflector now supplies restricted point-computing elimination and recursor-derived whole map action; its first concrete consumer proves the Circle merely connected and its set truncation contractible, without choosing global based paths or replacing the truncated carrier judgmentally by Unit. Category-indexed Groupoidify(C) has a whole unit and a target-side equivalence between maps out of the realization and path-valued functors on C; specialization recovers the groupoidal Interval from the directed WalkingArrow. A selected strict-object/lax-arrow Gray profile then derives a nonidentity walking-square interchanger from whole internal laxity. Source functoriality and the packaged groupoidification adjunction, the mirror Gray closure, and full Gray monoidality remain explicit boundaries.

An internal semisimplicial substrate now complements that local cell calculus: computing face codes form an augmented injective simplex category; iterated joins and Yoneda give distinct geometric and representable simplices; the boundary and three horns of the two-simplex are ordinary sieves; and a bounded path-groupoid 2-nerve computes all three horn fillers. Categorical decalage adds whole base and cone-tip observations and selected levelwise cone fibres. A variable-dimension decoder now realizes every nonempty skip/keep face code by recursive join maps; its whole identity/composition laws remain gated by join uniqueness. On the dependent side, one homd_/Sigma action now exposes both compositor triangles and an iterable tetrahedron map whose dependent component is the next internal-action projection. The generic compositor of the represented family now also supplies a whole source associator. Typed stable-owner comparisons expose a directed cell from (h o g) o f to h o (g o f) in every target category; its Path specialization is invertible even when the global associativity prototype is disabled. For a constructor-visible three-edge Sigma spine, that same cell projects as the native (kappa,lambda) tetrahedron input, maps through the existing dependent action componentwise, and retains another hom action. More globally, flagged native simplex classifiers through dimension three now iterate PathOut_cat; their whole map action is derived recursively from ordinary functor action, and visible boundaries expose all edges, triangular faces, the fourth face, and the top dependent filler without a parallel simplex record. The dimension-four acceptance level is also active: it derives another whole PathOut action, exposes tetrahedral faces through 0234, and deliberately retains the final 1234/top-filler frame so the later internal code carries recursive readable endpoint views. Degeneracies, generic-dimensional horns/Kan filling, and the whole mapping-category/ displayed-cell comparison remain future work.

That finite pattern now has an internal code. Codes are intrinsically indexed by their decoded category: zero is indexed by C, and a successor at flag x : Obj(K) is indexed by PathOut_K(x). Consequently decoding does not interpret arbitrary category syntax. Selected codes recover the native classifiers through dimension four, existing FaceCode supplies boundary references, and typed endpoint-view packages preserve the formal/readable distinction discovered at dimension four.

Mapped decoding is functorial as well as internal. Given F : C -> D, the code action recursively maps every stored flag, returns a target code over D, and reuses the existing whole pathout_map_func at each successor. The selected codes compute back to the native maps through dimension four, and a further hom action remains available; no parallel simplex-map calculus is introduced.

Nonempty semisimplicial faces now act on the same codes. The existing skip/keep FaceCode recursively selects either a face of the fixed flag, the corresponding face of the target simplex, or the whole outgoing-path image. This computes all three edges of a visible triangle and retains higher action. Visible face composition is preserved by the existing code owner; generic opaque whole-functor uniqueness remains an explicit later comparison.

The ordinal comparison is now constructive in variable dimension. The triangle and tetrahedron slices expose their ordinary faces and dependent top cells; the four-simplex is constructed by repeated whole PathOut lift, maps under every H : Functor(Delta[4],C), and exposes all five tetrahedral cofaces. A genuine Nat recursion then constructs one canonical intrinsic source for every Delta[n]. Arbitrary-target observation and nonempty-face access reuse the existing mapped decoder and FaceCode action, with selected computations checked through dimension four and another higher action retained. The current DependentSimplexObservation(C,n) is an object package; a whole DependentSimplex_cat(C,n) and its mapping-category equivalence with Functor_cat(Delta[n],C) remain future work.

The current v3.2 edition is a checked development draft and a working, bounded product—not a finished foundation, complete proof assistant, or claim of global metatheory.

Read And Review

Start with the concise Functorial Type Theory: An Executable Architecture for Directed Dependency overview, then continue to the current development edition of Functorial Type Theory: Univalent Foundations for Mathematics (0.6.1-dev, 355 pages; Zenodo record and DOI, assembled Markdown). The active mathematical source is emdash2/emdash3_2.lp, together with the modules it imports.

Use the live integrated reviewer to elaborate the bounded categorical syntax, inspect explicit Core and computation, run the three-panel research report, and read the book in the same client-side workbench.

To run that reviewer locally after bootstrapping a fresh checkout:

./scripts/bootstrap-worktree.sh
./scripts/pnpmw run reviewer:dev

For a compact terminal walkthrough of the same architecture:

./scripts/pnpmw run demo:external-review

The browser workbench is published from main by GitHub Pages. It is wholly client-side and does not require a Lambdapi process or other production backend.

What The Reviewer Shows

The reviewer brings four parts of the project into one place:

• an outer dependent logical framework, including a Sigma-telescope example;
• ordinary, natural, displayed-functorial, and displayed-natural categorical binders in their reviewed profiles;
• readable source, backend-neutral explicit emdash Core, inferred types, structural lowering, computation, and source-located failures; and
• the mathematical book alongside the executable examples and preserved minimal-Core playground.

The examples include nested functorial abstraction, a genuinely dependent displayed chain, and a displayed-natural telescope whose named variables cross one Sigma dependency. They are intended to expose the architecture and its present boundary, not to simulate completion of the book's entire notation.

AI-Native Proof And Workspace Foundation

The local TypeScript/emdash layer now also provides a source-first foundation for AI-authored developments: immutable proof plans, stable named goals, fingerprinted checked artifacts, exact module/fragment workspace graphs, locked mounted-file verification with offline cache reuse, finite explicit- dictionary selection, and stable paper/diagram/proof bindings. These features include a checked contextual have whose fact stays visible as a named source obligation even when unused, plus root-scoped typed-term refine templates which expand to ordinary have/exact plans. Fresh replay also derives a portable direct-dependency graph over stable named open goals without changing the proof artifact. A browser-safe two-revision semantic diff now checks both declaration workspaces while leaving proof source inert, reports exact declaration and structural dependency impact, and conservatively identifies unchanged proofs which require recheck—even when the current proof no longer checks. Selected-proof maintenance can then replay one exact current proof, project stable rejection diagnostics, and propose freshly checked exact or one-step-apply replacements for an open named hole. Acceptance returns an ordinary stale-safe plan patch and fresh replay evidence; persisting the changed source and refreshing its outer fingerprint remain explicit caller actions. These features lower to backend-neutral explicit Core and use the TypeScript checker; they do not require a resident proof server, MCP round trip, or Lambdapi process.

Ask the repository itself for the exact implemented and deferred envelope:

./scripts/emdash capabilities --format text
./scripts/emdash check --format text
./scripts/emdash goals --format text
./scripts/emdash workspace check \
  --project-root /absolute/project \
  --data-root /absolute/data

# Explicitly execute the demo management module as a macro, then check only
# its materialized canonical data through the general development command.
node --require ts-node/register \
  examples/v3_2_ai_proof_development_source.ts \
  > /absolute/project/emdash.proof-development.source.json
./scripts/emdash development goals \
  --project-root /absolute/project \
  --format text
./scripts/emdash development graph \
  --project-root /absolute/project \
  --format text

The legacy proof commands deliberately exercise a fixed checked proof module; workspace check accepts only canonical locked workspace files; and development check|goals|build|graph accepts only the fixed canonical proof-development file under an explicit real root. It never imports the management module or discovers an ambient project. The capability record states those scopes rather than presenting this qualified local foundation as an unrestricted host-language sandbox. In the browser reviewer's evidence view, Check paper proof states replays the release-pinned examples and keeps the named open goal visibly incomplete.

The detailed trust boundary, validation history, and consumer-gated next work are in the proof-assistant and goal-graph plan.

Architecture And Authority

Layer	Present role
Active Lambdapi v3.2 development	Authors and checks the categorical declarations, computation rules, and proof-time comparisons. It remains the mathematical authority.
TypeScript surface and explicit Core	Recursively elaborates a reviewed direct-TypeScript and textual surface into backend-neutral explicit owners.
Generic TypeScript dependent LF	Checks explicit Core, performs conversion and bounded reduction, and runs entirely in the client for the reviewer profile.
Lambdapi conformance route	Optionally emits deterministic judgments and compares selected results with the active kernel. It is a development oracle, not a production backend.

The TypeScript implementation is therefore a real small checker/evaluator, but only for its recorded profile. Readable syntax may omit parameters that bidirectional typing can recover; it may not invent categorical action or external naturality evidence when no internal construction owns it.

Current Boundaries

• The text adapter is not a parser for every notation in the book or for arbitrary Lambdapi source. It accepts the reviewed mathematical constructions and fails closed outside them.
• Displayed contexts support arbitrary finite depth in the canonical ordered sibling/Sigma normal form, including displayed-functorial and displayed- natural witnesses, together with qualified depth-generic finite Hom-category recursion. Arbitrary dependency or variance DAGs, general mixed introduction/curry, exchange across dependency, and unrestricted displayed coherence remain open.
• The remaining Lambdapi library has not been proven mechanically transferable as one batch. Bulk transfer qualification is deliberately deferred to a future goal.
• Direct cover completion constructs a fixed-site Cat-valued sheafification reflector. A commutative-ring lift, left exactness, and base-change semantics are not yet derived from it.
• The affine and site-relative scheme layers retain supplied structure-sheaf and locality capabilities. The projective-line package retains its global object and actual overlap; representation-independent schemes, graded Proj, and general projective space remain open.
• Systematic groupoidal specialization for every former, a generic category-to-groupoid reflector, and general normalization, confluence, canonicity, consistency, and semantic soundness for the combined calculus are not claimed. The Circle/Integer and representative product closure results are concrete checked slices, not those global theorems.

These are continuation boundaries, not hidden assumptions of the examples that already run.

Contributor Setup And Focused Commands

Node 22.13 or newer is required. The repository uses the pinned pnpm wrapper and one workspace lockfile; Lambdapi is additionally required for formal kernel and conformance checks.

./scripts/bootstrap-worktree.sh

Use the smallest gate that covers a change:

./scripts/pnpmw run reviewer:dev        # integrated local browser reviewer
./scripts/pnpmw run demo:external-review
./scripts/pnpmw run check:ts            # root TypeScript workbench
./scripts/pnpmw run kernel:check         # active Lambdapi kernel
./scripts/pnpmw run book:check           # authored book contracts

Repository workflow and authority are defined in AGENTS.md; formal-kernel changes also follow emdash2/AGENTS.md. Renewed TypeScript work starts from the v3.2 elaborator handoff, which routes to the living plans and detailed validation history.

Related Projects

• Arrowgram — diagrams and structured technical documents.
• Hotdocx — browser publishing and research workspaces.
• LastRevision.pro — hosted AI workspaces and automation.

Historical TypeScript Prototype

Repository history and parts of the root workbench preserve an earlier dependent-language feasibility prototype with bidirectional elaboration, holes, unification, rewriting, and proof-state machinery. Those generic mechanisms remain useful evidence, but the prototype's old category-specific design is not an authority for v3.2. The elaborator handoff records what was retained, replaced, and graduated in the renewed architecture.