Increasing Universe Polymorphism in Yoneda lemma

[maxsnew]

I'm currently developing some category theory where I'm heavily using presheaves and the Yoneda lemma. In doing so I've found that the universe polymorphism in the statement in the Yoneda lemma is a bit restrictive: the universe level of the presheaf is restricted to be the same as the level of the homs of the category (https://github.com/agda/cubical/blob/7c45b3776ea0dca5290a35ac02084fdfaf123bd8/Cubical/Categories/Yoneda.agda):

module _ {C : Category ℓ ℓ'} where
  open Category

  yoneda : (F : Functor C (SET ℓ'))
         → (c : C .ob)
         → Iso ((FUNCTOR C (SET ℓ')) [ C [ c ,-] , F ]) (fst (F ⟅ c ⟆))

But it could be made more general in the following way:

  module _ {C : Category ℓ ℓ'} where
  open Category

  yoneda : (F : Functor C (SET ℓ''))
         → (c : C .ob)
         → Iso ((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) [ LiftF {ℓ'}{ℓ''} ∘F (C [ c ,-]) , LiftF {ℓ''}{ℓ'} ∘F F ]) (fst (F ⟅ c ⟆))

where LiftF : Functor (SET ℓ) (SET (ℓ-max ℓ ℓ')) is the functor version of Lift.

This is essential if we want to relate representability in terms of presheaves with notions like limits as defined in the library. The presheaf of cones involved in the notion of limit defined here does not fit into the more restrictive version because the indexing category and the category we are taking the limit in are allowed to have different universes.

I'm going to write this updated version, but it would be backwards-incompatible change since the type of yoneda would be different. What's the policy on such a change? Should I give it a different name and keep the old version/implement the old version using the more general one? Is there a naming policy for this kind of thing (a more cumbersome but more universe-polymorphic version of a definition)?

[ecavallo]

I think it could be useful to keep the old version, so that the Lifts can be avoided when possible. But I also don't like the code duplication, which I see no way to avoid...

Maybe it could be called yoneda* by analogy with Unit*? But this is not a great convention...

[maxsnew]

Surprisingly (to me) it doesn't require any code duplication, just some straightforward but tedious Isos involving Lift: https://github.com/maxsnew/cubical/blob/more-representable/Cubical/Categories/Yoneda.agda#L148

I like yoneda*, I called it yonedaPoly above but I think * for a universe polymorphic version is a nice mnemonic that's already established.

[maxsnew]

Implemented in #988