{- 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
-}
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
Bedrock