2. Universe handling🔗

To translate kernel equalities into categorical equalities, one needs to handle universe levels carefully as categorical expressions occur in a common universe level:

variable {C : Type u} [Category.{v, u} C] (c c' : C)
C : Type u#check C
c ⟶ c' : Type v#check c ⟶ c'

One can see that the objects of the category are terms of C : Type u, and the morphisms are terms of c ⟶ c' : Type v

In the context of kernel equalities, we often have kernels where the carrier spaces have different universe levels:

variable {X : Type x} {Y : Type y} [MeasurableSpace X] [MeasurableSpace Y]
Kernel X Y : Type (max x y)#check Kernel X Y

Here, Kernel X Y has a universe level that depends on the universe levels of X and Y: max x y.

The counterpart of Kernel X Y in the SFinKer category would be SFinKer.of X ⟶ SFinKer.of Y. However, it fails to typecheck as X and Y have different universe levels:

{ carrier := X, str := inst✝¹ } ⟶ sorry : Type x#check SFinKer.of X ⟶ SFinKer.of Application type mismatch: The argument
  Y
has type
  Type y
of sort `Type (y + 1)` but is expected to have type
  Type x
of sort `Type (x + 1)` in the application
  @SFinKer.of YY

To solve this issue, one can manually lift the carrier spaces to a common universe level using ULift:

{ carrier := ULift.{max x y, x} X, str := ULift.instMeasurableSpace } ⟶
  { carrier := ULift.{x, y} Y, str := ULift.instMeasurableSpace } : Type (max x y)#check SFinKer.of (ULift.{max x y} X) ⟶ SFinKer.of (ULift Y)

In this setting, both ULift X and ULift Y have the same universe level, allowing the expression to typecheck correctly, as a morphism in SFinKer.{max x y}.

To translate an equality of kernels into an equality of morphisms in SFinKer, all kernels must be translated to morphisms in SFinKer by lifting their carrier spaces to a common universe level, using the ulift measurable equivalence. However, determining this common universe level requires care.

One might naively take the universe level of the equality's result (left or right-hand side), but this can fail. Consider the following example:

variable {Z : Type z} [MeasurableSpace Z] {κ : Kernel X Y} {η : Kernel Z X}
κ ∘ₖ η : Kernel Z Y#check κ ∘ₖ η
Kernel Z Y : Type (max z y)#check Kernel Z Y

The type of the composition κ ∘ₖ η has universe level max y z. However, to transform κ into a morphism in SFinKer, we must lift its carrier space X (along with Y) to a common level. If one naively tries to lift X to only max y z, it is impossible because x might be larger than max y z: we cannot lift a type from a larger universe to a smaller one.

The correct approach is to lift all carrier spaces to the maximum universe level of every space in the entire expression, which is max x y z in this example. This includes spaces that may "disappear" in the final result but still need consistent lifting.

To automate this, the collectExprUniverses function recursively collects all universe levels found in an expression. This allows us to determine the appropriate common universe level and uniformly lift all carrier spaces to it.

def

collectExprUniverses (e : Expr) : MetaM (List Level)
collectExprUniverses (e : Expr) :
  MetaM (List Level)

Recursively traverse an expression and collect universe levels found. Returns a list of all unique universe levels encountered.