Monoidal Bridge: DeepPackage ↔ PkgInterface SMC

This file connects the concrete package operations (DeepPackage.par, link) to the symmetric monoidal category on PkgInterface (from SemPkg.lean).

Main Results

• tensorAppendIso — toPkgInterface(I.append J) ≅ toPkgInterface(I) ⊗ toPkgInterface(J)
• unitIso — toPkgInterface(⟨[]⟩) ≅ 𝟙_
• diAppend_assoc / diAppend_empty_* — algebraic laws for diAppend
• appendAssocIso — coherence iso from List.append_assoc
• tensorAppend_assoc_coherence — pentagon coherence (stated, see note)

Architecture

The PkgInterface SMC (from SemPkg.lean) uses Sum-indexed families with definitional coherence (funext + cases + rfl). The concrete DeepInterface uses List-indexed families with diAppend = List.append as tensor.

The key difficulty: Fin (m + n) vs Fin m ⊕ Fin n. The tensorAppendIso bridges this gap using castKl' (proof-irrelevant transport on Kleisli arrows) with the roundtrip proofs handled by castKl'_castKl'_symm and castKl'_dep_fn (dependent function transport).

@[reducible, inline]

abbrev CatCrypt.Bridge.MonoidalBridge.toPI (I : Deep.DeepInterface) : Category.PkgInterface

Equations

• CatCrypt.Bridge.MonoidalBridge.toPI = CatCrypt.Category.DeepInterface.toPkgInterface

@[reducible, inline]

abbrev CatCrypt.Bridge.MonoidalBridge.diAppend (I J : Deep.DeepInterface) : Deep.DeepInterface

Equations

• CatCrypt.Bridge.MonoidalBridge.diAppend = CatCrypt.Category.DeepInterface.append

Family Correspondence

Type-level cast for operation families

Tensor-Append Isomorphism

noncomputable def CatCrypt.Bridge.MonoidalBridge.appendToTensor (I J : Deep.DeepInterface) : toPI (diAppend I J) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (toPI I) (toPI J)

Forward: handler for diAppend I J → handler for toPI I ⊗ toPI J.

Equations

• CatCrypt.Bridge.MonoidalBridge.appendToTensor I J h (Sum.inl i) = CatCrypt.Bridge.MonoidalBridge.castKl'✝ ⋯ (h ⟨↑i, ⋯⟩)
• CatCrypt.Bridge.MonoidalBridge.appendToTensor I J h (Sum.inr j) = CatCrypt.Bridge.MonoidalBridge.castKl'✝ ⋯ (h ⟨I.ops.length + ↑j, ⋯⟩)

noncomputable def CatCrypt.Bridge.MonoidalBridge.tensorToAppend (I J : Deep.DeepInterface) : CategoryTheory.MonoidalCategoryStruct.tensorObj (toPI I) (toPI J) ⟶ toPI (diAppend I J)

Inverse: handler for toPI I ⊗ toPI J → handler for diAppend I J.

Equations

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

noncomputable def CatCrypt.Bridge.MonoidalBridge.tensorAppendIso (I J : Deep.DeepInterface) : toPI (diAppend I J) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (toPI I) (toPI J)

The tensor-append isomorphism in the PkgInterface category.

This is the fundamental bridge between DeepInterface.append (list concat, Fin-indexed) and PkgInterface.tensor (Sum-indexed).

Equations

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

Unit Correspondence

noncomputable def CatCrypt.Bridge.MonoidalBridge.unitIso : toPI { ops := [] } ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit Category.PkgInterface

The empty deep interface maps to the monoidal unit.

Equations

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

Structural Properties of diAppend

theorem CatCrypt.Bridge.MonoidalBridge.diAppend_assoc (I J K : Deep.DeepInterface) : diAppend (diAppend I J) K = diAppend I (diAppend J K)

diAppend is associative: (I ++ J) ++ K = I ++ (J ++ K) as DeepInterfaces.

theorem CatCrypt.Bridge.MonoidalBridge.diAppend_empty_right (I : Deep.DeepInterface) : diAppend I { ops := [] } = I

Right unit: diAppend I ⟨[]⟩ = I.

theorem CatCrypt.Bridge.MonoidalBridge.diAppend_empty_left (I : Deep.DeepInterface) : diAppend { ops := [] } I = I

Left unit: diAppend ⟨[]⟩ I = I.

noncomputable def CatCrypt.Bridge.MonoidalBridge.appendAssocIso (I J K : Deep.DeepInterface) : toPI (diAppend (diAppend I J) K) ≅ toPI (diAppend I (diAppend J K))

The PkgInterface iso induced by associativity of diAppend.

Equations

• CatCrypt.Bridge.MonoidalBridge.appendAssocIso I J K = CategoryTheory.eqToIso ⋯

noncomputable def CatCrypt.Bridge.MonoidalBridge.appendEmptyRightIso (I : Deep.DeepInterface) : toPI (diAppend I { ops := [] }) ≅ toPI I

The PkgInterface iso from right-unit of diAppend.

Equations

• CatCrypt.Bridge.MonoidalBridge.appendEmptyRightIso I = CategoryTheory.eqToIso ⋯

noncomputable def CatCrypt.Bridge.MonoidalBridge.appendEmptyLeftIso (I : Deep.DeepInterface) : toPI (diAppend { ops := [] } I) ≅ toPI I

The PkgInterface iso from left-unit of diAppend.

Equations

• CatCrypt.Bridge.MonoidalBridge.appendEmptyLeftIso I = CategoryTheory.eqToIso ⋯

Coherence

The associator pentagon: the two paths from toPI((I++J)++K) to toPI I ⊗ (toPI J ⊗ toPI K) commute.

Note: The proof requires unfolding eqToHom (from appendAssocIso) into explicit castKl' form. The approach is:

1. Define appendAssocIso explicitly via castKl' (like tensorAppendIso)
2. Use castKl'_trans + castKl'_dep_fn + proof irrelevance Both paths compute castKl' at the same Fin.val index with propositionally equal operation triples, so the casts agree by proof irrelevance.

theorem CatCrypt.Bridge.MonoidalBridge.tensorAppend_assoc_coherence (I J K : Deep.DeepInterface) : CategoryTheory.CategoryStruct.comp (tensorAppendIso (diAppend I J) K).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (tensorAppendIso I J).hom (toPI K)) (CategoryTheory.MonoidalCategoryStruct.associator (toPI I) (toPI J) (toPI K)).hom) = CategoryTheory.CategoryStruct.comp (appendAssocIso I J K).hom (CategoryTheory.CategoryStruct.comp (tensorAppendIso I (diAppend J K)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (toPI I) (tensorAppendIso J K).hom))

Linking = Categorical Composition

toSemPkg maps DeepPackage.link to composition in Category DeepInterface. This is the fundamental functoriality theorem connecting the concrete package operation to the categorical structure.

Note: toSemPkg is NOT a strict functor — it does not preserve identity exactly. toSemPkg(DeepPackage.id I) returns fail on non-interface operations, while 𝟙 I = SemPkg.id I passes them through. Identity is only preserved on interface operations (see toSemPkg_id_mem and evalImpl_link_id_left/right).

theorem CatCrypt.Bridge.MonoidalBridge.toSemPkg_link_resolve (p₁ p₂ : Deep.DeepPackage) (oracle : Handler) : (toSemPkg (p₁.link p₂)).resolve oracle = (toSemPkg p₁).resolve ((toSemPkg p₂).resolve oracle)

toSemPkg preserves linking at the handler level: toSemPkg(link p₁ p₂).resolve = toSemPkg(p₁).resolve ∘ toSemPkg(p₂).resolve.

theorem CatCrypt.Bridge.MonoidalBridge.toSemPkg_link_comp (p₁ p₂ : Deep.DeepPackage) (h : p₁.imports = p₂.exports) : toSemPkg (p₁.link p₂) = (h ▸ toSemPkg p₁).comp (toSemPkg p₂)

toSemPkg preserves linking as SemPkg.comp: toSemPkg(link p₁ p₂) = toSemPkg(p₁).comp(toSemPkg(p₂)).

Requires p₁.imports = p₂.exports for the composition to be well-typed.

theorem CatCrypt.Bridge.MonoidalBridge.toSemPkg_link_cat (p₁ p₂ : Deep.DeepPackage) (h : p₁.imports = p₂.exports) : toSemPkg (p₁.link p₂) = CategoryTheory.CategoryStruct.comp (toSemPkg p₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (toSemPkg p₁))

toSemPkg preserves linking as categorical composition ≫ in Category DeepInterface (where f ≫ g = g.comp f): toSemPkg(link p₁ p₂) = toSemPkg(p₂) ≫ eqToHom(h.symm) ≫ toSemPkg(p₁).

Unitor Coherence

The unitor bridges: the two paths from toPI(I ++ ⟨[]⟩) to toPI(I) via (1) the append-empty iso, or (2) tensor-append iso + unitIso + monoidal unitor, are equal. Similarly for the left unitor.

theorem CatCrypt.Bridge.MonoidalBridge.tensorAppend_rightUnitor_coherence (I : Deep.DeepInterface) : CategoryTheory.CategoryStruct.comp (tensorAppendIso I { ops := [] }).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (toPI I) unitIso.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor (toPI I)).hom) = (appendEmptyRightIso I).hom

Right unitor coherence: the two paths from toPI(I ++ ⟨[]⟩) to toPI(I) agree. Path 1: toPI(I++⟨[]⟩) → toPI(I) ⊗ toPI(⟨[]⟩) → toPI(I) ⊗ 𝟙_ → toPI(I) Path 2: toPI(I++⟨[]⟩) → toPI(I) directly via appendEmptyRightIso.

theorem CatCrypt.Bridge.MonoidalBridge.tensorAppend_leftUnitor_coherence (I : Deep.DeepInterface) : CategoryTheory.CategoryStruct.comp (tensorAppendIso { ops := [] } I).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight unitIso.hom (toPI I)) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (toPI I)).hom) = (appendEmptyLeftIso I).hom

Left unitor coherence: the two paths from toPI(⟨[]⟩ ++ I) to toPI(I) agree. Path 1: toPI(⟨[]⟩++I) → toPI(⟨[]⟩) ⊗ toPI(I) → 𝟙_ ⊗ toPI(I) → toPI(I) Path 2: toPI(⟨[]⟩++I) → toPI(I) directly via appendEmptyLeftIso.

Braiding Bridge

noncomputable def CatCrypt.Bridge.MonoidalBridge.diAppend_braiding_iso (I J : Deep.DeepInterface) : toPI (diAppend I J) ≅ toPI (diAppend J I)

Braiding bridge: composing the tensor-append iso with braiding and the inverse tensor-append iso gives the concrete swap.

Equations

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