Equivalence-invariance of constructions on categories

Stream: Is there code for X?

[Brendan Seamas Murphy]

Specifically, if I have e1 : C ≌ C' and e2 : D ≌ D' is there a definition that will give me (C ⥤ D) ≌ (C' ⥤ D') and (C ⥤ D) × (C' ⥤ D') in terms of them?

[Brendan Seamas Murphy]

This follows from the fact that Prod : Cat.{v₁, u₁} × Cat.{v₂, u₂} → Cat.{max v₁ v₂, max u₂ u₁} and Fun : Cat.{v₁, u₁}^op × Cat.{v₂, u₂} → Cat.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} are (strict) 2-functors, but I don't really feel like filling in that theory

(edit: and also it's insufficient when C, C' live in different universes)

[Thomas Browning]

You could combine docs#category_theory.equivalence.congr_left with docs#category_theory.equivalence.congr_right, swapping out one side at a time

[Brendan Seamas Murphy]

oh great, I only needed congr_left. thanks!

[Brendan Seamas Murphy]

(but there's no such code for products still, right?)

[Thomas Browning]

Did you mean to write (C × C') ≌ (D × D')? Not that I could find on a cursory scan of the docs.

[Brendan Seamas Murphy]

Yep, sorry

[Brendan Seamas Murphy]

guess I'll add this to Mathlib.CategoryTheory.Products.Basic

def Equivalence.prodCongr {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
    {C' : Type u₃} [Category.{v₃} C'] {D' : Type u₄} [Category.{v₄} D']
    (e1 : C ≌ C') (e2 : D ≌ D') : C × D ≌ C' × D' where
  functor := e1.functor.prod e2.functor
  inverse := e1.inverse.prod e2.inverse
  unitIso := ⟨NatTrans.prod e1.unitIso.hom e2.unitIso.hom, NatTrans.prod e1.unitIso.inv e2.unitIso.inv, _, _⟩
  counitIso := ⟨NatTrans.prod e1.counitIso.hom e2.counitIso.hom, NatTrans.prod e1.counitIso.inv e2.counitIso.inv, _, _⟩
  functor_unitIso_comp := by rintro ⟨X, Y⟩; simp