transformHomToKernel
Opaque
Recursive transformation from morphism expression in SFinKer to kernel expression.
opaque
transformHomToKernel (e : Lean.Expr) (proofs : List Lean.Expr) : Lean.MetaM (Lean.Expr × List Lean.Expr)transformHomToKernel (e : Lean.Expr) (proofs : List Lean.Expr) : Lean.MetaM (Lean.Expr × List Lean.Expr)
Code
partial def transformHomToKernel (e : Expr) (proofs : List Expr) :
MetaM (Expr × List Expr)Proof
do
match e.getAppFn with
| Expr.const ``tensorHom _ =>
let args := e.getAppArgs
let κ := args[args.size - 2]!
let η := args[args.size - 1]!
let ST := args[args.size - 3]!
let SZ := args[args.size - 4]!
let SY := args[args.size - 5]!
let SX := args[args.size - 6]!
let (κ', proofs_κ) ← transformHomToKernel κ proofs
let (η', proofs_η) ← transformHomToKernel η proofs_κ
let (X, Y, _, _) ← getTypesFromKernel κ'
let (Z, T, _, _) ← getTypesFromKernel η'
let parallelComp_hom_proof ← mkAppMInst ``parallelComp_hom
#[SX, SY, SZ, ST, ← idME X, ← idME Y, ← idME Z, ← idME T, κ', η'] 2
return (← mkAppM ``Kernel.parallelComp #[κ', η'], parallelComp_hom_proof :: proofs_η)
| Expr.const ``CategoryStruct.comp _ =>
let args := e.getAppArgs
let κ := args[args.size - 2]!
let η := args[args.size - 1]!
let SY := args[args.size - 3]!
let SX := args[args.size - 4]!
let SZ := args[args.size - 5]!
let (κ', proofs_κ) ← transformHomToKernel κ proofs
let (η', proofs_η) ← transformHomToKernel η proofs_κ
let (X, Y, _, _) ← getTypesFromKernel η'
let (Z, _, _, _) ← getTypesFromKernel κ'
let comp_hom_proof ← mkAppMInst ``comp_hom
#[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, η', κ'] 2
return (← mkAppM ``Kernel.comp #[η', κ'], comp_hom_proof :: proofs_η)
| Expr.const ``CategoryStruct.id [xLvl, _] =>
let args := e.getAppArgs
let SX := args[args.size - 1]!
let X ← getTypeFromSFinKer SX
let mX' ← synthInstance (mkApp (mkConst ``MeasurableSpace [xLvl]) X)
let id ← mkAppOptM ``Kernel.id #[X, mX']
let id_hom_proof ← mkAppM ``id_hom #[SX, ← idME X]
return (id, id_hom_proof :: proofs)
| Expr.const ``ComonObj.counit [xLvl, _] =>
let args := e.getAppArgs
let SX := args[args.size - 2]!
let X ← getTypeFromSFinKer SX
let discard_kernel_const := mkConst ``Kernel.discard [xLvl, xLvl]
let discard_const := mkConst ``counit [xLvl, xLvl, xLvl]
let discard_hom_proof ← mkAppM' discard_const #[SX, ← idME X]
return (← mkAppOptM' discard_kernel_const #[X, none], discard_hom_proof :: proofs)
| Expr.const ``ComonObj.comul [xLvl, _] =>
let args := e.getAppArgs
let SX := args[args.size - 2]!
let X ← getTypeFromSFinKer SX
let copy_kernel_const := mkConst ``Kernel.copy [xLvl]
let copy_hom_proof ← mkAppM ``comul #[SX, ← idME X]
return (← mkAppOptM' copy_kernel_const #[X, none], copy_hom_proof :: proofs)
| Expr.const ``Kernel.hom _ =>
let args := e.getAppArgs
let κ := args[args.size - 2]!
return (κ, proofs)
| Expr.const ``MonoidalCategory.whiskerLeft [eLvl, _] =>
let (κ, kernel_id, SX, SY, SZ, X, Y, Z) ← deconstructWhiskersHomArgs e eLvl true
let (κ', proofs_κ) ← transformHomToKernel κ proofs
let whisker_left_hom_proof ← mkAppMInst ``Kernel.whiskerLeft
#[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ'] 1
return (← mkAppM ``Kernel.parallelComp #[kernel_id, κ'], whisker_left_hom_proof :: proofs_κ)
| Expr.const ``MonoidalCategory.whiskerRight [eLvl, _] =>
let (κ, kernel_id, SX, SY, SZ, X, Y, Z) ← deconstructWhiskersHomArgs e eLvl false
let (κ', proofs_κ) ← transformHomToKernel κ proofs
let whisker_right_hom_proof ← mkAppMInst ``Kernel.whiskerRight
#[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ'] 1
return (← mkAppM ``Kernel.parallelComp #[κ', kernel_id], whisker_right_hom_proof :: proofs_κ)
| Expr.const ``Iso.hom _ =>
let args := e.getAppArgs
let iso := args[args.size - 1]!
match iso.getAppFn with
| Expr.const ``BraidedCategory.braiding _ =>
let (braiding_expr, swap_hom_proof) ← deconstructBraiding iso
return (braiding_expr, swap_hom_proof :: proofs)
| Expr.const ``leftUnitor [eLvl, _] =>
let (left_unitor_expr, left_unitor_hom_proof) ← deconstructUnitors iso eLvl true true
return (left_unitor_expr, left_unitor_hom_proof :: proofs)
| Expr.const ``rightUnitor [eLvl, _] =>
let (right_unitor_expr, right_unitor_hom_proof) ← deconstructUnitors iso eLvl false true
return (right_unitor_expr, right_unitor_hom_proof :: proofs)
| Expr.const ``MonoidalCategory.associator [eLvl, _] =>
let (associator_expr, associator_hom_proof) ← deconstructAssociator iso eLvl true
return (associator_expr, associator_hom_proof :: proofs)
| _ => throwError "Unexpected isomorphism {iso}."
| Expr.const ``Iso.inv _ =>
let args := e.getAppArgs
let iso := args[args.size - 1]!
match iso.getAppFn with
| Expr.const ``BraidedCategory.braiding _ =>
let (braiding_expr, swap_hom_proof) ← deconstructBraiding iso
return (braiding_expr, swap_hom_proof :: proofs)
| Expr.const ``leftUnitor [eLvl, _] =>
let (left_unitor_expr, left_unitor_inv_hom_proof) ← deconstructUnitors iso eLvl true false
return (left_unitor_expr, left_unitor_inv_hom_proof :: proofs)
| Expr.const ``rightUnitor [eLvl, _] =>
let (right_unitor_expr, right_unitor_inv_hom_proof) ← deconstructUnitors iso eLvl false false
return (right_unitor_expr, right_unitor_inv_hom_proof :: proofs)
| Expr.const ``MonoidalCategory.associator [eLvl, _] =>
let (associator_expr, associator_inv_hom_proof) ← deconstructAssociator iso eLvl false
return (associator_expr, associator_inv_hom_proof :: proofs)
| _ => throwError "Unexpected isomorphism {iso}."
| _ => throwError "Expected a hom expression, got: {e}."Actions: Source · Open Issue
Meaning last changed in v4.34.0-rc2-1-g439785b (2026-08-23).
Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.
Dependency graph
Nothing to draw. Its statement rests on no other declaration in this project, and names nothing from a package left unaudited — so the graph is this declaration alone. That is the answer, not a missing picture.
Audit surface: 0 project declarations, 4 external constants
✓ Proved: no sorry anywhere in its closure
This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.