Indexed product

open import category-theory.category
module category-theory.indexed-product
  {o h} (𝒞 : Category o h) where

open import foundations.universe
open import foundations.identity-type
open Category 𝒞

private variable
  ℓ : Level
  I : Type ℓ

  Y W : Ob
  Z : I → Ob

  α : (i : I) → Hom Y (Z i)
  f : Hom Y W

record isIndexedProduct {ℓ} (I : Type ℓ) (A : I → Ob) X (π : (i : I) → Hom X (A i)) : Type (o ⊔ h ⊔ ℓ) where
  field
    ⟨_⟩ : ((i : I) → Hom Y (A i)) → Hom Y X
    β : ∀ (i : I) → π i ∘ ⟨ α ⟩ ＝ α i
    η : ⟨ (λ i → π i ∘ f) ⟩ ＝ f

record IndexedProduct {ℓ} (I : Type ℓ) (A : I → Ob) : Type (o ⊔ h ⊔ ℓ) where
  field
    X : Ob
    π : (i : I) → Hom X (A i)
    is-indexed-product : isIndexedProduct I A X π

  open isIndexedProduct is-indexed-product public