Axes engaged: 7 (PR/PI). See README.adoc § "Axis coverage matrix".
Verdict: distinct against propositional-predicate variants;
co-extensive with Σ-relevant variants. The honest claim is
narrower than the consolidated doc previously suggested. Truncation
argument formalised on three domains via echo-not-prop.
The previous consolidated doc said: "Refinement types refine inputs; Echo refines outputs. Different direction." This is not the load-bearing distinction. The load-bearing distinction is between two implementations of refinement:
-
Σ-relevant refinement. In Agda, Coq, and other dependently- typed languages where the predicate is a
Set, the refinement type{ x : A | P x }literally isΣ A P. WithP x := f x ≡ y, this isEcho f y. No win for echo. -
Propositional-predicate refinement. In F\*, Liquid Haskell, and other systems where the predicate is a propositional / SMT constraint, the refinement type is the propositional truncation of
Σ A P. The truncation discards individual witness identity. Echo wins here, formally certified byecho-not-prop.
Stating the claim narrowly is stronger than overstating it. The narrow claim survives scrutiny; the overstated claim doesn’t.
Echo coincides with Σ-relevant refinement types and is therefore
not distinct from them. Echo wins against propositional-predicate
refinement types via the truncation argument: echo-not-prop
certifies that propositional truncation loses what echo retains.
Formalised on three domains by gate-3’s canonical examples, each of which tests against refinement types explicitly:
-
TropicalArgmin— tie multiplicity at the optimum. Two argmin paths exist; truncation collapses them.echo-not-propcertifies non-truncatability. -
EpistemicUpdate— multiple consistent worlds. Truncation loses individual world identity, breakingrefine-injective. -
LinearErasure— multiple mode annotations consistent with one erasure. Truncation loses the linearity distinction.
Gate-3’s framing per example: "in Σ-relevant refinement (Agda,
Coq), refinement types literally are Σ Path (λ p → cost p ≡ 5)
and coincide with Echo on the type level. No win. In
propositional-predicate refinement (F\*, Liquid Haskell), the
predicate is a mere proposition and the refinement type is the
truncation; Echo wins, and echo-not-prop is the formal
certificate."
This is the right shape of claim for this neighbour: explicitly acknowledge the tied case; carry the win against the propositional case as the formal exhibit.
Beyond the echo-not-prop witness-loss certificate, the iso
family in proofs/agda/Echo.agda provides a structural analogue
that strengthens the truncation argument specifically against
propositional-predicate refinement:
-
Echo-comp-iso-{to, from, from-to, to-from}provesEcho (g ∘ f) y ≃ Σ b. Echo f b × (g b ≡ y)directly. -
With a bijection on the outer leg,
cancel-iso-{to, from}exhibit the cancellationEcho (g ∘ f) y → Echo f (s y)and back; the projection-pentagon lemmasEcho-comp-iso-pent-{B, echo}show two natural three-fold factorings agree.
None of this is standard refinement-type machinery. Refinement
subsets have no ambient theorem stating that
{ x | (g ∘ f) x = y } is canonically isomorphic to a Σ over
an intermediate refinement, because the predicate carrier does
not isolate the intermediate point as proof-relevant data.
Under Σ-relevant refinement (Agda, Coq), the predicate IS the
refinement type and the iso family is the same family, not a
separate result — the tied case acknowledged in "Distinctness
claim" above. Under propositional-predicate refinement, the
predicate cannot isolate the intermediate b as data without
becoming type-relevant, at which point it has left propositional
refinement. So the iso family is structural evidence that the
truncation argument is tracking the right axis: what
propositionally-truncated refinement loses under composition is
not a corner case but a load-bearing structural property of
Echo-as-Σ-family.
The fact is structural about Echo-as-Σ and is independent of EI-2’s negative termination — it strengthens the truncation argument’s distinctness against propositional-predicate refinement regardless of what the integration recipe does or doesn’t do.
Not directly applicable. Refinement-type systems do not, in general, formalise their own 2-cells — refinement-type theory is about single indexed types, not about transport between parallel pairs of them.
In Σ-relevant refinement (which is just Σ-typed Agda/Coq), the
quotient-case 2-cell argument applies trivially because the
refinement is the Σ. So the 2-cell argument from
quotients.adoc and the meet argument from
galois-connections.adoc apply, but at that point we’re using
Echo machinery anyway and the win is against the surface syntax
("refinement types") rather than against an additional structural
neighbour.
In propositional-predicate refinement, there’s no 2-cell to argue about — the propositional predicate is opaque to the refinement- type system’s term language.
The recipe (custom propositional decoration order + echo-indexed
family + transport action — see gate-2-handoff.adoc Observation
G) is expressible in Σ-relevant refinement types if the
refinement-type system supports indexed predicates and dependent
transport. Most do; this is part of why echo coincides with
Σ-relevant refinement.
In propositional-predicate refinement, the recipe is not expressible: the predicate cannot be parameterised by the echo-indexed family without making the predicate itself type-relevant, at which point you’re back in Σ-relevant refinement. This is the recipe-level form of the same truncation/non-truncation split.
-
Witness identity (the first projection of the Σ).
-
The ability to define functions on the witness type, not just truth-values about it.
-
The ability to distinguish multiple inhabitants of the refinement type.
-
Anything. They’re the same construction with different surface syntax. The refinement-types camp is correct that echo is "a parameterised family of refinements indexed by the output" — in their (Σ-relevant) language, echo is exactly that, and they could implement the recipe without naming it.
Either of the following retracts the narrow distinctness claim against propositional-predicate refinement types:
-
A propositional-predicate refinement-type system that recovers individual witness identity through some non-truncating mechanism (refinement-with-evidence, dependent refinement predicates, etc.).
-
A demonstration that
echo-not-propfollows from a generic refinement-type lemma in some specific propositional system, i.e., the truncation argument is itself a refinement-type lemma in disguise.
Neither has been exhibited. The first is somewhat plausible — hybrid refinement systems exist that selectively retain witness data — but they would themselves move toward the Σ-relevant camp, not away from it.
There is no dedicated proofs/agda/adjacency/Refinement.agda
formalisation specific to refinement-type comparison. The three
gate-3 echo-not-prop exhibits implicitly cover the
propositional-truncation case (since refinement types are one
of the truncation-vulnerable neighbours), but a general
formalisation of "refinement-type-with-propositional-predicate
≡ propositional truncation of echo" would make the narrow
distinctness claim sharper.
This is forwarded to Q2.1 (the general echo-not-prop
generalisation) — closing Q2.1 also discharges this open
obligation.
-
Truncation argument: formalised on three domains via
echo-not-prop. Specific refinement-type formalisation awaits Q2.1. -
Recipe-level distinctness: argued in prose; not formalised.
-
Honest tied case (Σ-relevant refinement): acknowledged explicitly, not glossed.
-
The dependent type theory tradition (Martin-Löf type theory, Agda’s
Σ, Coq’ssig) — these are Σ-relevant refinement. -
F\* and Liquid Haskell — propositional-predicate refinement.
-
proofs/agda/examples/{TropicalArgmin,EpistemicUpdate,LinearErasure}.agdafor the formalecho-not-propexhibits. -
quotients.adoc— the closely related neighbour on the truncation axis.