Effectus Theory

An effectus (Cho-Jacobs 2015) is a category with coproducts and a terminal object satisfying axioms about pullbacks along coproduct injections. We define the key properties needed for Kantorovich UCMonads.

Mathematical context

In the effectus framework, a predicate on an object X is a morphism p : X → 1 + 1 in the Kleisli category. The two injections κ₁, κ₂ : 1 → 1 + 1 represent "true" and "false". The predicate transformer wp(f, p) is defined by post-composition: wp(f, p) = p ∘ f.

The effectus axioms (E1-E3) ensure that predicates form an effect module:

• (E1) Finite coproducts exist and are disjoint
• (E2) Partial addition of predicates: p ⊕ q is defined when p + q ≤ 1
• (E3) Positive cancellation: p ⊕ q = 0 ⟹ p = 0 ∧ q = 0

Axiom (E3) is the key one for cryptographic applications. In the Kleisli category of a probability monad, it says: if a sum of non-negative quantities is zero, each quantity is zero. This is the property that makes game-hopping arguments valid — if an adversary has zero advantage, no sub-computation can have negative advantage "cancelling out" a positive one.

Relation to UCMonadPosCancel

The UCMonadPosCancel class in CatCrypt.Crypto.KantorovichUCMonad is the metric-enriched version of (E3): instead of "sum = 0 implies each = 0" for predicates, it states "sum of distances = 0 implies each distance = 0" for Kleisli morphisms. This file provides the categorical/predicate-level framing that motivates the metric version.

Main definitions

• EffectusPred — a predicate in the Kleisli category (map to Bool)
• wpTransformer — the weakest-precondition predicate transformer
• EffectusPositiveCancel — the positive cancellation axiom (E3) for a monad

References

• Cho, K. & Jacobs, B. (2015). An introduction to effectus theory.
• Cho, K. & Jacobs, B. (2019). Disintegration and Bayesian inversion via string diagrams. MSCS 29(7).

Predicates in the Kleisli Category

structure CatCrypt.Category.Effectus.EffectusPred (T : Type → Type) (α : Type) : Type

An effectus predicate on type α in the Kleisli category of T is a Kleisli morphism α → T Bool. The value true represents "accept" and false represents "reject".

This is equivalent to the standard effectus formulation using 1 + 1, since Bool ≅ Unit ⊕ Unit, but avoids universe issues.

For T = SPComp (sub-distribution monad), this is an event: a function that maps each state to a distribution over {true, false, ⊥}.

For T = QComp d (quantum monad), this is a binary-outcome instrument: a POVM with two elements (accept/reject).

• pred : α → T Bool

  The underlying Kleisli morphism

theorem CatCrypt.Category.Effectus.EffectusPred.ext {T : Type → Type} {α : Type} {p q : EffectusPred T α} (h : p.pred = q.pred) : p = q

theorem CatCrypt.Category.Effectus.EffectusPred.ext_iff {T : Type → Type} {α : Type} {p q : EffectusPred T α} : p = q ↔ p.pred = q.pred

def CatCrypt.Category.Effectus.EffectusPred.one (T : Type → Type) [Monad T] (α : Type) : EffectusPred T α

The one predicate always accepts (maps to true).

Equations

• CatCrypt.Category.Effectus.EffectusPred.one T α = { pred := fun (x : α) => pure true }

def CatCrypt.Category.Effectus.EffectusPred.falseP (T : Type → Type) [Monad T] (α : Type) : EffectusPred T α

The zero predicate always rejects (maps to false).

Equations

• CatCrypt.Category.Effectus.EffectusPred.falseP T α = { pred := fun (x : α) => pure false }

Predicate Transformer (Weakest Precondition)

def CatCrypt.Category.Effectus.wpTransformer {T : Type → Type} [Monad T] {α β : Type} (f : α → T β) (p : EffectusPred T β) : EffectusPred T α

The predicate transformer wp(f, p) for a Kleisli morphism f : α → T β and predicate p : EffectusPred T β is defined by Kleisli composition: wp(f, p)(a) = f(a) >>= p.pred. This is the "weakest precondition" transformer in the effectus framework.

In probabilistic terms: wp(f, p)(a) gives the probability that running f on input a and then testing with p yields "accept".

Equations

• CatCrypt.Category.Effectus.wpTransformer f p = { pred := fun (a : α) => f a >>= p.pred }

theorem CatCrypt.Category.Effectus.wpTransformer_pure {T : Type → Type} [Monad T] [LawfulMonad T] {α : Type} (p : EffectusPred T α) : wpTransformer pure p = p

Predicate transformer is functorial: wp(pure, p) = p.

theorem CatCrypt.Category.Effectus.wpTransformer_comp {T : Type → Type} [Monad T] [LawfulMonad T] {α β γ : Type} (f : α → T β) (g : β → T γ) (p : EffectusPred T γ) : wpTransformer (fun (a : α) => f a >>= g) p = wpTransformer f (wpTransformer g p)

Predicate transformer composes: wp(f ∘ₖ g, p) = wp(f, wp(g, p)).

Positive Cancellation (Effectus Axiom E3)

class CatCrypt.Category.Effectus.EffectusPositiveCancel (T : Type → Type) [Monad T] : Prop

Positive cancellation for the Kleisli category of T.

This is axiom (E3) from Cho-Jacobs (2015): if the "sum" of two predicates equals the zero predicate, then each predicate is individually zero.

We state this in a monad-agnostic way: post-composing two Kleisli morphisms with any test predicate and getting the same result implies the morphisms are equal. This is the "separation by tests" property.

For classical probability (SPComp), this says: if ∀ D : β → SPComp Bool, Pr[f₁;D] = Pr[f₂;D], then f₁ = f₂ (as sub-distributions).

For quantum (QComp d), this says: if two instruments give the same measurement statistics for all binary measurements, they are equal.

This class captures the qualitative (non-metric) version. The metric version is UCMonadPosCancel in KantorovichUCMonad.lean.

• posCancel {α β : Type} (f₁ f₂ : α → T β) : (∀ (p : EffectusPred T β), wpTransformer f₁ p = wpTransformer f₂ p) → f₁ = f₂

  If post-composing f₁ and f₂ with every test yields the same result, then f₁ = f₂. This is the "separation by tests" property.

theorem CatCrypt.Category.Effectus.wpTransformer_faithful {T : Type → Type} [Monad T] [EffectusPositiveCancel T] {α β : Type} (f₁ f₂ : α → T β) (h : ∀ (p : EffectusPred T β), wpTransformer f₁ p = wpTransformer f₂ p) : f₁ = f₂

Positive cancellation implies that the predicate transformer is faithful: wp(f₁, −) = wp(f₂, −) implies f₁ = f₂.

theorem CatCrypt.Category.Effectus.posCancel_comp_left {T : Type → Type} [Monad T] [LawfulMonad T] [EffectusPositiveCancel T] {α β γ : Type} (f : α → T β) (g₁ g₂ : β → T γ) (h : ∀ (p : EffectusPred T γ), wpTransformer g₁ p = wpTransformer g₂ p) : (fun (a : α) => f a >>= g₁) = fun (a : α) => f a >>= g₂

Positive cancellation is preserved by Kleisli composition on the left: if g₁ = g₂ (established via tests), then f >>= g₁ = f >>= g₂.

Stronger Separation: Arbitrary Codomain Tests

The effectus axiom (E3) traditionally uses Boolean tests (predicates to 1 + 1). A stronger version uses tests to arbitrary types — this is what UCMonadPosCancel does in the metric setting. We show that with LawfulMonad, the stronger version follows from the Boolean version by taking k = pure.

class CatCrypt.Category.Effectus.EffectusStrongPosCancel (T : Type → Type) [Monad T] : Prop

Strong positive cancellation: separation by all Kleisli morphisms (not just Boolean tests). This matches UCMonadPosCancel.

• strongPosCancel {α β : Type} (f₁ f₂ : α → T β) : (∀ (γ : Type) (k : β → T γ), (fun (a : α) => f₁ a >>= k) = fun (a : α) => f₂ a >>= k) → f₁ = f₂

  If post-composing f₁ and f₂ with every Kleisli morphism yields the same result, then f₁ = f₂.

instance CatCrypt.Category.Effectus.instEffectusStrongPosCancelOfLawfulMonadOfEffectusPositiveCancel (T : Type → Type) [Monad T] [LawfulMonad T] [EffectusPositiveCancel T] : EffectusStrongPosCancel T

EffectusPositiveCancel (Boolean tests suffice) implies EffectusStrongPosCancel (all tests suffice), since the all-tests hypothesis is strictly stronger than the Boolean-tests hypothesis. With LawfulMonad, the all-k hypothesis with k = pure already gives f₁ = f₂ via bind_pure.

theorem CatCrypt.Category.Effectus.strongPosCancel_of_pure {T : Type → Type} [Monad T] [LawfulMonad T] {α β : Type} (f₁ f₂ : α → T β) (h : (fun (a : α) => f₁ a >>= pure) = fun (a : α) => f₂ a >>= pure) : f₁ = f₂

With LawfulMonad, strong positive cancellation follows from taking k = pure in the "all morphisms" quantifier.

Connection to Metric Enrichment

The effectus axiom (E3) is the qualitative backbone of the metric-enriched positive cancellation in UCMonadPosCancel. The relationship is:

• EffectusPositiveCancel says: equality of all test outcomes implies equality of morphisms.
• UCMonadPosCancel says: zero distance in all post-processings implies zero distance of morphisms.

When the monad's pseudometric is faithful (ucSdist f g = 0 → f = g), the metric version implies the qualitative version. In general, the metric version is stated up to the equivalence relation induced by the pseudometric.