A semiring, kept local to this module so the delivery instance does not pull in an external numeric prelude.

An object of Chu(C, ⊥).

• a is the positive carrier.
• b is the negative carrier.
• chuPair is the pairing a ⊗ b → r into the dualising object.

A pointed Chu object: a ChuObj together with a chosen point pair.

This is the separate wrapper used by polesAsChu to retain the positive and negative points that witness a self-dual channel.

A Chu morphism A → B is a pair of base arrows:

• chuForward :: arr a c runs forward from A⁺ to B⁺.
• chuBackward :: arr d b runs backward from B⁻ to A⁻.

Chu t r arr is the Chu construction as a base arrow. Objects are ChuObjs; morphisms are adjoint pairs wrapped by the Chu constructor.

Closed type family giving the positive carrier of a Chu object tag.

Every object of Chu(C, ⊥) is ultimately a ChuObj; this family exposes the positive carrier so that identity and composition can be typed uniformly without a separate type class.

Closed type family giving the negative carrier of a Chu object tag.

See ChuPosType for motivation; this is the dual side.

Negation swaps the carriers via the symmetric braiding.

Involution is definitional for a symmetric braiding: braid . braid = id.

Identity Chu morphism.

Sequential composition of Chu morphisms.

Forward components compose covariantly; backward components compose contravariantly.

The adjoint law for arr = (->) and the cartesian tensor.

A pair (f⁺, f⁻) is a Chu morphism exactly when e_B (f⁺ a, d) = e_A (a, f⁻ d) for all a and d.

Pointwise adjoint law for arr = (->).

When the dualising object r does not have an Eq instance (e.g. it is itself a function), supply a probe k :: r -> s with Eq s.

Named-recipient delivery predicate over an arbitrary semiring.

A post whose recipient list contains who delivers with sOne; an empty list delivers to no one with sZero.

Delivery matrix for a fixed list of posts and a roster of agents.

Rows are posts (in the order given), columns are agents (in the order given), and entry (p, a) is the delivery weight of post p to agent a.

Negative part of the Chu tensor A ⊗ B.

A value (f, g) lives here when e_A(a, g(b)) = e_B(b, f(a)) for all a ∈ A⁺, b ∈ B⁺.

Positive part of the Chu par A ⅋ B.

A value (f, g) lives here when e_A(g(d), a) = e_B(f(a), d) for all a ∈ A⁻, d ∈ B⁻.

Tensor product of Chu objects over Set.

Par product of Chu objects over Set.

Linear implication A ⊸ B = A⊥ ⅋ B over Set.

The positive carrier is the set of Chu morphisms A → B, packaged as ChuParPos after negating A.

Additive conjunction A & B over Set.

Positive carrier is A⁺ × B⁺; negative carrier is the disjoint union A⁻ + B⁻.

Additive disjunction A ⊕ B over Set.

Positive carrier is the disjoint union A⁺ + B⁺; negative carrier is A⁻ × B⁻.

Additive unit ⊤ over Set.

Positive carrier is the terminal object 1; negative carrier is the initial object 0.

Additive unit 0 over Set.

Positive carrier is the initial object 0; negative carrier is the terminal object 1.

First projection A & B → A.

Second projection A & B → B.

Left injection A → A ⊕ B.

Right injection A → A ⊕ B.

Unique morphism A → ⊤.

Unique morphism 0 → A.

Pairing of morphisms into the additive conjunction.

Universal property of A & B: given f : C → A and g : C → B, produce ⟨f,g⟩ : C → A & B.

Copairing of morphisms out of the additive disjunction.

Universal property of A ⊕ B: given f : A → C and g : B → C, produce [f,g] : A ⊕ B → C.

Left unit isomorphism A → ⊤ & A.

Inverse of withTopLChu.

Right unit isomorphism A → A & ⊤.

Inverse of withTopRChu.

Left unit isomorphism A → 0 ⊕ A.

Inverse of zeroPlusLChu.

Right unit isomorphism A → A ⊕ 0.

Inverse of zeroPlusRChu.

Evaluation counit A ⊗ (A ⊸ B) → B over Set.

Forward applies the Chu morphism stored in the implication object. Backward pairs the argument with its own positive point, recovering the adjoint condition.

Tensor of two Chu morphisms.

Par of two Chu morphisms.

Unit object I = (1, K) with pairing snd.

Bottom object ⊥ = (K, 1), dual of the unit.

Enumerate all ChuTensorNeg values for finite carriers.

Enumerate all ChuParPos values for finite carriers.

A Chu object is separated when the pairing distinguishes every pair of positive points. Equivalently, the transposed pairing A⁺ -> (A⁻ ⊸ ⊥) is injective.

A Chu object is extensional when the pairing distinguishes every pair of negative points. Equivalently, the pairing A⁻ -> (A⁺ ⊸ ⊥) is injective.

Left unitor λ_A : I ⊗ A → A over Set.

Forward drops the unit; backward maps a negative point b to the unique Chu tensor negative with f() = b and g a = e(a, b).

Inverse of the left unitor.

Right unitor ρ_A : A ⊗ I → A over Set.

Inverse of the right unitor.

Associator (A ⊗ B) ⊗ C → A ⊗ (B ⊗ C) over Set.

Positives reassociate as pairs. Negatives reassociate the adjoint pairs: a negative of A ⊗ (B ⊗ C) is sent to a negative of (A ⊗ B) ⊗ C by unpacking the inner ChuTensorNeg.

Inverse associator A ⊗ (B ⊗ C) → (A ⊗ B) ⊗ C over Set.

Slide A ⊗ (B ⊗ C) → B ⊗ (A ⊗ C) over Set.

This is the Channel slide, derived as assoc . tensor braid id . assoc' and written directly so the instance does not have to manufacture intermediate object constraints.

Embed a symmetric pole into a pointed Chu object.

A self-dual channel Poles arr a a has write pole In arr a and read pole Out arr a. close is already the pairing In ⊗ Out → arr a a, so the embedding is direct. The point pair (conjoint e, companion e) is retained as the chosen point of the pointed object.

Apply a Chu endomorphism to a symmetric pole.

This is the lawful counterpart to the free dimap: the forward and backward maps are an adjoint pair by construction of ChuMorphism. The Chu law is discharged by the type, not just tested.

A type-level Chu object: a tag with a canonical ChuObj value and finite carrier enumerations.

chuPosAll and chuNegAll are used by separation / extensionality oracles and by enumeration of tensor / par negatives. They default to a runtime error; only objects that actually participate in finite oracles need to supply them.

Marker: the pairing distinguishes positive points.

Runtime evidence is available through chuSeparated. Instances close the constructors we admit (ChuTwo, ChuOUnit, tensor, negation).

Marker: the pairing distinguishes negative points.

Runtime evidence is available through chuExtensional. Negation swaps this with ChuSeparated.

Type-level non-emptiness of an object's positive carrier.

Used to guard additive marker instances: A & B can only be extensional when both A and B have at least one positive point, because the negative carrier is the disjoint union and distinct injections must be separated by a positive pair.

Type-level non-emptiness of an object's negative carrier.

Used to guard additive marker instances: A ⊕ B can only be separated when both A and B have at least one negative point, because the positive carrier is the disjoint union and distinct injections must be separated by a negative pair.

The object-indexed Chu construction as a base arrow.

Documentation alias for OChu.

This is a plain type synonym, not a separate category: the separated-extensional conditions are enforced only by the Ob constraint of OChu. If you need Barr's subcategory to be tracked in the type system, wrap OChu in a newtype with its own Category instance.

Parallel composition for OChu.

Left unitor I ⊗ A → A for OChu.

Inverse left unitor A → I ⊗ A for OChu.

Right unitor A ⊗ I → A for OChu.

Inverse right unitor A → A ⊗ I for OChu.

Symmetric braiding A ⊗ B → B ⊗ A for OChu.

Par structure on the object-indexed Chu category.

The par product of objects is ChuOPar; the structural morphisms are the Set-level par maps already defined for Chu morphisms.

Parallel composition for the par product on OChu.

Left unitor ⊥ ⅋ A → A for OChu.

Inverse left unitor A → ⊥ ⅋ A for OChu.

Right unitor A ⅋ ⊥ → A for OChu.

Inverse right unitor A → A ⅋ ⊥ for OChu.

Evaluation counit A ⊗ (A ⊸ B) → B for OChu.

Curry (A ⊗ B → C) → (A → B ⊸ C) for OChu.

Uncurry (A → B ⊸ C) → (A ⊗ B → C) for OChu.

Discard !A → I for OChu.

Dereliction !A → A for OChu.

Introduction A → ?A for OChu.

Merge ?A ⅋ ?A → ?A for OChu.

Unit ⊥ → ?A for OChu.

Copy !A → !A ⊗ !A for OChu.

Discard !A → I for OChu.

Merge !A ⊗ !A → !A for OChu.

Zero I → !A for OChu.

Unit object type for OChu.

Tensor object type for OChu.

Object-level negation A⊥.

Carriers swap; the pairing is negateChu of the underlying object. Separation and extensionality swap: if A is separated then A⊥ is extensional, and conversely.

Object-level additive conjunction A & B.

ChuSeparated is available whenever both summands are separated. ChuExtensional is guarded by ChuPosNonEmpty: when one summand has an empty positive carrier (e.g. A & 0), distinct negative injections cannot be separated, so the instance is not asserted.

Object-level additive disjunction A ⊕ B.

ChuExtensional is available whenever both summands are extensional. ChuSeparated is guarded by ChuNegNonEmpty: when one summand has an empty negative carrier (e.g. ⊤ ⊕ B), distinct positive injections cannot be separated, so the instance is not asserted.

Object-level multiplicative disjunction A ⅋ B.

Positive carrier is the set of ChuParPos witnesses; negative carrier is the product A⁻ × B⁻. This is the real par, distinct from the additive disjunction ChuOPlus.

Object-level additive unit ⊤.

Object-level additive zero 0.

The self-dual two-point Chu object used in the oracles.

A non-self-dual three-point Chu object over Bool.

Both carriers are Maybe Bool, but the pairing is the non-symmetric partial-order relation (Nothing <= Just False <= Just True), not equality. This breaks the self-duality coincidence of ChuTwo while keeping the object separated and extensional.

A finite Double-semiring Chu object.

Carriers are the two-element type Bool, representing the subset {0, 1} of Double. The full real line is replaced by this tiny subset so the finite oracles remain runnable. The pairing lands in Double via the existing ChuSemiring instance.

A concrete delivery-matrix Chu object: two posts and two agents.

The pairing is the boolean delivery matrix computed by deliveryMatrix and deliversToSemiring. Posts and agents are indexed by Bool so the carriers stay finite and the oracles remain runnable.

A tiny self-dual Chu object over Any (disjunction monoid) with equality pairing. Used to test the bimonoid on !A from a Monoid on A⁺.

Symmetric braiding for the Chu tensor over Set.

Double-negation unit A → A⊥⊥.

On carriers this is the identity: two braids restore A⁺ and A⁻, and the pairing is e . braid . braid = e. It is an isomorphism precisely on separated-extensional objects.

Double-negation counit A⊥⊥ → A.

Object-level linear implication A ⊸ B = A⊥ ⅋ B.

Curry (A ⊗ B → C) → (A → B ⊸ C) over Set.

Uncurry (A → B ⊸ C) → (A ⊗ B → C) over Set.

All functions from a finite domain to a finite codomain.

Cofree cocommutative comonoid on a Set-based Chu object.

Positives are those of A; negatives are every functional A⁺ → r; the pairing is evaluation. Original negatives embed by Yoneda d ↦ \a -> e(a, d), and constants k ↦ const k supply discard.

Free commutative monoid ?A = (!A⊥)⊥.

Positives are the functionals A⁻ → r; negatives are those of A.

Copy !A → !A ⊗ !A: diagonal on points, contraction on functionals.

Discard !A → I: the constant functionals.

Merge !A ⊗ !A → !A: the monoid operation on points, bilinearly extended to functionals.

Zero I → !A: the monoid unit as a point of A⁺.

Dereliction !A → A: identity on points, Yoneda on negatives.

Zero I → ?A. The unit functional is constantly sZero.

This is not the ⅋-monoid unit (that is zeroWhyNotParChu : ⊥ → ?A).

Introduction A → ?A: Yoneda on positives, identity on negatives.

Digging !A → !!A.

Over the Set-based ! of this module, !!A is the same object as !A (positive carrier A⁺, negative carrier A⁺ → r), so digging is the identity. This is an observable fact about the model, not a stub.

Promotion !A ⊗ !B → !(A & B).

Forward is the identity on the shared positive carrier (A⁺, B⁺). Backward turns a bilinear element of !A ⊗ !B into a functional on (A⁺, B⁺) using either leg of the bilinear condition.

Merge ?A ⅋ ?A → ?A: the dual of copyBangChu.

A par-positive is a pair of functionals A⁻ → (A⁻ → r) satisfying g y x = f x y. Merge contracts the diagonal \x -> g x x.

⅋-monoid unit ⊥ → ?A: constants, dual of discardBangChu.

Left unitor ⊥ ⅋ A → A over Set.

Inverse of the left par unitor: A → ⊥ ⅋ A over Set.

Right unitor A ⅋ ⊥ → A over Set.

Inverse of the right par unitor: A → A ⅋ ⊥ over Set.

Associator (A ⅋ B) ⅋ C → A ⅋ (B ⅋ C) over Set.

Inverse associator A ⅋ (B ⅋ C) → (A ⅋ B) ⅋ C over Set.

Symmetric braiding A ⅋ B → B ⅋ A over Set.

Object-level !A.

Object-level ?A = (!A⊥)⊥.