1. 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 C live in Type u, while the morphisms live in Type v.

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

variable {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
Kernel X Y : Type (max u_1 u_2)#check Kernel X Y

Here, Kernel X Y lives in a universe level that depends on the universe levels of X and 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 live in different universe levels:

{ carrier := X, str := inst✝¹ } ⟶ sorry : Type u_1#check SFinKer.of X ⟶ SFinKer.of Application type mismatch: The argument
  Y
has type
  Type u_2
of sort `Type (u_2 + 1)` but is expected to have type
  Type u_1
of sort `Type (u_1 + 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 u_1 u_2, u_1} X, str := ULift.instMeasurableSpace } ⟶
  { carrier := ULift.{u_1, u_2} Y, str := ULift.instMeasurableSpace } : Type (max u_1 u_2)#check SFinKer.of (ULift.{max u_1 u_2} X) ⟶ SFinKer.of (ULift Y)

In this setting, both ULift X and ULift Y live in the same universe level, allowing the expression to typecheck correctly.

However, manually uniformizing universe levels can be cumbersome when dealing with expressions involving multiple kernels of different carrier spaces. To this end, we designed the collectExprUniverses function, which recursively traverses an expression and collects all universe levels found. This allows us to automatically determine the minimum common universe level for which all carrier spaces of the kernels involved in a given expression can be lifted to (most likely the maximum of all universe levels encountered), and uniformly lift them to that level during the translation process.