agda-categories

agda-categories copied to clipboard

It's defined as:

record IndexedProduct {i} (I : Set i) : Set (i ⊔ o ⊔ e ⊔ ℓ) where
  field
    P         : I → Obj
    productOf : IndexedProductOf P

  open IndexedProductOf productOf public

AllProducts : ∀ i → Set (o ⊔ ℓ ⊔ e ⊔ suc i)
AllProducts i = (I : Set i) → IndexedProduct I

This is saying that for any index set, there is a product for that indexed set. It says nothing about what objects it could contain. There's nothing stopping it from just having the product over many copies of the same object. In fact, I think that's the only thing that it can have.

could you give a more concrete example?

P gives the component object for each I. so yeah, indeed the objects are meant to be anything.

Indeed, could you be more precise @Taneb ? IndexedProduct is used successfully in proving things around completeness of categories. Yes, it's a very strong assumption, but assuming "all" products is indeed extremely strong. I'm thinking of closing this issue.

This isn't a strong assumption at all as defined, is my point. We can construct an AllProducts for any category with a terminal object, as follows:

open import Categories.Category
open import Categories.Object.Product.Indexed
open import Categories.Object.Terminal

allProducts : ∀ {o ℓ e} {C : Category o ℓ e} i → Terminal C → AllProducts C i
allProducts {C = C} _ terminal I = record
  { P = λ _ → ⊤
  ; productOf = record
    { X = ⊤
    ; π = λ _ → id
    ; ⟨_⟩ = λ _ → !
    ; commute = λ f i → Equiv.trans identityˡ (!-unique (f i))
    ; unique = λ h _ _ → !-unique h
    }
  }
  where
    open Category C
    open Terminal terminal

Looking where this module is used, we don't use AllProducts but instead AllProductsOf, which doesn't have the problem I was trying to explain.