Natural equivalences and kernel performance

Stream: maths

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I have been working on a formalization project involving lots of universal properties expressed as natural equivalences between hom-types in categories.

Let me give you three examples, where $𝒞(X,Y)$ denotes the hom-type $X ⟶ Y$ for $X,Y : 𝒞$.

• For adjunctions $F ⊣ G$, we have the usual correspondence $𝒟(F(X), Y) ≃ 𝒞(X, G(Y))$.
• For products (in fact any limit), we have $𝒞(Z, X×Y) ≃ 𝒞(Z, X) × 𝒞(Z, Y)$.
• For $P: 𝒞 ⥤ 𝒞$ a polynomial functor on a map $p : 𝒞(E,B)$ (whatever that means), $𝒞(X, P(Y)) ≃ (b : 𝒞(X, B)) × 𝒞(b^*p, Y)$ (dependent pair on the right, and $b^*p$ means the corner of the pullback of $b$ along $p$).

In mathlib, bijections of this kind seem to usually be formalized as Equivs, e.g. docs#CategoryTheory.Adjunction.homEquiv.

However, there is more to this than an Equiv: the bijections are also natural, meaning they behave well on compositions. For example, if $i : 𝒟(F(X), Y) ≃ 𝒞(X, G(Y))$ for an adjunction, then $i(f ≫ g) = i(f) ≫ G(g)$; this is docs#CategoryTheory.Adjunction.homEquiv_naturality_right.

Now, one sometimes build up larger equivalences by composing smaller ones. The example I have in mind is the equivalence for polynomial functors; it can be obtained (e.g. here) as

𝒞(X,P(Y)) ≃ 𝒞(X,∑_{!_B}∏_p(!^*_E(Y)))
  ≃ ∑_{b:X⟶B}𝒞/B(b,∏_p(!^*_E(Y)))
  ≃ ∑_{b:X⟶B}𝒞/E(p^*b,!^*_E(Y))
  ≃ ∑_{b:X⟶B}𝒞(p^*b,Y)

We may now ask: why is this natural? On paper, the answer is 'obviously, because it's a composition of natural bijections'. In Lean, however, with the current approach we'd have to state naturality_left, naturality_right, etc., and prove all of these one-by-one by applying naturality laws for the smaller equivalences used as building blocks. This gets a bit painful for sufficiently complex equivalences, and is also very repetitive: here is one such proof I did last year.

In order to avoid doing more of these, I have been testing out an approach to formalizing the 'obviously' proof. The idea is that a natural equivalence is actually a natural isomorphism of functors into the category of types. For these, naturality is built-in as one of the fields, and crucially we get it for free when isomorphisms are composed. Here is that polynomial functor equivalence, now using the functor approach. Recovering mathlib-style naturality laws takes two lines.

Unfortunately, this approach has serious performance issues. The problem is that to even state the two sides of the equivalence, we need to write down what functors they are given by; e.g. $(X,Y) ↦ 𝒞(X,P(Y))$ is P ⋙₂ coyoneda, and the RHS is a complicated thing involving Functor.Sigma (which I defined for this purpose).

In order to recover an ordinary Equiv from the isomorphism, Lean has to see through the action of this functor on objects and compute the original hom-type; this may fall under 'defeq abuse'.

For example, in

def equiv (Γ X : C) : (Γ ⟶ P.functor.obj X) ≃ (b : Γ ⟶ B) × (pullback b P.p ⟶ X) :=
  Iso.toEquiv <| (P.iso_Sigma.app (.op Γ)).app X

theorem equiv_app (Γ X : C) (be : Γ ⟶ P.functor.obj X) :
    P.equiv Γ X be = (P.iso_Sigma.hom.app <| .op Γ).app X be := by
  dsimp [equiv]

the expected type of be appearing as an argument to (P.iso_Sigma.hom.app <| .op Γ).app X is ((P.functor ⋙₂ coyoneda).obj (op Γ)).obj X, which indeed computes down to Γ ⟶ P.functor.obj X. The RHS is analogous, except more computation is involved. The end result is that I have theorems which take ~0.3s to prove by simp (so they are fast with set_option debug.skipKernelTC true), but for which kernel typechecking takes ~10s, and in one pathological case upwards of a minute (!).

I like being able to skip bunch of gnarly proofs, but I have been unable to make this approach work at reasonable speeds.

I am wondering if anybody else has thought about:

• different ways of stating natural equivalences/universal properties that make 'trivial' naturality proofs trivial in Lean; or
• improving performance in similar situations that seem to rely on defeq abuse; or
• anything else related to this topic and my issue.