{- 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 --cubical --no-import-sorts --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