From 50c451cc89ba769e064b8d9fe1001d4d0f884071 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 23 Aug 2026 20:04:39 +0100
Subject: [PATCH 1/2] chore: global textual eradication of Nix and ReScript

---
 AUDIT.adoc | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/AUDIT.adoc b/AUDIT.adoc
index 7ddcc3c..798309f 100644
--- a/AUDIT.adoc
+++ b/AUDIT.adoc
@@ -227,8 +227,8 @@ in the `standards` subdir. Duplicating contractile scaffolding into a small
 prototype would be over-scope and would risk re-propagating stale copies. This
 repository defers to the estate canon.
 
-`guix.scm` / `flake.nix` packaging::
-*Future, not yet done.* The library is not yet packaged for Guix or Nix. This
+`guix.scm` / `flake.guix` packaging::
+*Future, not yet done.* The library is not yet packaged for Guix or Guix. This
 is honest deferral, not hidden debt; the `Justfile` entrypoint is sufficient for
 the prototype tier. Packaging may be added once the API stabilises beyond
 `prototype`.

From fd3756b55752b31e97262b2eb4330e0932447133 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 24 Aug 2026 08:11:17 +0100
Subject: [PATCH 2/2] refactor: migrate repository documentation from Markdown
 to AsciiDoc

---
 CHANGELOG.adoc       |  96 ++++++++++++++
 CHANGELOG.md         |  88 -------------
 CODE_OF_CONDUCT.adoc | 308 +++++++++++++++++++++++++++++++++++++++++++
 CODE_OF_CONDUCT.md   | 261 ------------------------------------
 CONTRIBUTING.adoc    | 232 ++++++++++++++++++++++++++++++++
 CONTRIBUTING.md      | 213 ------------------------------
 SECURITY.adoc        | 109 +++++++++++++++
 SECURITY.md          | 100 --------------
 8 files changed, 745 insertions(+), 662 deletions(-)
 create mode 100644 CHANGELOG.adoc
 delete mode 100644 CHANGELOG.md
 create mode 100644 CODE_OF_CONDUCT.adoc
 delete mode 100644 CODE_OF_CONDUCT.md
 create mode 100644 CONTRIBUTING.adoc
 delete mode 100644 CONTRIBUTING.md
 create mode 100644 SECURITY.adoc
 delete mode 100644 SECURITY.md

diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
new file mode 100644
index 0000000..b175c01
--- /dev/null
+++ b/CHANGELOG.adoc
@@ -0,0 +1,96 @@
+== Changelog
+
+All notable changes to this project will be documented in this file.
+
+The format is based on https://keepachangelog.com/en/1.1.0/[Keep a
+Changelog], and this project adheres to
+https://semver.org/spec/v2.0.0.html[Semantic Versioning].
+
+Dates are ISO 8601 (`+YYYY-MM-DD+`). This is a small, deliberately
+honest Agda formalization that favours mathematical honesty over a large
+API; the changelog records what is actually proved, not what is aspired
+to.
+
+=== https://github.com/hyperpolymath/epistemic-types/compare/v0.1.0...HEAD[Unreleased]
+
+==== Added
+
+* `+EpistemicTypes.ProofTransport+`: standpoint-indexed proof transport
+across trust boundaries.
+** `+View : Agent -> Artifact -> Status -> Claim -> Set+`, with statuses
+`+Data+` / `+Code+` / `+Claimed+` / `+Receipt+` / `+Proof+` /
+`+ProofUnder+`.
+** Transport modes `+Public+` / `+Designated+` / `+IssuerMediated+` /
+`+EnvironmentMediated+` / `+OpaqueReceipt+`.
+** `+transmit+` downgrades a sender’s `+Proof+` to a receiver’s
+`+Receipt+`; `+verify+` upgrades `+Data -> Proof+` only with the
+receiver’s OWN checker and evidence. Public views are portable,
+designated views are receiver-bound, and receipt-only views never
+certify.
+** `+proofNeedsChecker+`: the structural no-smuggling guarantee.
+* `+EpistemicTypes.ProofTransportExample+`: a worked K9-SVC / A2ML
+attestation scenario — issuer `+K9SVC+`, receiver `+Alice+`, third party
+`+Bob+`, claim `+ActionWasPerformed+`, artifact `+AttestationBlob+` —
+exercising transmit, receipt non-certification, and receiver-local
+verification.
+* Engineering rendering of proof transport for `+a2ml+` / `+k9+`
+consumers under `+.machine_readable/proof-transport/+`
+(`+ProofTransport.a2ml+`, `+proof-transport.k9.ncl+`, `+README.adoc+`),
+targeting the estate `+a2ml+` + `+k9+` contractile tooling.
+* `+EpistemicTypes.SurrealBridge+`: graded upgrade of surreal-numbered
+access.
+** `+SurrealAccess+` carrier and `+GradedSurrealModality+`.
+** `+daySurrealAccess+`, a finite birthday-tower account of standpoint
+access.
+
+==== Changed
+
+* `+EpistemicTypes.All+` re-export aggregator extended to include
+`+ProofTransport+`, `+ProofTransportExample+`, and the upgraded
+`+SurrealBridge+`.
+* RSR-compliance and documentation pass: machine-readable `+6a2+`
+descriptors (`+0-AI-MANIFEST.a2ml+`, `+STATE.a2ml+`) and AsciiDoc docs
+(`+readme.adoc+`, `+explainme.adoc+`) brought into line with the current
+module set. Existing lowercase doc filenames are preserved deliberately.
+
+==== Notes
+
+* Continuous integration is not enabled for this repository (see
+`+AUDIT.adoc+`). Verification is local-only via `+just check+`.
+
+=== https://github.com/hyperpolymath/epistemic-types/releases/tag/v0.1.0[0.1.0] - 2026-06-15
+
+Prototype baseline: the first honest formalization of standpoint-indexed
+modal / epistemic / echo-like type formers.
+
+==== Added
+
+* `+EpistemicTypes.Base+`: the core interface.
+`+E : K -> Set ℓ -> Set ℓ+`, where `+E κ A+` reads "``+A+` is
+epistemically available at standpoint `+κ+``". This is a plain indexed
+endofunctor (`+map+` only) — deliberately NOT a monad or comonad, with
+no generic `+return+` / `+reflect+`. Provides `+Modality+`,
+`+LawfulModality+`, `+FactiveModality+`, `+BeliefModality+`, and
+`+ReturnModality+`.
+* `+EpistemicTypes.Warrant+`: `+Warrant+`, `+Epi+`, and
+`+SoundWarrant+`.
+* `+EpistemicTypes.Access+`: a `+Preorder+` on standpoints and an
+`+AccessibleModality+` whose `+increase+` transports availability along
+the preorder.
+* `+EpistemicTypes.EchoBridge+`: min-plus graded loss / residue
+`+Echo r A+`, kept deliberately distinct from `+E κ A+`. Composes with
+the sibling `+echo-types+` loss-with-residue formalism.
+* `+EpistemicTypes.SurrealBridge+`: initial `+SurrealAccess+` carrier
+and graded surreal modality.
+* `+EpistemicTypes.Examples+`: small worked instances of the above.
+* `+EpistemicTypes.All+`: re-export aggregator over the public modules.
+* Build tooling: a `+Justfile+` with `+just check+`, defined as
+`+agda --no-libraries -i src src/EpistemicTypes/All.agda+` (Agda 2.8.0),
+plus the `+epistemic-types.agda-lib+` library descriptor.
+
+==== Project conventions
+
+* Compiles under `+{-# OPTIONS --safe --without-K #-}+`.
+* No postulates.
+* No Agda standard library: built with `+agda --no-libraries+`, using
+only `+Agda.Builtin.*+` and `+Agda.Primitive+`.
diff --git a/CHANGELOG.md b/CHANGELOG.md
deleted file mode 100644
index 24fc131..0000000
--- a/CHANGELOG.md
+++ /dev/null
@@ -1,88 +0,0 @@
-# Changelog
-
-All notable changes to this project will be documented in this file.
-
-The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
-and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
-
-Dates are ISO 8601 (`YYYY-MM-DD`). This is a small, deliberately honest Agda
-formalization that favours mathematical honesty over a large API; the changelog
-records what is actually proved, not what is aspired to.
-
-## [Unreleased]
-
-### Added
-
-- `EpistemicTypes.ProofTransport`: standpoint-indexed proof transport across
-  trust boundaries.
-  - `View : Agent -> Artifact -> Status -> Claim -> Set`, with statuses
-    `Data` / `Code` / `Claimed` / `Receipt` / `Proof` / `ProofUnder`.
-  - Transport modes `Public` / `Designated` / `IssuerMediated` /
-    `EnvironmentMediated` / `OpaqueReceipt`.
-  - `transmit` downgrades a sender's `Proof` to a receiver's `Receipt`;
-    `verify` upgrades `Data -> Proof` only with the receiver's OWN checker and
-    evidence. Public views are portable, designated views are receiver-bound,
-    and receipt-only views never certify.
-  - `proofNeedsChecker`: the structural no-smuggling guarantee.
-- `EpistemicTypes.ProofTransportExample`: a worked K9-SVC / A2ML attestation
-  scenario — issuer `K9SVC`, receiver `Alice`, third party `Bob`, claim
-  `ActionWasPerformed`, artifact `AttestationBlob` — exercising transmit,
-  receipt non-certification, and receiver-local verification.
-- Engineering rendering of proof transport for `a2ml` / `k9` consumers under
-  `.machine_readable/proof-transport/` (`ProofTransport.a2ml`,
-  `proof-transport.k9.ncl`, `README.adoc`), targeting the estate `a2ml` + `k9`
-  contractile tooling.
-- `EpistemicTypes.SurrealBridge`: graded upgrade of surreal-numbered access.
-  - `SurrealAccess` carrier and `GradedSurrealModality`.
-  - `daySurrealAccess`, a finite birthday-tower account of standpoint access.
-
-### Changed
-
-- `EpistemicTypes.All` re-export aggregator extended to include
-  `ProofTransport`, `ProofTransportExample`, and the upgraded `SurrealBridge`.
-- RSR-compliance and documentation pass: machine-readable `6a2` descriptors
-  (`0-AI-MANIFEST.a2ml`, `STATE.a2ml`) and AsciiDoc docs (`readme.adoc`,
-  `explainme.adoc`) brought into line with the current module set. Existing
-  lowercase doc filenames are preserved deliberately.
-
-### Notes
-
-- Continuous integration is not enabled for this repository (see `AUDIT.adoc`).
-  Verification is local-only via `just check`.
-
-## [0.1.0] - 2026-06-15
-
-Prototype baseline: the first honest formalization of standpoint-indexed
-modal / epistemic / echo-like type formers.
-
-### Added
-
-- `EpistemicTypes.Base`: the core interface. `E : K -> Set ℓ -> Set ℓ`, where
-  `E κ A` reads "`A` is epistemically available at standpoint `κ`". This is a
-  plain indexed endofunctor (`map` only) — deliberately NOT a monad or comonad,
-  with no generic `return` / `reflect`. Provides `Modality`, `LawfulModality`,
-  `FactiveModality`, `BeliefModality`, and `ReturnModality`.
-- `EpistemicTypes.Warrant`: `Warrant`, `Epi`, and `SoundWarrant`.
-- `EpistemicTypes.Access`: a `Preorder` on standpoints and an
-  `AccessibleModality` whose `increase` transports availability along the
-  preorder.
-- `EpistemicTypes.EchoBridge`: min-plus graded loss / residue `Echo r A`, kept
-  deliberately distinct from `E κ A`. Composes with the sibling `echo-types`
-  loss-with-residue formalism.
-- `EpistemicTypes.SurrealBridge`: initial `SurrealAccess` carrier and graded
-  surreal modality.
-- `EpistemicTypes.Examples`: small worked instances of the above.
-- `EpistemicTypes.All`: re-export aggregator over the public modules.
-- Build tooling: a `Justfile` with `just check`, defined as
-  `agda --no-libraries -i src src/EpistemicTypes/All.agda` (Agda 2.8.0), plus
-  the `epistemic-types.agda-lib` library descriptor.
-
-### Project conventions
-
-- Compiles under `{-# OPTIONS --safe --without-K #-}`.
-- No postulates.
-- No Agda standard library: built with `agda --no-libraries`, using only
-  `Agda.Builtin.*` and `Agda.Primitive`.
-
-[Unreleased]: https://github.com/hyperpolymath/epistemic-types/compare/v0.1.0...HEAD
-[0.1.0]: https://github.com/hyperpolymath/epistemic-types/releases/tag/v0.1.0
diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc
new file mode 100644
index 0000000..556f73f
--- /dev/null
+++ b/CODE_OF_CONDUCT.adoc
@@ -0,0 +1,308 @@
+== Code of Conduct
+
+=== Our Pledge
+
+We as members, contributors, and leaders pledge to make participation in
+epistemic-types a harassment-free experience for everyone, regardless of
+age, body size, visible or invisible disability, ethnicity, sex
+characteristics, gender identity and expression, level of experience,
+education, socio-economic status, nationality, personal appearance,
+race, caste, colour, religion, or sexual identity and orientation.
+
+We pledge to act and interact in ways that contribute to an open,
+welcoming, diverse, inclusive, and healthy community.
+
+epistemic-types is a small, deliberately honest Agda formalisation of
+standpoint-indexed modal / epistemic / echo-like type formers. It is a
+single-maintainer prototype, so this Code of Conduct is right-sized
+accordingly: the community here is small, and reports go directly to the
+maintainer. We recognise that even a small project benefits from
+*psychological safety* — an environment where people can contribute, ask
+questions, make mistakes, and learn without fear of ridicule or
+retaliation.
+
+'''''
+
+=== Our Standards
+
+==== Expected Behaviour
+
+The following behaviours contribute to a positive environment:
+
+*Communication* - Using welcoming and inclusive language - Being
+respectful of differing viewpoints and experiences - Giving and
+gracefully accepting constructive feedback - Assuming good intent while
+addressing impact - Communicating clearly and patiently, especially with
+newcomers
+
+*Collaboration* - Focusing on what is best for the community - Showing
+empathy and kindness toward other community members - Being
+collaborative rather than competitive - Mentoring and supporting less
+experienced contributors - Celebrating others’ contributions and
+successes
+
+*Professionalism* - Accepting responsibility and apologising to those
+affected by our mistakes - Learning from the experience and avoiding
+repetition - Respecting others’ time and attention - Staying on topic in
+project spaces - Following project conventions (this is a
+`+--safe --without-K+` Agda library with no postulates and no standard
+library; corrections and proofs should preserve that discipline)
+
+*Accessibility* - Using plain language and avoiding unnecessary jargon -
+Providing alt text for images and transcripts for audio/video - Being
+patient with those using assistive technologies - Accommodating
+different communication styles and needs - Recognising that not everyone
+communicates the same way
+
+==== Unacceptable Behaviour
+
+The following behaviours are considered harassment and are unacceptable:
+
+*Harassment* - The use of sexualised language or imagery, and sexual
+attention or advances of any kind - Trolling, insulting or derogatory
+comments, and personal or political attacks - Public or private
+harassment - Deliberate intimidation, stalking, or following (online or
+in-person) - Unwelcome physical contact or simulated physical contact
+(e.g., emoji) - Sustained disruption of discussions
+
+*Discrimination* - Discriminatory jokes and language - Posting or
+threatening to post others’ personally identifying information
+("`doxing`") - Advocating for, or encouraging, any of the above
+behaviour - Microaggressions — subtle, often unintentional,
+discriminatory comments or actions
+
+*Professional Misconduct* - Publishing others’ private information
+without explicit permission - Misrepresenting affiliation or
+contributions - Plagiarism or claiming credit for others’ work -
+Retaliating against anyone who reports a Code of Conduct violation -
+Other conduct which could reasonably be considered inappropriate in a
+professional setting
+
+==== Grey Areas
+
+Some situations require judgement. When uncertain:
+
+* *Intent vs Impact*: Good intentions do not excuse harmful impact.
+Focus on making things right.
+* *Power Dynamics*: Those with more power (the maintainer, employers,
+experienced contributors) must be especially mindful of their impact.
+* *Cultural Differences*: What’s acceptable varies by culture. When in
+doubt, err on the side of caution and ask.
+* *Humour*: Jokes at others’ expense are rarely funny to everyone. Punch
+up, not down.
+
+'''''
+
+=== Scope
+
+This Code of Conduct applies within all project spaces, including:
+
+*Online Spaces* - Repository discussions, issues, and pull requests on
+`+hyperpolymath/epistemic-types+` - Mailing lists and forums where the
+project is discussed - Social media when representing the project
+
+*In-Person Spaces* - Any meeting, talk, or gathering where you represent
+the project
+
+*Representation* This Code of Conduct also applies when an individual is
+officially representing the project in public spaces. Examples include:
+
+* Using an official project email address
+* Posting via an official social media account
+* Speaking on behalf of the project
+
+'''''
+
+=== Enforcement
+
+==== Reporting
+
+If you experience or witness unacceptable behaviour, or have any other
+concerns, please report it as soon as possible.
+
+*How to Report*
+
+[width="99%",cols="30%,33%,37%",options="header",]
+|===
+|Method |Details |Best For
+|*Email* |Jonathan D.A. Jewell (hyperpolymath) — j.d.a.jewell@open.ac.uk
+|All reports, including sensitive matters
+
+|*Private Message* |Contact the maintainer directly |Quick questions,
+minor issues
+|===
+
+As a single-maintainer prototype, reports are received and handled by
+the maintainer, Jonathan D.A. Jewell (hyperpolymath).
+
+*What to Include*
+
+* Your contact information (unless you wish to remain anonymous)
+* Names/usernames of those involved
+* Description of what happened
+* When and where it occurred
+* Any witnesses
+* Any supporting evidence (screenshots, links)
+* How you would like us to respond (if you have a preference)
+
+*What Happens Next*
+
+[arabic]
+. You will receive acknowledgment within *5 working days*
+. The maintainer will review the report
+. We may ask for additional information
+. We will determine appropriate action
+. We will inform you of the outcome (respecting others’ privacy)
+
+==== Confidentiality
+
+All reports will be handled with discretion:
+
+* Reporter identity is protected by default
+* Details are shared only with those who need to know
+* We will ask before naming you in any communication
+* Anonymous reports are accepted and investigated as far as is practical
+
+==== Conflicts of Interest
+
+If the maintainer is themselves involved in an incident, an independent
+and trusted third party will be asked to review the report. Any
+potential conflict will be disclosed.
+
+'''''
+
+=== Enforcement Guidelines
+
+The maintainer will follow these guidelines in determining consequences:
+
+==== 1. Correction
+
+*Community Impact*: Use of inappropriate language or other behaviour
+deemed unprofessional or unwelcome.
+
+*Consequence*: A private, written warning providing clarity around the
+nature of the violation and an explanation of why the behaviour was
+inappropriate. A public apology may be requested.
+
+*Duration*: Immediate
+
+==== 2. Warning
+
+*Community Impact*: A violation through a single incident or series of
+actions.
+
+*Consequence*: A warning with consequences for continued behaviour. No
+interaction with the people involved, including unsolicited interaction
+with those enforcing the Code of Conduct, for a specified period. This
+includes avoiding interactions in project spaces as well as external
+channels like social media. Violating these terms may lead to a
+temporary or permanent ban.
+
+*Duration*: 1-4 weeks
+
+==== 3. Temporary Ban
+
+*Community Impact*: A serious violation of community standards,
+including sustained inappropriate behaviour.
+
+*Consequence*: A temporary ban from any sort of interaction or public
+communication within the project for a specified period. No public or
+private interaction with the people involved, including unsolicited
+interaction with those enforcing the Code of Conduct, is allowed during
+this period. Violating these terms may lead to a permanent ban.
+
+*Duration*: 1-6 months
+
+==== 4. Permanent Ban
+
+*Community Impact*: Demonstrating a pattern of violation of community
+standards, including sustained inappropriate behaviour, harassment of an
+individual, or aggression toward or disparagement of classes of
+individuals.
+
+*Consequence*: A permanent ban from any sort of public interaction
+within the project.
+
+*Duration*: Permanent (with appeal rights after 12 months)
+
+'''''
+
+=== Appeals
+
+If you believe an enforcement decision was made in error:
+
+[arabic]
+. *Wait 7 days* after the decision (cooling-off period)
+. *Email* j.d.a.jewell@open.ac.uk with subject line "`Appeal: [Original
+Report Reference]`"
+. *Explain* why you believe the decision should be reconsidered
+. *Provide* any new information not previously available
+
+*Grounds for Appeal*
+
+* Procedural errors in the original handling
+* New evidence not previously available
+* Disproportionate response to the violation
+* Misunderstanding of facts
+
+Because this is a single-maintainer project, an appeal may be reviewed
+by the maintainer or, where a conflict exists, by an independent third
+party. The appeals decision is final, and you may only appeal once per
+incident.
+
+'''''
+
+=== Supporting Those Who Report
+
+We are committed to supporting those who report violations:
+
+*We Will* - Believe and take all reports seriously - Respect your
+privacy and confidentiality preferences - Keep you informed of progress
+(if you wish) - Take steps to protect you from retaliation - Provide
+resources if you need support
+
+*We Will Not* - Require you to confront the person directly - Dismiss
+reports without investigation - Reveal your identity without consent -
+Tolerate retaliation against reporters - Rush you to make decisions
+
+'''''
+
+=== Acknowledgments
+
+This Code of Conduct is adapted from:
+
+* https://www.contributor-covenant.org/[Contributor Covenant], version
+2.1
+* https://www.djangoproject.com/conduct/[Django Code of Conduct]
+* https://www.rust-lang.org/policies/code-of-conduct[Rust Code of
+Conduct]
+* https://www.python.org/psf/conduct/[Python Community Code of Conduct]
+
+We thank these communities for their leadership in creating welcoming
+spaces.
+
+'''''
+
+=== Questions?
+
+If you have questions about this Code of Conduct:
+
+* Open a
+https://github.com/hyperpolymath/epistemic-types/discussions[Discussion]
+(for general questions)
+* Email j.d.a.jewell@open.ac.uk (for private questions)
+* Contact the maintainer directly
+
+'''''
+
+=== Summary
+
+*Be kind. Be respectful. Be collaborative.*
+
+We’re all here because we care about getting the mathematics honest.
+Let’s make this a place where everyone can do their best work.
+
+'''''
+
+Last updated: 2026-06-15 · epistemic-types 0.1.0 (prototype) · Based on
+Contributor Covenant 2.1
diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md
deleted file mode 100644
index 2d2e50b..0000000
--- a/CODE_OF_CONDUCT.md
+++ /dev/null
@@ -1,261 +0,0 @@
-# Code of Conduct
-
-## Our Pledge
-
-We as members, contributors, and leaders pledge to make participation in epistemic-types a harassment-free experience for everyone, regardless of age, body size, visible or invisible disability, ethnicity, sex characteristics, gender identity and expression, level of experience, education, socio-economic status, nationality, personal appearance, race, caste, colour, religion, or sexual identity and orientation.
-
-We pledge to act and interact in ways that contribute to an open, welcoming, diverse, inclusive, and healthy community.
-
-epistemic-types is a small, deliberately honest Agda formalisation of standpoint-indexed modal / epistemic / echo-like type formers. It is a single-maintainer prototype, so this Code of Conduct is right-sized accordingly: the community here is small, and reports go directly to the maintainer. We recognise that even a small project benefits from **psychological safety** — an environment where people can contribute, ask questions, make mistakes, and learn without fear of ridicule or retaliation.
-
----
-
-## Our Standards
-
-### Expected Behaviour
-
-The following behaviours contribute to a positive environment:
-
-**Communication**
-- Using welcoming and inclusive language
-- Being respectful of differing viewpoints and experiences
-- Giving and gracefully accepting constructive feedback
-- Assuming good intent while addressing impact
-- Communicating clearly and patiently, especially with newcomers
-
-**Collaboration**
-- Focusing on what is best for the community
-- Showing empathy and kindness toward other community members
-- Being collaborative rather than competitive
-- Mentoring and supporting less experienced contributors
-- Celebrating others' contributions and successes
-
-**Professionalism**
-- Accepting responsibility and apologising to those affected by our mistakes
-- Learning from the experience and avoiding repetition
-- Respecting others' time and attention
-- Staying on topic in project spaces
-- Following project conventions (this is a `--safe --without-K` Agda library with no postulates and no standard library; corrections and proofs should preserve that discipline)
-
-**Accessibility**
-- Using plain language and avoiding unnecessary jargon
-- Providing alt text for images and transcripts for audio/video
-- Being patient with those using assistive technologies
-- Accommodating different communication styles and needs
-- Recognising that not everyone communicates the same way
-
-### Unacceptable Behaviour
-
-The following behaviours are considered harassment and are unacceptable:
-
-**Harassment**
-- The use of sexualised language or imagery, and sexual attention or advances of any kind
-- Trolling, insulting or derogatory comments, and personal or political attacks
-- Public or private harassment
-- Deliberate intimidation, stalking, or following (online or in-person)
-- Unwelcome physical contact or simulated physical contact (e.g., emoji)
-- Sustained disruption of discussions
-
-**Discrimination**
-- Discriminatory jokes and language
-- Posting or threatening to post others' personally identifying information ("doxing")
-- Advocating for, or encouraging, any of the above behaviour
-- Microaggressions — subtle, often unintentional, discriminatory comments or actions
-
-**Professional Misconduct**
-- Publishing others' private information without explicit permission
-- Misrepresenting affiliation or contributions
-- Plagiarism or claiming credit for others' work
-- Retaliating against anyone who reports a Code of Conduct violation
-- Other conduct which could reasonably be considered inappropriate in a professional setting
-
-### Grey Areas
-
-Some situations require judgement. When uncertain:
-
-- **Intent vs Impact**: Good intentions do not excuse harmful impact. Focus on making things right.
-- **Power Dynamics**: Those with more power (the maintainer, employers, experienced contributors) must be especially mindful of their impact.
-- **Cultural Differences**: What's acceptable varies by culture. When in doubt, err on the side of caution and ask.
-- **Humour**: Jokes at others' expense are rarely funny to everyone. Punch up, not down.
-
----
-
-## Scope
-
-This Code of Conduct applies within all project spaces, including:
-
-**Online Spaces**
-- Repository discussions, issues, and pull requests on `hyperpolymath/epistemic-types`
-- Mailing lists and forums where the project is discussed
-- Social media when representing the project
-
-**In-Person Spaces**
-- Any meeting, talk, or gathering where you represent the project
-
-**Representation**
-This Code of Conduct also applies when an individual is officially representing the project in public spaces. Examples include:
-
-- Using an official project email address
-- Posting via an official social media account
-- Speaking on behalf of the project
-
----
-
-## Enforcement
-
-### Reporting
-
-If you experience or witness unacceptable behaviour, or have any other concerns, please report it as soon as possible.
-
-**How to Report**
-
-| Method | Details | Best For |
-|--------|---------|----------|
-| **Email** | Jonathan D.A. Jewell (hyperpolymath) — j.d.a.jewell@open.ac.uk | All reports, including sensitive matters |
-| **Private Message** | Contact the maintainer directly | Quick questions, minor issues |
-
-As a single-maintainer prototype, reports are received and handled by the maintainer, Jonathan D.A. Jewell (hyperpolymath).
-
-**What to Include**
-
-- Your contact information (unless you wish to remain anonymous)
-- Names/usernames of those involved
-- Description of what happened
-- When and where it occurred
-- Any witnesses
-- Any supporting evidence (screenshots, links)
-- How you would like us to respond (if you have a preference)
-
-**What Happens Next**
-
-1. You will receive acknowledgment within **5 working days**
-2. The maintainer will review the report
-3. We may ask for additional information
-4. We will determine appropriate action
-5. We will inform you of the outcome (respecting others' privacy)
-
-### Confidentiality
-
-All reports will be handled with discretion:
-
-- Reporter identity is protected by default
-- Details are shared only with those who need to know
-- We will ask before naming you in any communication
-- Anonymous reports are accepted and investigated as far as is practical
-
-### Conflicts of Interest
-
-If the maintainer is themselves involved in an incident, an independent and trusted third party will be asked to review the report. Any potential conflict will be disclosed.
-
----
-
-## Enforcement Guidelines
-
-The maintainer will follow these guidelines in determining consequences:
-
-### 1. Correction
-
-**Community Impact**: Use of inappropriate language or other behaviour deemed unprofessional or unwelcome.
-
-**Consequence**: A private, written warning providing clarity around the nature of the violation and an explanation of why the behaviour was inappropriate. A public apology may be requested.
-
-**Duration**: Immediate
-
-### 2. Warning
-
-**Community Impact**: A violation through a single incident or series of actions.
-
-**Consequence**: A warning with consequences for continued behaviour. No interaction with the people involved, including unsolicited interaction with those enforcing the Code of Conduct, for a specified period. This includes avoiding interactions in project spaces as well as external channels like social media. Violating these terms may lead to a temporary or permanent ban.
-
-**Duration**: 1-4 weeks
-
-### 3. Temporary Ban
-
-**Community Impact**: A serious violation of community standards, including sustained inappropriate behaviour.
-
-**Consequence**: A temporary ban from any sort of interaction or public communication within the project for a specified period. No public or private interaction with the people involved, including unsolicited interaction with those enforcing the Code of Conduct, is allowed during this period. Violating these terms may lead to a permanent ban.
-
-**Duration**: 1-6 months
-
-### 4. Permanent Ban
-
-**Community Impact**: Demonstrating a pattern of violation of community standards, including sustained inappropriate behaviour, harassment of an individual, or aggression toward or disparagement of classes of individuals.
-
-**Consequence**: A permanent ban from any sort of public interaction within the project.
-
-**Duration**: Permanent (with appeal rights after 12 months)
-
----
-
-## Appeals
-
-If you believe an enforcement decision was made in error:
-
-1. **Wait 7 days** after the decision (cooling-off period)
-2. **Email** j.d.a.jewell@open.ac.uk with subject line "Appeal: [Original Report Reference]"
-3. **Explain** why you believe the decision should be reconsidered
-4. **Provide** any new information not previously available
-
-**Grounds for Appeal**
-
-- Procedural errors in the original handling
-- New evidence not previously available
-- Disproportionate response to the violation
-- Misunderstanding of facts
-
-Because this is a single-maintainer project, an appeal may be reviewed by the maintainer or, where a conflict exists, by an independent third party. The appeals decision is final, and you may only appeal once per incident.
-
----
-
-## Supporting Those Who Report
-
-We are committed to supporting those who report violations:
-
-**We Will**
-- Believe and take all reports seriously
-- Respect your privacy and confidentiality preferences
-- Keep you informed of progress (if you wish)
-- Take steps to protect you from retaliation
-- Provide resources if you need support
-
-**We Will Not**
-- Require you to confront the person directly
-- Dismiss reports without investigation
-- Reveal your identity without consent
-- Tolerate retaliation against reporters
-- Rush you to make decisions
-
----
-
-## Acknowledgments
-
-This Code of Conduct is adapted from:
-
-- [Contributor Covenant](https://www.contributor-covenant.org/), version 2.1
-- [Django Code of Conduct](https://www.djangoproject.com/conduct/)
-- [Rust Code of Conduct](https://www.rust-lang.org/policies/code-of-conduct)
-- [Python Community Code of Conduct](https://www.python.org/psf/conduct/)
-
-We thank these communities for their leadership in creating welcoming spaces.
-
----
-
-## Questions?
-
-If you have questions about this Code of Conduct:
-
-- Open a [Discussion](https://github.com/hyperpolymath/epistemic-types/discussions) (for general questions)
-- Email j.d.a.jewell@open.ac.uk (for private questions)
-- Contact the maintainer directly
-
----
-
-## Summary
-
-**Be kind. Be respectful. Be collaborative.**
-
-We're all here because we care about getting the mathematics honest. Let's make this a place where everyone can do their best work.
-
----
-
-<sub>Last updated: 2026-06-15 · epistemic-types 0.1.0 (prototype) · Based on Contributor Covenant 2.1</sub>
diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc
new file mode 100644
index 0000000..2c1e934
--- /dev/null
+++ b/CONTRIBUTING.adoc
@@ -0,0 +1,232 @@
+== Contributing to epistemic-types
+
+`+epistemic-types+` is a small, deliberately honest Agda formalization
+of standpoint-indexed modal / epistemic / echo-like type formers. It
+favours mathematical honesty over a large API. Contributions are
+welcome, but the bar is *everything still type-checks under
+`+--safe --without-K+`, with no shortcuts*.
+
+* *Author:* Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
+* *Version:* 0.1.0 (status: prototype)
+* *Last updated:* 2026-06-15
+
+'''''
+
+=== Contribution model — Tri-Perimeter Contribution Framework (TPCF)
+
+epistemic-types follows the estate-wide *Tri-Perimeter Contribution
+Framework (TPCF)* — graduated trust without gatekeeping:
+
+* *Perimeter 1 — Core Systems (maintainers only).* The proof kernel:
+`+src/EpistemicTypes/*.agda+` (Base, Access, Warrant, ProofTransport,
+the EchoBridge/SurrealBridge), the `+All.agda+` wiring, and build
+tooling.
+* *Perimeter 2 — Expert Extensions (trusted contributors).* New
+epistemic/standpoint modules, examples, and bridges. Apply via issue →
+review → merge, with `+just check+` green.
+* *Perimeter 3 — Community Sandbox (open to all).* Docs (`+.adoc+`),
+`+.well-known/+`, AI manifests, spec proposals.
+
+==== Fork workflow
+
+External contributors use the standard *fork*-and-pull-request workflow:
+fork the repository, branch from `+main+`, run `+just check+` (the full
+`+--safe --without-K+` type-check) locally, and open a PR. Proofs are
+load-bearing — a red `+agda+` check blocks merge, and no `+postulate+` /
+`+believe_me+` shortcuts are accepted.
+
+=== Build and check
+
+There is exactly one thing to run, and it must stay green:
+
+....
+just check
+....
+
+which is:
+
+....
+agda --no-libraries -i src src/EpistemicTypes/All.agda
+....
+
+Requirements:
+
+* *Agda 2.8.0*.
+* *No Agda standard library.* The build runs with `+--no-libraries+`;
+the only imports allowed are from `+Agda.Builtin.*+` and
+`+Agda.Primitive+`. Do not add a dependency on `+agda-stdlib+` or any
+other library.
+
+`+All.agda+` re-exports every module, so `+just check+` checks the whole
+library. A change is not done until `+just check+` passes with no errors
+and no warnings.
+
+There is no CI (see `+AUDIT.adoc+` / repo notes — CI is not enabled).
+The type-checker run above is the gate. Run it locally before opening a
+PR.
+
+'''''
+
+=== The honesty rules
+
+These are non-negotiable. A PR that breaks any of them will not be
+merged.
+
+* *No `+postulate+`.* Nothing is asserted without proof. If a law holds,
+prove it; if it does not, it is not stated as if it did. Where a law is
+not derivable but is needed, it appears as an explicit _field_ the
+caller must supply (see `+LawfulModality+`, `+FactiveModality+`,
+`+BeliefModality+`), so the assumption is visible at the type level
+rather than smuggled in.
+* *No standard library.* As above: `+Agda.Builtin.*+` and
+`+Agda.Primitive+` only.
+* *`+--safe --without-K+`.* Every module compiles under
+`+{-# OPTIONS --safe --without-K #-}+`. This rules out `+postulate+`,
+unsafe pragmas, axiom K, and `+--type-in-type+`. Do not weaken these
+options.
+* *No too-strong rules.* Keep the interfaces as weak as the proofs
+allow. The base form `+E : K → Set ℓ → Set ℓ+` is a plain indexed
+endofunctor (`+map+` only) — it is *not* a monad or comonad, and there
+is no generic `+return+`/`+reflect+`. Do not promote it to one. If
+something needs more structure, add a _named_ stronger interface
+(e.g. `+ReturnModality+`) that callers opt into, and keep the base
+interface untouched.
+* *Add lemmas with proofs, not admits.* New results land as complete
+proofs closed with normal Agda terms. No holes (`+?+`), no admit-shaped
+escapes, no `+TERMINATING+`/`+NON_COVERING+` pragmas to paper over gaps.
+
+==== Keep the bridges distinct
+
+The library is careful about what is and is not the same thing. Preserve
+these separations when extending:
+
+* `+Echo r A+` (the min-plus graded loss/residue in `+EchoBridge+`) is
+*not* `+E κ A+`. Keep the echo bridge separate; do not collapse it into
+the modality, and do not import a full graded comonad to get it.
+* In `+ProofTransport+`, the no-smuggling discipline is the point:
+`+transmit+` downgrades a sender’s `+Proof+` to a receiver’s
+`+Receipt+`; `+verify+` upgrades `+Data → Proof+` only with the
+receiver’s *own* checker and evidence; public proofs are portable,
+designated ones are receiver-bound, and a receipt alone never certifies
+(`+proofNeedsChecker+`). Any new transport rule must respect these — no
+rule that lets one agent’s `+Proof+` become another’s without the
+receiver’s own checker.
+
+'''''
+
+=== Adding a module or lemma
+
+[arabic]
+. Put Agda source under `+src/EpistemicTypes/+` and add the new module
+to the `+import+`/re-export list in `+src/EpistemicTypes/All.agda+` so
+`+just check+` covers it.
+. Open each module with `+{-# OPTIONS --safe --without-K #-}+`.
+. Keep modules small and single-purpose, mirroring the existing layout:
+`+Base+`, `+Warrant+`, `+Access+`, `+EchoBridge+`, `+SurrealBridge+`,
+`+ProofTransport+`, `+ProofTransportExample+`, `+Examples+`.
+. State assumptions as interface fields, not postulates. Add lawful
+instances only after the laws are proved or explicitly required as
+fields.
+. Run `+just check+`.
+
+If a change touches the ProofTransport engineering rendering (the
+a2ml/k9 attestation target under
+`+.machine_readable/proof-transport/+`), keep the Agda model and the
+machine-readable description in step.
+
+'''''
+
+=== Documentation
+
+* *AsciiDoc (`+.adoc+`) is the default* for documentation. Update the
+relevant `+.adoc+` file alongside any behavioural or interface change.
+* Existing docs keep their current lowercase names: `+readme.adoc+` and
+`+explainme.adoc+`. Do *not* rename or duplicate them.
+* Machine-readable descriptions live under `+.machine_readable/+` (a2ml
++ Nickel/k9). a2ml files use the canonical TOML-like dialect:
+`+[section]+` headers, `+key = "value"+`, arrays `+[ "a", "b" ]+`,
+inline tables `+{ k = "v", j = "w" }+`.
+* Only these files may be Markdown (GitHub community-health
+special-casing): `+CONTRIBUTING.md+`, `+CODE_OF_CONDUCT.md+`,
+`+SECURITY.md+`, `+CHANGELOG.md+`. Everything else is `+.adoc+`.
+
+'''''
+
+=== Commits and pull requests
+
+==== Branch naming
+
+....
+feat/short-description    # new module, interface, or lemma
+fix/short-description     # corrected proof or definition
+docs/short-description    # .adoc / machine-readable docs
+refactor/short-description
+....
+
+==== Conventional Commits
+
+Commit messages follow https://www.conventionalcommits.org/[Conventional
+Commits]:
+
+....
+<type>(<scope>): <description>
+
+[optional body]
+
+[optional footer]
+....
+
+Typical scopes match the modules: `+base+`, `+warrant+`, `+access+`,
+`+echo+`, `+surreal+`, `+proof-transport+`, `+docs+`.
+
+==== Signed commits
+
+All commits must be *signed*. Use the existing SSH/GPG signing key; do
+not create new keys. Verify with:
+
+....
+git log --show-signature
+....
+
+Unsigned commits will be asked to be re-signed before merge.
+
+==== Before you open a PR
+
+[arabic]
+. `+just check+` passes — no errors, no warnings.
+. No `+postulate+`, no library imports, no `+?+`/admits, no weakened
+pragmas.
+. The honesty rules above still hold (weak base interface, distinct
+bridges, no proof-smuggling in transport).
+. Relevant `+.adoc+` and `+.machine_readable/+` files updated.
+. Commits are conventional and signed.
+
+Keep PRs small and focused — one idea, one proof obligation, easy to
+check.
+
+'''''
+
+=== Licence note
+
+The licence is owner-managed. Do *not* add `+LICENSE+`,
+`+SPDX-License-Identifier+` headers, or copyright header lines in a PR.
+The repo is currently SPDX-free and stays consistent; licensing is
+handled separately by the owner.
+
+'''''
+
+=== Ecosystem siblings
+
+`+epistemic-types+` sits alongside (and should stay coherent with) these
+estate repos:
+
+* *echo-types* — Agda loss-with-residue formalism; `+EchoBridge+`
+composes with it. Audit it before duplicating echo machinery here.
+* *ephapax* — sibling formal language (four-layer redesign with echo
+obligations).
+* *standards* — estate RSR/standards, k9-svc, and a2ml tooling.
+* *a2ml / k9* — machine-readable + contractile tooling; the engineering
+target for `+ProofTransport+`.
+
+When a contribution overlaps a sibling (especially echo-types), prefer
+reusing or extending it upstream over re-deriving it locally.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
deleted file mode 100644
index 04694c9..0000000
--- a/CONTRIBUTING.md
+++ /dev/null
@@ -1,213 +0,0 @@
-# Contributing to epistemic-types
-
-`epistemic-types` is a small, deliberately honest Agda formalization of
-standpoint-indexed modal / epistemic / echo-like type formers. It favours
-mathematical honesty over a large API. Contributions are welcome, but the bar
-is **everything still type-checks under `--safe --without-K`, with no shortcuts**.
-
-- **Author:** Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-- **Version:** 0.1.0 (status: prototype)
-- **Last updated:** 2026-06-15
-
----
-
-## Contribution model — Tri-Perimeter Contribution Framework (TPCF)
-
-epistemic-types follows the estate-wide **Tri-Perimeter Contribution Framework (TPCF)** — graduated trust without gatekeeping:
-
-- **Perimeter 1 — Core Systems (maintainers only).** The proof kernel:
-  `src/EpistemicTypes/*.agda` (Base, Access, Warrant, ProofTransport, the
-  EchoBridge/SurrealBridge), the `All.agda` wiring, and build tooling.
-- **Perimeter 2 — Expert Extensions (trusted contributors).** New
-  epistemic/standpoint modules, examples, and bridges. Apply via issue → review
-  → merge, with `just check` green.
-- **Perimeter 3 — Community Sandbox (open to all).** Docs (`.adoc`),
-  `.well-known/`, AI manifests, spec proposals.
-
-### Fork workflow
-
-External contributors use the standard **fork**-and-pull-request workflow: fork
-the repository, branch from `main`, run `just check` (the full `--safe
---without-K` type-check) locally, and open a PR. Proofs are load-bearing — a red
-`agda` check blocks merge, and no `postulate` / `believe_me` shortcuts are
-accepted.
-
-## Build and check
-
-There is exactly one thing to run, and it must stay green:
-
-```
-just check
-```
-
-which is:
-
-```
-agda --no-libraries -i src src/EpistemicTypes/All.agda
-```
-
-Requirements:
-
-- **Agda 2.8.0**.
-- **No Agda standard library.** The build runs with `--no-libraries`; the only
-  imports allowed are from `Agda.Builtin.*` and `Agda.Primitive`. Do not add a
-  dependency on `agda-stdlib` or any other library.
-
-`All.agda` re-exports every module, so `just check` checks the whole library.
-A change is not done until `just check` passes with no errors and no warnings.
-
-There is no CI (see `AUDIT.adoc` / repo notes — CI is not enabled). The
-type-checker run above is the gate. Run it locally before opening a PR.
-
----
-
-## The honesty rules
-
-These are non-negotiable. A PR that breaks any of them will not be merged.
-
-- **No `postulate`.** Nothing is asserted without proof. If a law holds, prove
-  it; if it does not, it is not stated as if it did. Where a law is not
-  derivable but is needed, it appears as an explicit *field* the caller must
-  supply (see `LawfulModality`, `FactiveModality`, `BeliefModality`), so the
-  assumption is visible at the type level rather than smuggled in.
-- **No standard library.** As above: `Agda.Builtin.*` and `Agda.Primitive` only.
-- **`--safe --without-K`.** Every module compiles under
-  `{-# OPTIONS --safe --without-K #-}`. This rules out `postulate`, unsafe
-  pragmas, axiom K, and `--type-in-type`. Do not weaken these options.
-- **No too-strong rules.** Keep the interfaces as weak as the proofs allow. The
-  base form `E : K → Set ℓ → Set ℓ` is a plain indexed endofunctor (`map` only)
-  — it is **not** a monad or comonad, and there is no generic `return`/`reflect`.
-  Do not promote it to one. If something needs more structure, add a *named*
-  stronger interface (e.g. `ReturnModality`) that callers opt into, and keep the
-  base interface untouched.
-- **Add lemmas with proofs, not admits.** New results land as complete proofs
-  closed with normal Agda terms. No holes (`?`), no admit-shaped escapes, no
-  `TERMINATING`/`NON_COVERING` pragmas to paper over gaps.
-
-### Keep the bridges distinct
-
-The library is careful about what is and is not the same thing. Preserve these
-separations when extending:
-
-- `Echo r A` (the min-plus graded loss/residue in `EchoBridge`) is **not**
-  `E κ A`. Keep the echo bridge separate; do not collapse it into the modality,
-  and do not import a full graded comonad to get it.
-- In `ProofTransport`, the no-smuggling discipline is the point: `transmit`
-  downgrades a sender's `Proof` to a receiver's `Receipt`; `verify` upgrades
-  `Data → Proof` only with the receiver's **own** checker and evidence; public
-  proofs are portable, designated ones are receiver-bound, and a receipt alone
-  never certifies (`proofNeedsChecker`). Any new transport rule must respect
-  these — no rule that lets one agent's `Proof` become another's without the
-  receiver's own checker.
-
----
-
-## Adding a module or lemma
-
-1. Put Agda source under `src/EpistemicTypes/` and add the new module to the
-   `import`/re-export list in `src/EpistemicTypes/All.agda` so `just check`
-   covers it.
-2. Open each module with `{-# OPTIONS --safe --without-K #-}`.
-3. Keep modules small and single-purpose, mirroring the existing layout:
-   `Base`, `Warrant`, `Access`, `EchoBridge`, `SurrealBridge`, `ProofTransport`,
-   `ProofTransportExample`, `Examples`.
-4. State assumptions as interface fields, not postulates. Add lawful instances
-   only after the laws are proved or explicitly required as fields.
-5. Run `just check`.
-
-If a change touches the ProofTransport engineering rendering (the a2ml/k9
-attestation target under `.machine_readable/proof-transport/`), keep the Agda
-model and the machine-readable description in step.
-
----
-
-## Documentation
-
-- **AsciiDoc (`.adoc`) is the default** for documentation. Update the relevant
-  `.adoc` file alongside any behavioural or interface change.
-- Existing docs keep their current lowercase names: `readme.adoc` and
-  `explainme.adoc`. Do **not** rename or duplicate them.
-- Machine-readable descriptions live under `.machine_readable/` (a2ml +
-  Nickel/k9). a2ml files use the canonical TOML-like dialect: `[section]`
-  headers, `key = "value"`, arrays `[ "a", "b" ]`, inline tables
-  `{ k = "v", j = "w" }`.
-- Only these files may be Markdown (GitHub community-health special-casing):
-  `CONTRIBUTING.md`, `CODE_OF_CONDUCT.md`, `SECURITY.md`, `CHANGELOG.md`.
-  Everything else is `.adoc`.
-
----
-
-## Commits and pull requests
-
-### Branch naming
-
-```
-feat/short-description    # new module, interface, or lemma
-fix/short-description     # corrected proof or definition
-docs/short-description    # .adoc / machine-readable docs
-refactor/short-description
-```
-
-### Conventional Commits
-
-Commit messages follow [Conventional Commits](https://www.conventionalcommits.org/):
-
-```
-<type>(<scope>): <description>
-
-[optional body]
-
-[optional footer]
-```
-
-Typical scopes match the modules: `base`, `warrant`, `access`, `echo`,
-`surreal`, `proof-transport`, `docs`.
-
-### Signed commits
-
-All commits must be **signed**. Use the existing SSH/GPG signing key; do not
-create new keys. Verify with:
-
-```
-git log --show-signature
-```
-
-Unsigned commits will be asked to be re-signed before merge.
-
-### Before you open a PR
-
-1. `just check` passes — no errors, no warnings.
-2. No `postulate`, no library imports, no `?`/admits, no weakened pragmas.
-3. The honesty rules above still hold (weak base interface, distinct bridges,
-   no proof-smuggling in transport).
-4. Relevant `.adoc` and `.machine_readable/` files updated.
-5. Commits are conventional and signed.
-
-Keep PRs small and focused — one idea, one proof obligation, easy to check.
-
----
-
-## Licence note
-
-The licence is owner-managed. Do **not** add `LICENSE`,
-`SPDX-License-Identifier` headers, or copyright header lines in a PR. The repo
-is currently SPDX-free and stays consistent; licensing is handled separately by
-the owner.
-
----
-
-## Ecosystem siblings
-
-`epistemic-types` sits alongside (and should stay coherent with) these estate
-repos:
-
-- **echo-types** — Agda loss-with-residue formalism; `EchoBridge` composes with
-  it. Audit it before duplicating echo machinery here.
-- **ephapax** — sibling formal language (four-layer redesign with echo
-  obligations).
-- **standards** — estate RSR/standards, k9-svc, and a2ml tooling.
-- **a2ml / k9** — machine-readable + contractile tooling; the engineering target
-  for `ProofTransport`.
-
-When a contribution overlaps a sibling (especially echo-types), prefer reusing
-or extending it upstream over re-deriving it locally.
diff --git a/SECURITY.adoc b/SECURITY.adoc
new file mode 100644
index 0000000..f06be9f
--- /dev/null
+++ b/SECURITY.adoc
@@ -0,0 +1,109 @@
+== Security Policy
+
+_Last updated: 2026-06-15 — version 0.1.0 (prototype)_
+
+=== Scope and threat model
+
+`+epistemic-types+` (`+hyperpolymath/epistemic-types+`) is a small Agda
+formalization of standpoint-indexed modal / epistemic / echo-like type
+formers. It is a single-tool, library-only project:
+
+* *No runtime.* There is no executable, server, daemon, or service. The
+only "`execution`" is Agda type-checking the source.
+* *No network, no secrets, no I/O.* The library reads no input and
+writes no output beyond what the type-checker reports.
+* *No dependencies.* It compiles under
+`+{-# OPTIONS --safe --without-K #-}+` with *no postulates* and *no Agda
+standard library* (built with `+agda --no-libraries+`, using only
+`+Agda.Builtin.*+` / `+Agda.Primitive+`).
+
+Because there is no runtime surface, the meaningful "`attack surface`"
+is the *proofs and machine-readable specifications themselves*. A
+security-relevant defect here is essentially a _soundness_ defect — for
+example:
+
+* a proof that type-checks but encodes a false or misleading claim;
+* an unintended use of a postulate, `+--type-in-type+`, an `+unsafe+`
+pragma, or some other escape hatch that would weaken the
+`+--safe --without-K+` guarantee;
+* a flaw in the `+ProofTransport+` discipline that lets an attestation
+claim more than it should — e.g. something that lets a receiver-bound
+(designated) proof be treated as portable, or a receipt-only artifact be
+treated as a certifying proof, contrary to the `+proofNeedsChecker+`
+"`no-smuggling`" invariant. The same applies to the `+EchoBridge+`
+graded loss/residue accounting and the `+SurrealBridge+` birthday-tower
+carriers.
+* a divergence between the Agda formalization and its engineering
+rendering in `+.machine_readable/proof-transport/+` (a2ml / Nickel-k9)
+that would let the machine-readable spec be read as guaranteeing
+something the proofs do not.
+
+Plain typos, broken imports, or build breakage are ordinary bugs, not
+security issues — please raise those as normal issues rather than via
+this policy.
+
+=== Reporting a vulnerability
+
+If you believe you have found a soundness or attestation-discipline
+defect of the kind above, please report it *privately first*:
+
+* *Preferred:* open a
+https://github.com/hyperpolymath/epistemic-types/security/advisories/new[GitHub
+security advisory] (private) on `+hyperpolymath/epistemic-types+`.
+* *Alternatively:* email *Jonathan D.A. Jewell (hyperpolymath)* at
+*j.d.a.jewell@open.ac.uk* with `+[epistemic-types security]+` in the
+subject.
+
+Please include the affected module(s) and a minimal Agda snippet (or a
+machine-readable excerpt) that demonstrates the issue, if you can.
+
+=== Response expectations
+
+This is a prototype maintained by a single author, so timelines are
+best-effort rather than contractual:
+
+* *Acknowledgement:* within 7 days.
+* *Initial assessment:* within 30 days.
+* *Fix or documented decision:* as soon as practicable thereafter.
+Because the remedy for a soundness defect is usually to _correct or
+withdraw a claim_ rather than ship a patch to running software, the
+resolution may take the form of a documentation correction, a proof
+revision, or an honest note that a stated property does not hold.
+
+There is no automated CI on this repository (see `+AUDIT.adoc+`), so
+verification is manual: the canonical check is
+
+....
+just check   # == agda --no-libraries -i src src/EpistemicTypes/All.agda
+....
+
+with *Agda 2.8.0*.
+
+=== Supported versions
+
+[cols=",,",options="header",]
+|===
+|Version |Status |Supported
+|`+main+` |active |yes
+|`+0.1.0+` |prototype |yes (current)
+|===
+
+Only the latest state of `+main+` and the current `+0.1.0+` prototype
+are maintained. There are no prior released versions to back-port to.
+
+=== Coordinated disclosure
+
+Please give a reasonable opportunity to assess and correct an issue
+before disclosing it publicly. Good-faith research that follows this
+policy is welcome; there will be no legal action against researchers who
+report responsibly and avoid privacy violations or destructive testing.
+
+=== Related projects
+
+Findings here may also be relevant to sibling formal-methods work in the
+estate — in particular `+echo-types+` (the loss-with-residue formalism
+that `+EchoBridge+` composes with), `+ephapax+` (sibling formal language
+with echo obligations), and the `+standards+` / `+a2ml+` / `+k9+`
+tooling that `+ProofTransport+`’s machine-readable rendering targets.
+Where appropriate, a report against one may be cross-referenced to the
+others.
diff --git a/SECURITY.md b/SECURITY.md
deleted file mode 100644
index ed83181..0000000
--- a/SECURITY.md
+++ /dev/null
@@ -1,100 +0,0 @@
-# Security Policy
-
-_Last updated: 2026-06-15 — version 0.1.0 (prototype)_
-
-## Scope and threat model
-
-`epistemic-types` (`hyperpolymath/epistemic-types`) is a small Agda
-formalization of standpoint-indexed modal / epistemic / echo-like type
-formers. It is a single-tool, library-only project:
-
-- **No runtime.** There is no executable, server, daemon, or service. The
-  only "execution" is Agda type-checking the source.
-- **No network, no secrets, no I/O.** The library reads no input and writes
-  no output beyond what the type-checker reports.
-- **No dependencies.** It compiles under `{-# OPTIONS --safe --without-K #-}`
-  with **no postulates** and **no Agda standard library** (built with
-  `agda --no-libraries`, using only `Agda.Builtin.*` / `Agda.Primitive`).
-
-Because there is no runtime surface, the meaningful "attack surface" is the
-**proofs and machine-readable specifications themselves**. A security-relevant
-defect here is essentially a *soundness* defect — for example:
-
-- a proof that type-checks but encodes a false or misleading claim;
-- an unintended use of a postulate, `--type-in-type`, an `unsafe` pragma, or
-  some other escape hatch that would weaken the `--safe --without-K`
-  guarantee;
-- a flaw in the `ProofTransport` discipline that lets an attestation claim
-  more than it should — e.g. something that lets a receiver-bound (designated)
-  proof be treated as portable, or a receipt-only artifact be treated as a
-  certifying proof, contrary to the `proofNeedsChecker` "no-smuggling"
-  invariant. The same applies to the `EchoBridge` graded loss/residue
-  accounting and the `SurrealBridge` birthday-tower carriers.
-- a divergence between the Agda formalization and its engineering rendering in
-  `.machine_readable/proof-transport/` (a2ml / Nickel-k9) that would let the
-  machine-readable spec be read as guaranteeing something the proofs do not.
-
-Plain typos, broken imports, or build breakage are ordinary bugs, not security
-issues — please raise those as normal issues rather than via this policy.
-
-## Reporting a vulnerability
-
-If you believe you have found a soundness or attestation-discipline defect of
-the kind above, please report it **privately first**:
-
-- **Preferred:** open a [GitHub security advisory](https://github.com/hyperpolymath/epistemic-types/security/advisories/new)
-  (private) on `hyperpolymath/epistemic-types`.
-- **Alternatively:** email **Jonathan D.A. Jewell (hyperpolymath)** at
-  **j.d.a.jewell@open.ac.uk** with `[epistemic-types security]` in the
-  subject.
-
-Please include the affected module(s) and a minimal Agda snippet (or a
-machine-readable excerpt) that demonstrates the issue, if you can.
-
-## Response expectations
-
-This is a prototype maintained by a single author, so timelines are
-best-effort rather than contractual:
-
-- **Acknowledgement:** within 7 days.
-- **Initial assessment:** within 30 days.
-- **Fix or documented decision:** as soon as practicable thereafter. Because
-  the remedy for a soundness defect is usually to *correct or withdraw a
-  claim* rather than ship a patch to running software, the resolution may take
-  the form of a documentation correction, a proof revision, or an honest
-  note that a stated property does not hold.
-
-There is no automated CI on this repository (see `AUDIT.adoc`), so
-verification is manual: the canonical check is
-
-```
-just check   # == agda --no-libraries -i src src/EpistemicTypes/All.agda
-```
-
-with **Agda 2.8.0**.
-
-## Supported versions
-
-| Version    | Status    | Supported            |
-| ---------- | --------- | -------------------- |
-| `main`     | active    | yes                  |
-| `0.1.0`    | prototype | yes (current)        |
-
-Only the latest state of `main` and the current `0.1.0` prototype are
-maintained. There are no prior released versions to back-port to.
-
-## Coordinated disclosure
-
-Please give a reasonable opportunity to assess and correct an issue before
-disclosing it publicly. Good-faith research that follows this policy is
-welcome; there will be no legal action against researchers who report
-responsibly and avoid privacy violations or destructive testing.
-
-## Related projects
-
-Findings here may also be relevant to sibling formal-methods work in the
-estate — in particular `echo-types` (the loss-with-residue formalism that
-`EchoBridge` composes with), `ephapax` (sibling formal language with echo
-obligations), and the `standards` / `a2ml` / `k9` tooling that
-`ProofTransport`'s machine-readable rendering targets. Where appropriate, a
-report against one may be cross-referenced to the others.