    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Products
    ------------------------------------------------------------------------

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

    module Data.Product where

    open import Level using (Level; _⊔_)
    open import Relation.Nullary.Negation.Core using (¬_)

    private
      variable
        a b c ℓ p q r s : Level
        A B C : Set a

    ------------------------------------------------------------------------
    -- Definition of dependent products

    open import Data.Product.Base public

    -- These are here as they are not 'basic' but instead "very dependent",
    -- i.e. the result type depends on the full input 'point' (x , y).
    map-Σ : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} →
       (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) →
       ((x , y) : Σ A P) → Σ (B x) (Q y)
    map-Σ f g (x , y) = (f x , g y)

    -- This is a "non-dependent" version of map-Σ whereby the input is actually
    -- a pair (i.e. _×_ ) but the output type still depends on the input 'point' (x , y).
    map-Σ′ : {B : A → Set b} {P : Set p} {Q : P → Set q} →
      (f : (x : A) → B x) → ((x : P) → Q x) → ((x , y) : A × P) → B x × Q y
    map-Σ′ f g (x , y) = (f x , g y)

    -- This is a generic zipWith for Σ where different functions are applied to each
    -- component pair, and recombined.
    zipWith : {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s}
      (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) →
      (_*_ : (x : C) → (y : R x) → S x y) →
      ((a , p) : Σ A P) → ((b , q) : Σ B Q) → S (a ∙ b) (p ∘ q)
    zipWith _∙_ _∘_ _*_ (a , p) (b , q) = (a ∙ b) * (p ∘ q)

    ------------------------------------------------------------------------
    -- Negation of existential quantifier

    ∄ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
    ∄ P = ¬ ∃ P

    -- Unique existence (parametrised by an underlying equality).

    ∃! : {A : Set a} → (A → A → Set ℓ) → (A → Set b) → Set (a ⊔ b ⊔ ℓ)
    ∃! _≈_ B = ∃ λ x → B x × (∀ {y} → B y → x ≈ y)

    -- Syntax

    infix 2 ∄-syntax

    ∄-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
    ∄-syntax = ∄

    syntax ∄-syntax (λ x → B) = ∄[ x ] B