Weakly Positive Subtyping (wp)
A subtyping judgment wp Φ Ψ A B for iso-recursive types with BCD-style intersections, where the two side-sets Φ, Ψ record the recursive assumptions in play.
Key realization (2026-05-30)
wp {} {} = ISub = BCDSub.
ISub is not a separate system — it is the special case of wp where both assumption sets are empty (the top-level entry point). “谜底就在谜面上.” This collapses what looked like two relations into one parameterized judgment.
Further: wp is a precise characterization of the Amber rule. The hypothesis a ≤ b ⊢ … that the Amber rule threads through a recursive subtyping derivation is exactly what the wp side-sets Φ/Ψ record.
Why it matters
- Removes a layer of redundancy in the development — lemmas stated for
ISubare instances ofwplemmas. - Makes the recursive-assumption bookkeeping explicit and inspectable, which is what the cover and transitivity arguments manipulate.
Related
- Split-Cover and Polarity Certificates
- Distributivity Subtyping Laws
- Size-Stratified Mutual Transitivity
- See Full Proposal of ISub - May 29 and Distributivity Subtyping (project notes).