ff-json is a small Cubical Agda library for JSON-shaped data.
Its central design choice is that the recursive JSON tree is parameterized by an atom universe. That lets the same structure represent ordinary JSON and custom JSON-like data with domain-specific primitive atoms.
Public Core
The public entry point is FF.Json. It re-exports:
FF.Json.Base, with generic atom universes, generic JSON values, rendering, and codec records;FF.Json.Native, with ordinary JSON atoms and native constructor helpers.
The generic atom universe has three parts:
Code: names for atom classes
El: the Agda type carried by each atom class
renderAtom: the renderer for that atom
The recursive JSON type has atoms, arrays, and objects. Object key order is preserved, and duplicate keys are representable; the library does not normalize or reject them.
Rendering And Codecs
The rendering surface includes compact and pretty rendering. The compact renderer emits no optional whitespace. The pretty renderer uses a two-space layout.
Codec records are explicit:
ToJSON' encodes a value into a Json U;FromJSON' decodes a Json U into a Maybe A;FromToJSON' packages both directions with a roundtrip law for encoded values.
That law is important. It does not say every JSON value decodes. It says values produced by the encoder decode back to the original Agda value.
Native JSON
The native universe includes strings, natural-number JSON numbers, booleans, and null. Full JSON numeric syntax is intentionally not modeled as one built-in numeric universe; negative numbers, fractions, and exponents can be represented by choosing a different atom universe.
Why It Matters
Proof-assistant workflows constantly cross boundaries. A browser edits a value. A server stores it. A code generator emits a module. A checker accepts or rejects generated source. JSON is a natural interchange format for those steps, but raw JSON strings do not say what has been preserved.
ff-json gives Formal Foundry a checked vocabulary for that boundary. The atom-universe design lets the same recursive tree support ordinary JSON and domain-specific JSON-like data. The codec records then make the important law explicit: values produced by an encoder decode back to the original Agda value.
That makes ff-json a foundation for other parts of the stack. ff-generics can serialize generic specifications and values. State-machine tooling can export structural machine data. MLTTDB-facing tools can use JSON-shaped values around generated records and editor contracts.
The public claim is simple: Formal Foundry does not treat data interchange as an untyped side channel. Even at the JSON layer, the system asks what shape is represented and which roundtrip properties hold.
