Epistemic Types — Standpoint-Indexed Modalities and Proof Transport

Constructive Agda prototype for standpoint-indexed epistemic modalities, separating knowledge, belief, and warrant, with proof transport sound relative to an explicit claim meaning.

Contents

• Overview
• The modality spectrum
• Warrants
• Accessibility and surreal standpoints
  • The surreal bridge
• Store-coherent reads and certified residues
• Proof transport across trust boundaries
• What is standard and what is ours
• What remains intentionally unformalized
• Build
• Documentation
• License

Overview

When an agent observes a fact, the type of their access matters. Knowledge is factive; belief is not. A warrant records evidence without assuming soundness. Proof transported across a boundary becomes a receipt; a receiving proof requires a successful sound check of the receiver’s claim meaning.

Epistemic types provide a mechanised vocabulary for these distinctions. Given a type of standpoints K (agents, observers, evidence states), the modality E : K → Set ℓ → Set ℓ reads: E κ A is the type of A as epistemically available from standpoint κ.

This repo does not define a complete epistemic logic or Kripke semantics. It provides the minimal interfaces — factive vs. non-factive modalities, warrants, accessibility preorder, and compositional proof transport — and proves the structural laws that hold generically, while making explicit what must be assumed.

The modality spectrum

The base interface treats E as an indexed endofunctor. Stronger structure is added incrementally, each as a separate record:

Interface	Structure added	Intended reading
Modality	E, map	Plain indexed endofunctor
LawfulModality	Functor identity + composition laws	map respects structure
FactiveModality	reflect : E κ A → A	Knowledge (veridical: what is available is true)
BeliefModality	Intentionally no reflect	Belief (non-factive: available does not imply true)
ReturnModality	return : A → E κ A	Strong introduction (internal observation)

Monadic (bind) and comonadic (extract) structure are not provided by default. They are future commitments, not hidden assumptions.

Warrants

A warrant records the type of evidence for a claim without assuming the evidence is valid:

• Warrant κ A — the type of evidence tokens for A from standpoint κ.

• Epi κ A — an evidence token paired with its warrant type.

• SoundWarrant — a separate interface adding a soundness map (evidence → A). Not assumed by default.

This separates "I have a receipt for A" from "A is true."

Accessibility and surreal standpoints

Standpoint access is modelled by a preorder κ ≤κ κ' (read: κ' is at least as informed as κ). Transport increase moves epistemic availability along this order.

The surreal bridge

SurrealBridge enriches the preorder with an instance-supplied access grade. Its laws specify composition; they do not establish a physical cost or an information-loss measure:

magnitude-loss : x ≤♯ y → Grade
loss-refl      : magnitude-loss refl ≡ finite zero
loss-trans     : magnitude-loss (trans p q) ≡ gradePlus (magnitude-loss p) (magnitude-loss q)

Its concrete Echo adapter relaxes a proved upper bound on a residue measure along p : x ≤♯ y, while preserving the retained value:

E x (BoundedEcho C measure r visible)
  → E y (BoundedEcho C measure (gradePlus r (magnitude-loss p)) visible)

The concrete daySurrealAccess instance models the finite birthday tower using Nat standpoints, where the grade is the number of refinement steps. This is a set-sized fragment, not the full Conway proper class of surreals.

Store-coherent reads and certified residues

ReadConsistency now models finite store histories. A ReadView s proves its value equals contents s; a cached read records its source history and ancestry. Writes make existing caches stale. synchronize reads current contents in the model, while preserving evidence across a change requires an explicit proof. The former version-only relabelling and free Sync witness have been removed.

Echo C y carries a residue satisfying the relation specified by Retention C. Source compatibility is explicit in MatchesSource; exact recovery and migration need their respective round-trip and adequacy laws. A checked counterexample shows that discarded distinctions cannot support a migration requiring those distinctions. Resource grades are separate, measured upper bounds.

See the breaking API correction and proof boundaries. An optional integration gate proves correspondence with the actual sibling EchoResidue.EchoR; the core remains dependency-free.

Proof transport across trust boundaries

ProofTransport is parameterised by agents, claim labels, artefacts, Meaning : Agent → Artifact → Claim → Set, and a certificate Payload : Artifact → Claim → Set. The caller states the meaning being proved.

A CertificateCheck contains an executable Boolean check and a proof that acceptance entails that exact meaning. Evidence carries a payload; possessing it alone proves nothing. A proof constructor also requires runChecker checker evidence ≡ true.

proofSound : View holder a Proof c -> Meaning holder a c

verify evaluates the checking function and returns InvalidEvidence on rejection. transmit produces a receipt at the receiving holder. publicIsPortable requires an explicit implication between the two holders' meanings; it does not silently relabel holder-dependent truths.

The example checks Boolean artefacts and certificates, proves legitimate acceptance, and refutes false claims. It does not claim that a physical action occurred. The older token-only model lacked semantic soundness; the strengthened interface is a breaking correction documented in docs/proof-transport.adoc.

What is standard and what is ours

Concept	Status	Home in this repo
Indexed endofunctor / modality	Standard	EpistemicTypes.Base
Knowledge (factivity) vs. Belief distinction	Standard (modal logic S5 vs. KD45)	EpistemicTypes.Base
Warrant types without assumed soundness	Project-specific emphasis	EpistemicTypes.Warrant
Preorder accessibility with transport	Standard	EpistemicTypes.Access
Resource-bound transport on surreal-like standpoints	Project-specific composition; no novelty theorem	EpistemicTypes.SurrealBridge
Proof transport with explicit semantic soundness	Novel formalisation	EpistemicTypes.ProofTransport

What remains intentionally unformalized

Caution

This is a prototype, not a complete epistemic logic. The following are intentionally omitted as future commitments, not hidden assumptions:

• Complete epistemic logic or Kripke semantics

• Graded comonad for echo-type composition

• Proof irrelevance or decidability

• Global soundness of warrants

• Monadic (bind) or comonadic (extract) structure for E

Build

just check  # positive proofs and expected rejection controls

Or directly:

agda --no-libraries -i src src/EpistemicTypes/All.agda

Documentation

• EXPLAINME — claim-by-claim receipts and known gaps

• Continuity foundations — store coherence, retained information, bounds, and next obligations

• Proof transport — semantic verification across boundaries

License

SPDX-License-Identifier: MPL-2.0 — see LICENSE.