Product mk in category of types

Stream: Is there code for X?

[Christian Merten]

Is there a product version of Types.Limit.mk, i.e.

import Mathlib

universe u v

open CategoryTheory Limits

noncomputable def Types.Pi.mk [UnivLE.{v, u}] (ι : Type v) (f : ι → Type u)
    (x : ∀ j, f j) : (∏ f : Type u) := by
  apply Types.Limit.mk (Discrete.functor f) (fun ⟨i⟩ => x i)
  intro ⟨i⟩ ⟨j⟩ u
  have h : i = j := Discrete.eq_of_hom u
  aesop_subst [h]
  simp only [Discrete.functor_obj, Discrete.functor_map_id, types_id_apply]