echo-types

Constructive Agda prototype for standpoint-indexed epistemic modalities, separating knowledge (factive) from belief and warrant. Provides a tropical-graded bridge from standpoint access to echo-type residues, and a compositional proof-transport calculus with a no-smuggling guarantee across trust boundaries.

Five approaches to building a programming language with every known level of type safety (10 levels, from basic types to homotopy types). An exploration mapping the territory of type safety via five concurrent routes (extend, dyadic, aspect, aggregate, clean-slate) sharing a common test suite and documenting all failures in a stumble journal.

An executable finite-domain Julia companion to the Agda echo-types library, for running echo/residue and Landauer/Bennett constructions on small models and finding counterexamples. It is a model and test aid, not a proof checker.

Constructive Agda development of Echo Types: proof-relevant fibers as typed witnesses for structured information loss under non-injective maps. Provides a mechanised loss taxonomy, separation proofs distinguishing Echo from Shannon entropy and resource grades, and audience surfaces for provenance, security, and sensitivity analysis.

Graded multiparty session / choreographic types in Agda, combining echo loss-grades with epistemic warrants. The keystone K-CUT (grading and transport commute with endpoint projection) is machine-checked, --safe --without-K, for the finite binary-choice plain-merge fragment plus asynchrony. Recursion, full merge, delegation open.

A host-side contract and evidence layer for coprocessor launches: models host/device roles, resource grades, transfer residues, launch receipts and CNO/OND claims. It records launch semantics; it does not run accelerator kernels.

Work in progress: evidence-indexed residual types; checked minimal Agda core, Echo/Epistemic comparisons and a separate finite explorer.