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

module Terra.Data.Sigma where
open import Terra.Data.Level
open import Agda.Builtin.Sigma public

-- private
--   variable
--     ℓ : Level

-- record Σ {ℓ} {ℓ′} (I : Set ℓ) (P : I -> Set ℓ′) : Set (ℓ ⊔ ℓ′) where
--   constructor _,_
--   field
--     fst : I
--     snd : P fst

-- infixr 5 _,_

-- open Σ public

-- {-# BUILTIN SIGMA Σ #-}

-- syntax Σ I (λ i -> P) = Σ[ i ∈ I ] P