The Package Category: Substitution, Not Sequencing

Substitution vs Sequencing

Cryptographic packages compose by oracle resolution (substitution): when package p₁ calls an oracle, the call is resolved by package p₂'s implementation. This is fundamentally different from Kleisli sequencing (the composition in Fam(KlSPComp)), where one computation's output feeds as input to the next.

	Substitution (packages)	Sequencing (Fam/Kleisli)
Morphisms	Handler → Handler (higher-order)	A →ₖ B (first-order)
Composition	Function composition	Monadic bind
Crypto meaning	Oracle resolution	Data pipeline
PL analogy	Variable substitution	Statement sequencing

This distinction is well-studied in programming language semantics (Fiore–Plotkin–Turi), where substitution and sequencing are related by the continuation-passing transform but are categorically distinct. All major cryptographic frameworks (CatCrypt, constructive crypto, UC, EasyCrypt) use substitution-style composition for packages.

The Package Category

We define a category on PkgInterface where:

• Objects are package interfaces (indexed families of operation signatures)
• Morphisms I ⟶ J are typed handler transformers: given implementations of I's operations, produce implementations of J's
• Composition is function composition (= oracle resolution)
• Identity is the pass-through handler

This is the category induced by the functor TypedHandler : PkgInterface → Type that maps each interface to its handler type (product of Kleisli arrows). In the language of enriched category theory, it is the underlying ordinary category of Set(TypedHandler(I), TypedHandler(J)).

Monoidal Structure

The symmetric monoidal structure comes from the product decomposition:

TypedHandler(I ⊗ J) ≅ TypedHandler(I) × TypedHandler(J)

Since PkgInterface.tensor uses Sum on index types and Sum.elim on families, this isomorphism is essentially definitional. The monoidal laws reduce to Sum index manipulation (funext + cases + rfl), in contrast to the complex fam_ext/HEq/erw proofs needed for Fam(C).

Relationship to Fam(KlSPComp)

Fam(KlSPComp) provides the correct monoidal structure (parallel composition) and individual Kleisli arrows for each operation. But its composition (Kleisli bind) does NOT match cryptographic linking (oracle substitution). Packages share Fam's monoidal structure but have their own categorical composition.

There is no functor between these categories in either direction: Fam composition is first-order (data pipeline), while package composition is second-order (handler transformation). They are related by CPS / double-negation translation but categorically distinct.

Main definitions

• TypedHandler — typed handler for an interface (product of Kleisli arrows)
• Category PkgInterface — the package category
• MonoidalCategory PkgInterface — parallel composition (from Sum on indices)
• BraidedCategory PkgInterface — interface swapping (from Sum.swap)
• SymmetricCategory PkgInterface — braiding is self-inverse

Implementation Note

The MonoidalCategoryStruct is defined as a private helper and explicitly assigned to MonoidalCategory via toMonoidalCategoryStruct. This ensures:

1. Within MonoidalCategory where, all struct fields are accessible for coherence proofs (pentagon, etc.) which are all rfl.
2. There is exactly ONE path to tensorObj (no typeclass diamond), so I ⊗ J definitionally equals the struct's tensorObj I J.
3. The braiding iso can be defined on PkgInterface.tensor (where Sum structure is visible) and coerced via definitional equality.

Typed Handler

def CatCrypt.Category.TypedHandler (I : PkgInterface) : Type

A typed oracle handler for interface I: for each operation indexed by I.ι, a Kleisli arrow from the domain type to the codomain type.

This is the product ∏_{i : I.ι} KlSPComp(I.doms i, I.codoms i), the "semantic content" of a package that exports interface I.

Equations

• CatCrypt.Category.TypedHandler I = ((i : I.ι) → I.doms i → CatCrypt.Core.SPComp (I.codoms i))

def CatCrypt.Category.TypedHandler.fst {I J : PkgInterface} (h : TypedHandler (I.tensor J)) : TypedHandler I

Extract the left component of a handler for a tensor interface.

Equations

• h.fst i = h (Sum.inl i)

def CatCrypt.Category.TypedHandler.snd {I J : PkgInterface} (h : TypedHandler (I.tensor J)) : TypedHandler J

Extract the right component of a handler for a tensor interface.

Equations

• h.snd j = h (Sum.inr j)

def CatCrypt.Category.TypedHandler.pair {I J : PkgInterface} (h₁ : TypedHandler I) (h₂ : TypedHandler J) : TypedHandler (I.tensor J)

Combine handlers for the left and right components into a tensor handler.

Equations

• h₁.pair h₂ (Sum.inl i) = h₁ i
• h₁.pair h₂ (Sum.inr j) = h₂ j

@[simp]

theorem CatCrypt.Category.TypedHandler.pair_fst {I J : PkgInterface} (h₁ : TypedHandler I) (h₂ : TypedHandler J) : (h₁.pair h₂).fst = h₁

@[simp]

theorem CatCrypt.Category.TypedHandler.pair_snd {I J : PkgInterface} (h₁ : TypedHandler I) (h₂ : TypedHandler J) : (h₁.pair h₂).snd = h₂

@[simp]

theorem CatCrypt.Category.TypedHandler.fst_pair_snd {I J : PkgInterface} (h : TypedHandler (I.tensor J)) : h.fst.pair h.snd = h

Category Instance

@[implicit_reducible]

instance CatCrypt.Category.pkgCat : CategoryTheory.Category.{0, 1} PkgInterface

The package category: objects are PkgInterface, morphisms are handler transformers. Composition is function composition, corresponding to oracle resolution (substitution).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CatCrypt.Category.pkg_comp_apply {I J K : PkgInterface} (f : I ⟶ J) (g : J ⟶ K) (h : TypedHandler I) : CategoryTheory.CategoryStruct.comp f g h = g (f h)

@[simp]

theorem CatCrypt.Category.pkg_id_apply {I : PkgInterface} (h : TypedHandler I) : CategoryTheory.CategoryStruct.id I h = h

Monoidal Category Instance

The MonoidalCategoryStruct is built as a private helper, then assigned to the MonoidalCategory instance via toMonoidalCategoryStruct. This avoids:

• The typeclass diamond (separate struct instance vs derived struct)
• Elaboration depth issues with rfl for pentagon/triangle

@[implicit_reducible]

instance CatCrypt.Category.pkgMCS : CategoryTheory.MonoidalCategoryStruct PkgInterface

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CatCrypt.Category.pkgMonoidal : CategoryTheory.MonoidalCategory PkgInterface

Equations

• One or more equations did not get rendered due to their size.

Braiding and Symmetric Structure

The braiding iso is defined on PkgInterface.tensor where Sum structure is directly visible. It is then used in the SymmetricCategory instance via the definitional equality I.tensor J = I ⊗ J.

@[implicit_reducible]

instance CatCrypt.Category.pkgSMC : CategoryTheory.SymmetricCategory PkgInterface

Equations

• One or more equations did not get rendered due to their size.

Connection to Untyped Handlers

The untyped Handler from PkgEval.lean handles ALL operations (∀ op dom codom, dom → SPComp codom). TypedHandler I restricts to a specific interface. The relationship:

• Restrict: Given an untyped handler and an interface I, project to TypedHandler I by evaluating at each I-operation's signature.
• Extend: Given TypedHandler I, extend to an untyped handler by mapping non-I operations to SPComp.fail.

The typed version is the correct mathematical object for the SMC structure, while the untyped version is convenient for the DeepPackage evaluation bridge.

theorem CatCrypt.Category.typedHandler_eq_pkgImpl_ofImpls (I : PkgInterface) : TypedHandler I = ((i : I.ι) → I.doms i → Core.SPComp (I.codoms i))

PkgImpl (σ = id) is exactly TypedHandler. This connects the categorical framework to the Fam-based representation. PkgImpl.ofImpls constructs a Fam morphism from componentwise implementations; TypedHandler IS those componentwise implementations.