{-# OPTIONS --cubical-compatible #-}

module Terra.Data.Sigma.Syntax where
open import Terra.Data.Sigma
open import Terra.Data.Level
open import Terra.Data.Level.Variables


Σ' : (A : Set ℓ) (I : A -> Set ℓ′) -> Set (ℓ ⊔ ℓ′)
Σ' = Σ

syntax Σ' A (λ i -> E) = Σ[ i ∈ A ] E