Kernel lifting utilities

This file provides helper functions for lifting and unlifting kernel expressions, including type extraction and equivalence construction.

Main declarations

• getTypesFromKernel: extracts carrier types and universe levels from kernel expressions.
• constructMeasurableEquiv: recursively builds measurable equivalences.
• getOriginalType: retrieves the original type from a lifted type.

def getTypesFromKernel (κ : 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 constructMeasurableEquiv (e : Lean.Expr) (eLevel maxLvl : Lean.Level) : Lean.MetaM Lean.Expr

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

def getTypesFromMeasurableEquiv (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Get departure and target types from a MeasurableEquiv expression.

Equations

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

partial def getOriginalType (t : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Level)

Get the original type from a lifted type.