Iterated categorical (bi/co/)products?

Stream: Is there code for X?

[Scott Morrison]

Do we already have this somewhere:

/-- An iterated product is a product over a sigma type. -/
@[simps]
def piPiIso {f : ι → Type _} {g : (i : ι) → (f i) → C}
    [∀ i, HasProduct (g i)] [HasProduct fun i => ∏ g i]
    [HasProduct fun p : Σ i, f i => g p.1 p.2] :
    (∏ fun i => ∏ g i) ≅ (∏ fun p : Σ i, f i => g p.1 p.2) where
  hom := Pi.lift fun ⟨i, x⟩ => Pi.π _ i ≫ Pi.π _ x
  inv := Pi.lift fun i => Pi.lift fun x => Pi.π _ (⟨i, x⟩ : Σ i, f i)

[Markus Himmel]

I don't think so