Kernel category tactics

This file implements the kernel_coherence and kernel_monoidal tactics, which apply the kernel_hom transformation and then use categorical coherence or monoidal tactics to solve the resulting goal.

Main declarations

• kernel_coherence: tactic combining kernel_hom and categorical coherence.
• kernel_monoidal: tactic combining kernel_hom and categorical monoidal coherence.

def kernelCoherence : Lean.ParserDescr

The kernel_coherence tactic applies the kernel_hom transformation to the goal and then invokes the coherence tactic to solve the resulting goal.

Equations

• kernelCoherence = Lean.ParserDescr.node `kernelCoherence 1024 (Lean.ParserDescr.nonReservedSymbol "kernel_coherence" false)

def kernelMonoidal : Lean.ParserDescr

The kernel_coherence tactic applies the kernel_hom transformation to the goal and then invokes the monoidal tactic to solve or simplify the resulting goal.

Equations

• kernelMonoidal = Lean.ParserDescr.node `kernelMonoidal 1024 (Lean.ParserDescr.nonReservedSymbol "kernel_monoidal" false)