module Lib.Indexing where

open import Lib.Sigma

[_] : { I : Set } → (I → Set) → Set
[_] { I } X = { i : I } → X i

_→i_ : { I : Set } → (X Y : I → Set) → I → Set
(X →i Y) i = X i → Y i

<_> : forall {I : Set} → (I → Set) → Set
<_> { I } X = Σ I \ i → X i

_×i_ : forall {I : Set} → (X Y : I → Set) → I → Set
(X ×i Y) i = X i × Y i