2. Universe handling🔗

The first step in the translation of kernel equalities into categorical equalities is to handle universe levels carefully as categorical expressions occur in a common universe level, while kernels may have carrier spaces in different universe levels.

For instance, consider a category C with objects in universe u and morphisms in universe v:

C : Type u

c ⟶ c' : Type v

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:

Kernel X Y : Type (max 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:

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 Y

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

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, the first step is to lift all kernels' 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:

κ ∘ₖ η : Kernel Z Y

Kernel Z Y : Type (max z y)

The type of the composition κ ∘ₖ η has universe level max y z. The SFinKer counterpart of this expression would be η.hom ≫ κ.hom, where Kernel.hom would represent the translation of a kernel into a morphism in SFinKer. However, to transform κ and η into morphisms, we need to lift their carrier space X (along with Y and Z) to a common level. If we naively try 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 type of the final expression but still need consistent lifting.

To automate this, the lift_eq tactic computes the maximum universe level of all carrier spaces in the kernel expression through the collectExprUniverses function, and lifts all carrier spaces to this level using ulift. One can then translate the lifted kernel expression into a categorical expression in SFinKer without worrying about universe inconsistencies.

The collectExprUniverses function has the following type signature:

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

The lift_eq tactic is not confined to kernel expressions alone. Thanks to its modular design, it can be extended to other kinds of expressions, using the operators and primitives specific to that type. It is thus a general-purpose tactic for raising expressions to a shared universe level, and can be applied in other settings where universe levels need to be reconciled. It is available as a standalone project on GitHub. The reverse tactic, unlift_eq, is also included; it carries out the opposite operation of lift_eq, restoring a lifted expression to its original universe levels.

EqLift : ParserDescr
EqLift : ParserDescr

EqUnlift : ParserDescr
EqUnlift : ParserDescr