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

theorem CatCrypt.Bridge.MonoidalBridge.ops_get_left (I J : Deep.DeepInterface) (i : Fin I.ops.length) : (I.ops ++ J.ops).get ⟨↑i, ⋯⟩ = I.ops.get i

theorem CatCrypt.Bridge.MonoidalBridge.ops_get_right (I J : Deep.DeepInterface) (j : Fin J.ops.length) : (I.ops ++ J.ops).get ⟨I.ops.length + ↑j, ⋯⟩ = J.ops.get j

theorem CatCrypt.Bridge.MonoidalBridge.ops_get_dispatch_left (I J : Deep.DeepInterface) {k : Fin (I.ops ++ J.ops).length} (hk : ↑k < I.ops.length) : (I.ops ++ J.ops).get k = I.ops.get ⟨↑k, hk⟩

theorem CatCrypt.Bridge.MonoidalBridge.ops_get_dispatch_right (I J : Deep.DeepInterface) {k : Fin (I.ops ++ J.ops).length} (hk : ¬↑k < I.ops.length) : (I.ops ++ J.ops).get k = J.ops.get ⟨↑k - I.ops.length, ⋯⟩

Type-level cast for operation families

noncomputable def CatCrypt.Bridge.MonoidalBridge.castKl' {t₁ t₂ : ℕ × Type × Type} (h : t₁ = t₂) (f : t₁.2.1 → Core.SPComp t₁.2.2) : t₂.2.1 → Core.SPComp t₂.2.2

Transport a Kleisli arrow along an equality of operation triples. Defined via ▸ (Eq.mpr), so the transport is proof-irrelevant in h.

Equations

• CatCrypt.Bridge.MonoidalBridge.castKl' h f = Eq.rec (motive := fun (x : ℕ × Type × Type) (h : t₁ = x) => x.2.1 → CatCrypt.Core.SPComp x.2.2) f h

@[simp]

theorem CatCrypt.Bridge.MonoidalBridge.castKl'_rfl {t : ℕ × Type × Type} (f : t.2.1 → Core.SPComp t.2.2) : castKl' ⋯ f = f

@[simp]

theorem CatCrypt.Bridge.MonoidalBridge.castKl'_castKl'_symm {t₁ t₂ : ℕ × Type × Type} (h₁ : t₁ = t₂) (h₂ : t₂ = t₁) (f : t₁.2.1 → Core.SPComp t₁.2.2) : castKl' h₂ (castKl' h₁ f) = f

@[simp]

theorem CatCrypt.Bridge.MonoidalBridge.castKl'_trans {t₁ t₂ t₃ : ℕ × Type × Type} (h₁ : t₁ = t₂) (h₂ : t₂ = t₃) (f : t₁.2.1 → Core.SPComp t₁.2.2) : castKl' h₂ (castKl' h₁ f) = castKl' ⋯ f

theorem CatCrypt.Bridge.MonoidalBridge.castKl'_dep_fn {ι : Type} {F : ι → ℕ × Type × Type} {a b : ι} (hab : a = b) (f : (i : ι) → (F i).2.1 → Core.SPComp (F i).2.2) (eq : F a = F b) : castKl' eq (f a) = f b

A dependent function application transports correctly along castKl'. If a = b as indices and eq is the induced operation equality, then castKl' eq (f a) = f b.

theorem CatCrypt.Bridge.MonoidalBridge.castKl'_dep_fn_congr {ι : Type} {F : ι → ℕ × Type × Type} {t : ℕ × Type × Type} {a b : ι} (hab : a = b) (f : (i : ι) → (F i).2.1 → Core.SPComp (F i).2.2) (eq_a : F a = t) (eq_b : F b = t) : castKl' eq_a (f a) = castKl' eq_b (f b)

Two castKl' applications to the same target agree when the indices are equal.

theorem CatCrypt.Bridge.MonoidalBridge.castKl'_dep_fn_sum {ιL ιR : Type} {F : ιL ⊕ ιR → ℕ × Type × Type} {a b : ιL ⊕ ιR} (hab : a = b) (f : (k : ιL ⊕ ιR) → (F k).2.1 → Core.SPComp (F k).2.2) (eq : F a = F b) : castKl' eq (f a) = f b

Sum-indexed variant of castKl'_dep_fn.

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.eqToHom_handler {I J : Deep.DeepInterface} (h_eq : I = J) (handler : Category.TypedHandler (toPI I)) : CategoryTheory.eqToHom ⋯ handler = h_eq ▸ handler

eqToHom on PkgInterface acts as ▸ (transport) on handlers.

theorem CatCrypt.Bridge.MonoidalBridge.handler_transport_apply {I J : Deep.DeepInterface} (h_eq : I = J) (handler : Category.TypedHandler (toPI I)) (k : (toPI J).ι) : (h_eq ▸ handler) k = castKl' ⋯ (handler ⟨↑k, ⋯⟩)

Transport of a handler along a DeepInterface equality is pointwise identity up to castKl' at the same Fin.val.

@[simp]

theorem CatCrypt.Bridge.MonoidalBridge.tensorAppendIso_hom (I J : Deep.DeepInterface) : (tensorAppendIso I J).hom = appendToTensor I J

@[simp]

theorem CatCrypt.Bridge.MonoidalBridge.appendAssocIso_hom (I J K : Deep.DeepInterface) : (appendAssocIso I J K).hom = CategoryTheory.eqToHom ⋯

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.SemPkg.resolve_transport {I₁ I₂ : Deep.DeepInterface} {I_exp : Deep.DeepInterface} (h : I₁ = I₂) (s : SemPkg I₁ I_exp) : (h ▸ s).resolve = s.resolve

Transport of a SemPkg along an import equality preserves 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.eqToHom_resolve {I J : Deep.DeepInterface} (h : I = J) : (CategoryTheory.eqToHom h).resolve = id

eqToHom in Category DeepInterface preserves resolve.

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.