{-# 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