Agda formalisation of a graded multiparty-session and choreographic type theory, combining echo loss-grades and epistemic standpoint-warrants. The central artefact is the open keystone K-CUT: the conjecture that grading and transport commute with projection across a consistent frontier.
A global choreographic type G is read as a partial causal order. It is projected to local types (endpoint projection), where each edge is graded by:
-
An echo loss-grade (from
echo-types): the structured information loss at that interaction. -
An epistemic standpoint-warrant (from
epistemic-types): the evidence required to authorise that interaction.
A cut is a consistent frontier (antichain) across the causal order. Loss is read modally: ∇ contingent (loss may occur) / △ non-contingent (loss is impossible), indexed by an ordinal loss value.
The sole purpose of this repository is to prove or falsify the keystone conjecture K-CUT: that grading and transport commute with projection across a cut.
K-CUT states: grading and transport commute with endpoint projection across a consistent frontier. It splits into two fragments:
- K-CUT-LOSS
-
Grading commutes with projection as an equality. Loss is type-determined: the grade of the global cut equals the grade computed locally at the endpoint. Status: OPEN (only degenerate single-static-edge base cases exist, proved in sibling repos).
- K-CUT-WARRANT
-
Warrant transport commutes with projection only as a bound, and only under a
SoundWarrantside-condition. The type upper-bounds discoverability but cannot determine it (an agent may know more than the type requires, but never less). Status: OPEN (no proof exists).
|
Caution
|
Nothing in this repo is proven yet. Only degenerate single-static-edge base cases exist, located in sibling repositories ( |
| Concept | Status | Home |
|---|---|---|
Multiparty session / choreographic types |
Standard (Honda–Yoshida–Carbone, Montesi, Hirsch–Garg, Bocchi–Yoshida) |
Core definitions |
Endpoint projection from global to local types |
Standard |
Projection module |
Dioid/tropical grading of sessions |
Standard (various timed/costed session works) |
Re-proved in-site (tropical resource-dioid) |
Echo loss-grades on choreographic edges |
Imported from |
|
Epistemic warrants on choreographic edges |
Imported from |
|
Assembly of echo + epistemic grades on partial causal orders |
Ours (assembly) |
Core definitions |
K-CUT (grading/transport commutes with projection across a cut) |
Ours (conjecture) |
The keystone — OPEN |
This repository imports from the estate’s Agda kernel:
-
echo-types— theℕ ∪ {∞}loss-dioid and thechoreo-grade-commutebase case. -
epistemic-types— the non-factiveWarrant/SoundWarrantinterface (the proof home for the warrant gap in K-CUT-WARRANT).
The tropical resource-dioid is re-proved in-site rather than imported across kernels. This follows the estate’s port-and-reprove pattern (precedent: typed-wasm/…/Tropical.idr), ensuring this repo is self-contained at the resource-algebra layer while maintaining logical consistency with tropical-resource-typing.
Full cited statement of borrowed vs. ours: dev-notes/2026-06-16-choreographic-types-what-it-is.adoc.
-
NOT Gentzen cut-elimination. A cut here is a consistent frontier (antichain) of a causal order, not a proof-theoretic cut.
-
NOT a kernel or engine. Implementation belongs to
typell. -
NOT a subdirectory of
echo-typesorepistemic-types. It is a standalone repository registered innextgen-typing.
| Path | Purpose |
|---|---|
|
Agda formalisation (definitions, projection, K-CUT statement) |
|
Design notes, borrowed-vs-ours statement |
|
Pre-registration state (keystone, provenance, decisions) |
SPDX-License-Identifier: MPL-2.0 — see LICENSE.= Choreographic Types — Graded Multiparty Session Fusion :toc: preamble :toc-title: Contents :icons: font :doctype: article
Agda formalisation of a graded multiparty-session and choreographic type theory, combining echo loss-grades and epistemic standpoint-warrants. The central artefact is the open keystone K-CUT: the conjecture that grading and transport commute with projection across a consistent frontier.
A global choreographic type G is read as a partial causal order. It is projected to local types (endpoint projection), where each edge is graded by:
-
An echo loss-grade (from
echo-types): the structured information loss at that interaction. -
An epistemic standpoint-warrant (from
epistemic-types): the evidence required to authorise that interaction.
A cut is a consistent frontier (antichain) across the causal order. Loss is read modally: ∇ contingent (loss may occur) / △ non-contingent (loss is impossible), indexed by an ordinal loss value.
The sole purpose of this repository is to prove or falsify the keystone conjecture K-CUT: that grading and transport commute with projection across a cut.
K-CUT states: grading and transport commute with endpoint projection across a consistent frontier. It splits into two fragments:
- K-CUT-LOSS
-
Grading commutes with projection as an equality. Loss is type-determined: the grade of the global cut equals the grade computed locally at the endpoint. Status: OPEN (only degenerate single-static-edge base cases exist, proved in sibling repos).
- K-CUT-WARRANT
-
Warrant transport commutes with projection only as a bound, and only under a
SoundWarrantside-condition. The type upper-bounds discoverability but cannot determine it (an agent may know more than the type requires, but never less). Status: OPEN (no proof exists).
|
Caution
|
Nothing in this repo is proven yet. Only degenerate single-static-edge base cases exist, located in sibling repositories ( |
| Concept | Status | Home |
|---|---|---|
Multiparty session / choreographic types |
Standard (Honda–Yoshida–Carbone, Montesi, Hirsch–Garg, Bocchi–Yoshida) |
Core definitions |
Endpoint projection from global to local types |
Standard |
Projection module |
Dioid/tropical grading of sessions |
Standard (various timed/costed session works) |
Re-proved in-site (tropical resource-dioid) |
Echo loss-grades on choreographic edges |
Imported from |
|
Epistemic warrants on choreographic edges |
Imported from |
|
Assembly of echo + epistemic grades on partial causal orders |
Ours (assembly) |
Core definitions |