feat(display): add responder coalgebras

[quangvdao]

Motivation and context

This is G1 of the Aberlé general-theory stack, based directly on #75 (which is
itself stacked on #74). #74 introduces PFunctor.Display, the intrinsic
dependent-polynomial layer over a base polynomial. This PR supplies the first
coalgebraic application of that layer: proof-relevant responder contracts in
the exact local form used by Aberlé's Agda DepMealy.appD.

The key distinction is variance. For a display S over a query interface
P, a verified responder does not choose a precondition witness. Its caller
supplies c : S.position a; the responder returns evidence that its committed
answer satisfies S.direction a c ..., together with a recursively preserved
state witness. Capturing that dependency correctly is what makes the API
useful for the later dependent-program and coinductive-behavior slices.

What this PR adds

Generic displayed coalgebras

Display.Coalgebra S step F is the transparent abbreviation

(state : C) → F state → S.Obj F (step state)

It deliberately does not bundle or duplicate the base coalgebra. For a
Responder C P, it is applied directly to the existing R.out map.

The responder display

Display.responder S lies over the existing responder interface P ⊸ X.
Above an answer section, its data are

position answer :=
  (a : P.A) → (c : S.position a) →
    S.direction a c (answer a)

direction _answer _post query := S.position query.1

Thus a displayed position gives answer-dependent post-evidence for every
query and supplied pre-witness, while the displayed direction retains that
pre-witness for the recursively verified continuation.

responderChart is the canonical covariant chart that forgets this evidence.

Exact local dependent-Mealy interface

responderCoalgebraEquiv identifies a generic displayed coalgebra over
R.out with the literal local obligation

(state : C) → F state →
  (a : P.A) → (c : S.position a) →
    S.direction a c (R.answer state a) × F (R.next state a)

This is the state-presented, one-step form of the Agda declaration

appD : (a) → (c : S.position a) →
  S.direction a c (answer a) × DepMealy next

Both directions of the equivalence have simp-normal projection equations for
the postcondition and continuation components.

Relationship to existing PolyFun abstractions

• Display is intrinsic dependent-polynomial data over one PFunctor.
  Display.Coalgebra preserves a proof-relevant family through one base
  coalgebra step.
• The existing Displayed namespace concerns algebras, folds, and
  decorations indexed over already-built Free trees. It remains the right
  layer for the later applications, but it is not the representation of the
  dependent polynomial itself.
• This is not DynSystem.SafetyRefinement: that API is proposition-valued and
  relational between two systems. Here the contract is proof-relevant and
  intrinsic to one responder.
• The existing Responder / DynSystem state presentation is reused; no
  second verified-machine structure or paper-specific alias is introduced.

Tests and falsifiable canaries

The tests include:

• two queries with genuinely different response types;
• query-dependent precondition types and response-dependent post-evidence;
• a proof-relevant state family Fin (state + 1);
• an empty precondition fiber, demonstrating that the universally quantified
  paper obligation is vacuously inhabited and does not manufacture evidence;
• a Bool precondition whose returned next witness differs with the supplied
  Bool, detecting accidental erasure of continuation dependence;
• forward and inverse use of the direct paper-shaped equivalence; and
• independently separated universes for interface positions, responses,
  display positions, display directions, states, and state witnesses.

Alternatives rejected and implementation findings

The first draft used Σ c : S.position a, ... for responder positions and
PUnit for displayed directions. Independent review found that this reverses
the paper's precondition variance: it chooses one witness instead of accepting
every caller-supplied witness, and forces one shared continuation per query.
An empty precondition fiber is a minimal counterexample.

That initial representation also appeared to admit a stronger forgetting
Lens. The corrected representation shows why no such lens exists in
general: lifting a bare query contravariantly would require inventing an
element of S.position a, which may be empty. The invalid lens and all of its
laws were removed; the covariant chart is the correct general projection.

This finding changes the later coinductive-behavior design: it must construct
a genuinely displayed/coinductive fiber over fixed base behavior, rather than
using a fiber of M.mapLens induced by a nonexistent total-to-base lens.

Deliberate non-goals

• No coinductive/greatest-fixed-point DepMealy object yet; that belongs to
  the later behavior slice.
• No dependent free-program composition or handler wiring; those are separate
  G2/G3 slices.
• No aliases copied from the paper when existing PolyFun abstractions already
  express the concept.
• No claim that arbitrary evidence-forgetting charts can be strengthened to
  lenses.

Stack and validation

• Base: refactor(displayed): use algebra terminology #75 at 9f68b3da59b3bf59c38527415164dd2f1ebd0c1f
• Head: 53aa6cdd937075704f5bf3e423a6642ce904d755
• One commit; no dependency on the other open theory/application trains.
• ./scripts/validate.sh --lint --test: passed on the exact head (8832 project
  jobs, umbrella-import and documentation checks, environment lint, and all
  1970 test jobs).
• lake exe lint-style, lake lint, and git diff --check: passed.
• Independent review-lean-formalization review: the initial variance and
  lens findings were resolved, and the exact-head closure pass reported no
  remaining actionable findings.

Final restack and audit (2026-07-19)

This final record supersedes earlier candidate SHA and count language above.

• Exact base: 9f68b3da59b3bf59c38527415164dd2f1ebd0c1f (refactor(displayed): use algebra terminology #75)
• Exact head: 53aa6cdd937075704f5bf3e423a6642ce904d755
• Shape: 1 commit; 7 files; 430 additions; 5 deletions
• State: Ready, clean/mergeable, open, intentionally unmerged

The final exact-head review reconfirmed that Display.Coalgebra is the correct transparent generic layer, while Display.responder and responderCoalgebraEquiv are the responder specialization with caller-supplied precondition variance. Empty-fiber and Boolean-continuation canaries reject evidence erasure or existential variance. No universe coupling or duplicate bundle remains.

Fresh ./scripts/validate.sh --lint --test passed at this head: 8,840 build jobs, generated imports, docs integrity, environment lint, and the full test library. Style, diff, trust, and axiom audits pass. Hosted style and summary pass; the full local validator is authoritative for this non-default stacked base.

[dtumad]

Reviewed the responder coalgebra variance and dependent evidence flow. A displayed position supplies post-evidence from query plus pre-evidence, while directions retain the supplied evidence; the coalgebra equivalence correctly packages answer and next witness. Empty and dependent examples cover the delicate cases. No blocking findings.

[dtumad]

Re-reviewed the clean restack. Range-diff is patch-identical to the previously approved unique commit series, now based on the reconstructed #75 head.

[dtumad]

Approval renewed after GitHub merged current main into the patch-identical restack; the endpoint diff remains the previously reviewed isolated change.