{- Basic definitions using Σ-types
Σ-types are defined in Core/Primitives as they are needed for Glue types.
The file contains:
- Non-dependent pair types: A × B
- Mere existence: ∃[x ∈ A] B
- Unique existence: ∃![x ∈ A] B
-}
{-# OPTIONS --safe #-}
module Cubical.Data.Sigma.Base where
open import Cubical.Core.Primitives public
open import Cubical.Foundations.Prelude
open import Cubical.HITs.PropositionalTruncation.Base

-- Non-dependent pair types
_×_ :  { ℓ'} (A : Type ) (B : Type ℓ')  Type (ℓ-max  ℓ')
A × B = Σ A  _  B)
infixr 5 _×_

-- Mere existence
 :  { ℓ'} (A : Type ) (B : A  Type ℓ')  Type (ℓ-max  ℓ')
 A B =  Σ A B ∥₁
infix 2 ∃-syntax
∃-syntax :  { ℓ'} (A : Type ) (B : A  Type ℓ')  Type (ℓ-max  ℓ')
∃-syntax = 
syntax ∃-syntax A  x  B) = ∃[ x  A ] B

-- Unique existence
∃! :  { ℓ'} (A : Type ) (B : A  Type ℓ')  Type (ℓ-max  ℓ')
∃! A B = isContr (Σ A B)
infix 2 ∃!-syntax
∃!-syntax :  { ℓ'} (A : Type ) (B : A  Type ℓ')  Type (ℓ-max  ℓ')
∃!-syntax = ∃!
syntax ∃!-syntax A  x  B) = ∃![ x  A ] B