Kernel transformation utilities

This file provides helper functions for transforming between kernel expressions and categorical morphism expressions, including type extraction and equivalence construction.

Main declarations

• get_types_from_kernel: extracts carrier types and universe levels from kernel expressions.
• construct_measurable_equiv: recursively builds measurable equivalences.
• transformEquality: transforms an equality expression to an other using a provided transformation function.
• unfold_kernel_op: unfolds kernel operations in an expression for easier matching.

def get_types_from_kernel (κ : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Level × Lean.Level)

Extract (X, Y, u, v) from an expression of type Kernel X Y.

Equations

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

partial def construct_measurable_equiv (e : Lean.Expr) (eLevel maxLvl : Lean.Level) : Lean.MetaM Lean.Expr

Build a measurable equivalence for e into universe maxLvl (recursive on products).

inductive CategoryOP : Type

Categorical operations recorded during transformation for later rewriting.

• leftUnitor_hom (lvl : Lean.Level) (e : Lean.Expr) : CategoryOP
• leftUnitor_inv (lvl : Lean.Level) (e : Lean.Expr) : CategoryOP
• rightUnitor_hom (lvl : Lean.Level) (e : Lean.Expr) : CategoryOP
• rightUnitor_inv (lvl : Lean.Level) (e : Lean.Expr) : CategoryOP
• WhiskerLeft (e : Lean.Expr) : CategoryOP
• WhiskerRight (e : Lean.Expr) : CategoryOP
• id (e : Lean.Expr) : CategoryOP
• Associator_hom (e₁ e₂ e₃ : Lean.Expr) : CategoryOP
• Associator_inv (e₁ e₂ e₃ : Lean.Expr) : CategoryOP
• Braiding_hom (e₁ e₂ : Lean.Expr) : CategoryOP
• Counit (e : Lean.Expr) : CategoryOP
• Comul (e : Lean.Expr) : CategoryOP

def transformEquality (maxLvl : Lean.Level) (e : Lean.Expr) (transform : Lean.Level → Lean.Expr → List CategoryOP → Lean.MetaM (Lean.Expr × List CategoryOP)) : Lean.MetaM (Lean.Expr × List CategoryOP × Lean.Expr × Lean.Expr)

Transform both sides of an equality and return the new equality plus metadata.

Equations

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

def unfold_kernel_op (e : Lean.Expr) : Lean.MetaM Lean.Expr

Unfold kernel operations in an expression.

Equations

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