Package Category

This file proves that CatCrypt's deep packages form a category.

Main definitions

• PkgHom I E - Semantic package morphism from interface I to interface E
• Category DeepInterface - Category instance (all laws hold by rfl)
• DeepPackage.toPkgHom - Embedding of concrete packages into semantic morphisms

Main results

• All three category laws (id_comp, comp_id, assoc) hold by rfl
• DeepPackage.toPkgHom_id - Identity package maps to identity morphism
• Tensor product of interfaces via list append

Design

The key insight is that semantic package morphisms (PkgHom) abstract away from concrete code representations and work purely with oracle handlers. This gives all category laws definitionally (by rfl), following the Kleisli category construction for the State+Prob monad.

Semantic Package Morphisms

def CatCrypt.Deep.PkgHom (I E : DeepInterface) : Type (u + 1)

Semantic package morphism from interface I to interface E.

A PkgHom I E represents a package that exports operations in E and imports operations from I. For each exported operation, given a domain value and an oracle handler for I's operations, it produces an SPComp computation.

This abstracts over concrete code representations (RawCode, ValidCode) and works purely at the semantic level, giving clean categorical properties.

In the Kleisli category interpretation:

• Objects are interfaces (types of operations)
• Morphisms are semantic oracle-transforming functions
• Composition is oracle handler chaining (= package linking)
• Identity forwards all operations to the handler

Equations

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

def CatCrypt.Deep.PkgHom.id (I : DeepInterface) : PkgHom I I

Identity morphism: forwards each operation call to the oracle handler.

Equations

• CatCrypt.Deep.PkgHom.id I op dom codom h x handler = handler op dom codom h x

def CatCrypt.Deep.PkgHom.comp {I M E : DeepInterface} (f : PkgHom I M) (g : PkgHom M E) : PkgHom I E

Composition of morphisms (diagrammatic order: f ≫ g = "first f, then g").

Given f : PkgHom I M and g : PkgHom M E, the composition has g resolve its oracle calls through f, which in turn resolves through the external handler.

Equations

• f.comp g op dom codom h_exp x handler_I = g op dom codom h_exp x fun (op' : ℕ) (dom' codom' : Type ?u.12) (h_M : (op', dom', codom') ∈ M.ops) (x' : dom') => f op' dom' codom' h_M x' handler_I

theorem CatCrypt.Deep.PkgHom.id_comp {I E : DeepInterface} (f : PkgHom I E) : (id I).comp f = f

Left identity: id ≫ f = f. Holds by eta-reduction.

theorem CatCrypt.Deep.PkgHom.comp_id {I E : DeepInterface} (f : PkgHom I E) : f.comp (id E) = f

Right identity: f ≫ id = f. Holds by beta-reduction.

theorem CatCrypt.Deep.PkgHom.comp_assoc {I J K L : DeepInterface} (f : PkgHom I J) (g : PkgHom J K) (h : PkgHom K L) : (f.comp g).comp h = f.comp (g.comp h)

Associativity: (f ≫ g) ≫ h = f ≫ (g ≫ h). Holds definitionally.

Category Instance

@[implicit_reducible]

instance CatCrypt.Deep.instCategoryDeepInterface : CategoryTheory.Category.{u + 1, u + 1} DeepInterface

Category of deep interfaces and semantic package morphisms.

Objects are DeepInterfaces (specifying operation signatures). Morphisms are PkgHoms (semantic oracle-transforming functions). All three category laws (id_comp, comp_id, assoc) hold definitionally.

Equations

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

Connection to DeepPackage

Every concrete `DeepPackage` gives rise to a semantic `PkgHom` via
evaluation. This embedding preserves the identity package structure. 

noncomputable def CatCrypt.Deep.DeepPackage.toPkgHom (p : DeepPackage) : PkgHom p.imports p.exports

Embed a concrete DeepPackage into a semantic PkgHom.

Given a package p with imports I and exports E, we get a PkgHom by evaluating each operation's code with the provided oracle handler via evalWith.

Equations

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

theorem CatCrypt.Deep.DeepPackage.toPkgHom_id (iface : DeepInterface) : (id iface).toPkgHom = PkgHom.id iface

The identity package maps to the identity PkgHom.

The identity package implements each operation as an oracle call, and evalWith maps oracle calls to the handler, giving identity.

Tensor Product of Interfaces

def CatCrypt.Deep.tensorObj (I J : DeepInterface) : DeepInterface

Tensor product of interfaces: concatenation of operation lists.

Equations

• CatCrypt.Deep.tensorObj I J = { ops := I.ops ++ J.ops }

def CatCrypt.Deep.tensorUnit' : DeepInterface

The tensor unit: empty interface with no operations.

Equations

• CatCrypt.Deep.tensorUnit' = { ops := [] }

theorem CatCrypt.Deep.tensorObj_assoc (I J K : DeepInterface) : tensorObj (tensorObj I J) K = tensorObj I (tensorObj J K)

Tensor product is associative.

theorem CatCrypt.Deep.tensorObj_unit_left (I : DeepInterface) : tensorObj tensorUnit' I = I

Empty interface is a left unit for tensor.

theorem CatCrypt.Deep.tensorObj_unit_right (I : DeepInterface) : tensorObj I tensorUnit' = I

Empty interface is a right unit for tensor.

Tensor Product of Morphisms

The tensor product of two morphisms dispatches exported operations
to the appropriate morphism and restricts oracle handlers accordingly.
This requires classical decidability since `Type u` membership in
lists is not computably decidable. 

noncomputable def CatCrypt.Deep.PkgHom.tensor {I₁ E₁ I₂ E₂ : DeepInterface} (f : PkgHom I₁ E₁) (g : PkgHom I₂ E₂) : PkgHom (tensorObj I₁ I₂) (tensorObj E₁ E₂)

Tensor product of morphisms: parallel composition.

Given f : PkgHom I₁ E₁ and g : PkgHom I₂ E₂, produces PkgHom (tensorObj I₁ I₂) (tensorObj E₁ E₂) by dispatching:

• Operations in E₁: handled by f (with handler restricted to I₁)
• Operations in E₂: handled by g (with handler restricted to I₂)

Equations

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

noncomputable def CatCrypt.Deep.PkgHom.whiskerLeft (X : DeepInterface) {Y₁ Y₂ : DeepInterface} (f : PkgHom Y₁ Y₂) : PkgHom (tensorObj X Y₁) (tensorObj X Y₂)

Left whiskering: tensor identity on the left with a morphism.

whiskerLeft X f : (X ⊗ Y₁) ⟶ (X ⊗ Y₂) for f : Y₁ ⟶ Y₂. Operations in X are forwarded to the handler (identity); operations in Y₂ are handled by f.

Equations

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

noncomputable def CatCrypt.Deep.PkgHom.whiskerRight {X₁ X₂ : DeepInterface} (f : PkgHom X₁ X₂) (Y : DeepInterface) : PkgHom (tensorObj X₁ Y) (tensorObj X₂ Y)

Right whiskering: tensor a morphism on the left with identity on the right.

whiskerRight f Y : (X₁ ⊗ Y) ⟶ (X₂ ⊗ Y) for f : X₁ ⟶ X₂. Operations in X₂ are handled by f; operations in Y are forwarded to the handler (identity).

Equations

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

Pass-through Morphisms

A "pass-through" morphism is one that just forwards all operations to
the oracle handler, converting membership proofs via a list equality.
This is the key building block for structural morphisms (associator,
unitors, braiding).

The crucial property: any two pass-through morphisms between the same
types are equal, by proof irrelevance on the membership proofs. 

def CatCrypt.Deep.PkgHom.ofOpsEq {I E : DeepInterface} (h : E.ops = I.ops) : PkgHom I E

A pass-through morphism that forwards to the handler, converting membership proofs via a list equality.

Equations

• CatCrypt.Deep.PkgHom.ofOpsEq h op dom codom hE x handler = handler op dom codom ⋯ x

theorem CatCrypt.Deep.PkgHom.ofOpsEq_rfl (I : DeepInterface) : ofOpsEq ⋯ = id I

ofOpsEq rfl is the identity.

theorem CatCrypt.Deep.PkgHom.ofOpsEq_comp {I M E : DeepInterface} (h₁ : M.ops = I.ops) (h₂ : E.ops = M.ops) : (ofOpsEq h₁).comp (ofOpsEq h₂) = ofOpsEq ⋯

Composition of pass-throughs is a pass-through.

theorem CatCrypt.Deep.PkgHom.ofOpsEq_unique {I E : DeepInterface} (h₁ h₂ : E.ops = I.ops) : ofOpsEq h₁ = ofOpsEq h₂

Any two pass-throughs between the same types are equal.

Whisker Laws

theorem CatCrypt.Deep.PkgHom.whiskerLeft_id (X Y : DeepInterface) : whiskerLeft X (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (tensorObj X Y)

Whiskering on the left with the identity is the identity.

theorem CatCrypt.Deep.PkgHom.whiskerRight_id (X Y : DeepInterface) : whiskerRight (CategoryTheory.CategoryStruct.id X) Y = CategoryTheory.CategoryStruct.id (tensorObj X Y)

Whiskering on the right with the identity is the identity.

Monoidal Category Instance

`DeepInterface` forms a (strict) monoidal category with:
- Tensor product = list append of operations
- Unit = empty interface
- Associator/unitors defined directly as pass-through morphisms
- All coherence axioms follow from proof irrelevance 

noncomputable def CatCrypt.Deep.assocIso (X Y Z : DeepInterface) : tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)

Associator: pass-through using List.append_assoc.

Equations

• CatCrypt.Deep.assocIso X Y Z = { hom := CatCrypt.Deep.PkgHom.ofOpsEq ⋯, inv := CatCrypt.Deep.PkgHom.ofOpsEq ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def CatCrypt.Deep.leftUnitorIso (X : DeepInterface) : tensorObj tensorUnit' X ≅ X

Left unitor: pass-through using List.nil_append.

Equations

• CatCrypt.Deep.leftUnitorIso X = { hom := CatCrypt.Deep.PkgHom.ofOpsEq ⋯, inv := CatCrypt.Deep.PkgHom.ofOpsEq ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def CatCrypt.Deep.rightUnitorIso (X : DeepInterface) : tensorObj X tensorUnit' ≅ X

Right unitor: pass-through using List.append_nil.

Equations

• CatCrypt.Deep.rightUnitorIso X = { hom := CatCrypt.Deep.PkgHom.ofOpsEq ⋯, inv := CatCrypt.Deep.PkgHom.ofOpsEq ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Monoidal Category Structure

We provide `MonoidalCategoryStruct` (the tensor product data) and prove
the coherence axioms (pentagon, triangle) that hold unconditionally.

**Important**: The naturality axioms (`tensorHom_comp_tensorHom`,
`associator_naturality`, `braiding_naturality`) require that tensor
components have **disjoint** operation lists. This matches Rocq SSProve,
which enforces disjointness via `:|:` (disjoint union of finite maps).
With overlapping operations, `dite`-based dispatch becomes inconsistent
between left-whiskered and right-whiskered morphisms.

The coherence axioms (pentagon, triangle, hexagons, symmetry) hold
unconditionally because they involve only structural morphisms
(pass-throughs and braiding), not arbitrary morphisms `f`, `g`. 

@[implicit_reducible]

noncomputable instance CatCrypt.Deep.instMonoidalCategoryStructDeepInterface : CategoryTheory.MonoidalCategoryStruct DeepInterface

Equations

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

Unconditionally valid monoidal axioms

theorem CatCrypt.Deep.pkg_id_tensor_id (X₁ X₂ : DeepInterface) : ((PkgHom.id X₁).whiskerRight X₂).comp (PkgHom.whiskerLeft X₁ (PkgHom.id X₂)) = PkgHom.id (tensorObj X₁ X₂)

Tensor of identities is identity.

theorem CatCrypt.Deep.pkg_rightUnitor_naturality {X Y : DeepInterface} (f : X ⟶ Y) : (PkgHom.whiskerRight f tensorUnit').comp (rightUnitorIso Y).hom = PkgHom.comp (rightUnitorIso X).hom f

Right unitor is natural.

theorem CatCrypt.Deep.pkg_pentagon (W X Y Z : DeepInterface) : (PkgHom.whiskerRight (assocIso W X Y).hom Z).comp (PkgHom.comp (assocIso W (tensorObj X Y) Z).hom (PkgHom.whiskerLeft W (assocIso X Y Z).hom)) = PkgHom.comp (assocIso (tensorObj W X) Y Z).hom (assocIso W X (tensorObj Y Z)).hom

Pentagon coherence for associators.

theorem CatCrypt.Deep.pkg_triangle (X Y : DeepInterface) : PkgHom.comp (assocIso X tensorUnit' Y).hom (PkgHom.whiskerLeft X (leftUnitorIso Y).hom) = PkgHom.whiskerRight (rightUnitorIso X).hom Y

Triangle coherence for associator and unitors.

Braided and Symmetric Structure

The braiding swaps the two halves of a tensor product.
Since our tensor is list append, braiding reindexes operations
via commutativity of `∨` in list membership.

Coherence axioms (hexagons, symmetry) hold unconditionally.
Naturality requires disjoint interfaces (see above). 

noncomputable def CatCrypt.Deep.PkgHom.braiding (X Y : DeepInterface) : PkgHom (tensorObj X Y) (tensorObj Y X)

Braiding morphism: swap the two halves of a tensor product.

Equations

• CatCrypt.Deep.PkgHom.braiding X Y op dom codom h_exp x handler = handler op dom codom ⋯ x

theorem CatCrypt.Deep.PkgHom.braiding_braiding (X Y : DeepInterface) : (braiding X Y).comp (braiding Y X) = id (tensorObj X Y)

Braiding composed with itself is identity (by proof irrelevance).

noncomputable def CatCrypt.Deep.braidingIso (X Y : DeepInterface) : tensorObj X Y ≅ tensorObj Y X

Braiding isomorphism: X ⊗ Y ≅ Y ⊗ X.

Equations

• CatCrypt.Deep.braidingIso X Y = { hom := CatCrypt.Deep.PkgHom.braiding X Y, inv := CatCrypt.Deep.PkgHom.braiding Y X, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem CatCrypt.Deep.pkg_hexagon_forward (X Y Z : DeepInterface) : PkgHom.comp (assocIso X Y Z).hom ((PkgHom.braiding X (tensorObj Y Z)).comp (assocIso Y Z X).hom) = ((PkgHom.braiding X Y).whiskerRight Z).comp (PkgHom.comp (assocIso Y X Z).hom (PkgHom.whiskerLeft Y (PkgHom.braiding X Z)))

theorem CatCrypt.Deep.pkg_hexagon_reverse (X Y Z : DeepInterface) : PkgHom.comp (assocIso X Y Z).inv ((PkgHom.braiding (tensorObj X Y) Z).comp (assocIso Z X Y).inv) = (PkgHom.whiskerLeft X (PkgHom.braiding Y Z)).comp (PkgHom.comp (assocIso X Z Y).inv ((PkgHom.braiding X Z).whiskerRight Y))

theorem CatCrypt.Deep.pkg_symmetry (X Y : DeepInterface) : (PkgHom.braiding X Y).comp (PkgHom.braiding Y X) = PkgHom.id (tensorObj X Y)

Braiding is a symmetric involution.