{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Sigma.Base where

open import Cubical.Core.Primitives public

-- Σ-types are defined in Core/Primitives as they are needed for Glue types.