{-# OPTIONS --universe-polymorphism #-} module Data.Indexed where open import Data.Product _|×|_ : ∀ {i f g} {Ix : Set i} (F : Ix → Set f) (G : Ix → Set g) → (Ix → Set _) F |×| G = λ A → F A × G A _|→|_ : ∀ {i f g} {Ix : Set i} (F : Ix → Set f) (G : Ix → Set g) → (Ix → Set _) F |→| G = λ A → F A → G A