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

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

module Data.Product where

open import Function.Base
open import Level
open import Relation.Nullary.Negation.Core

private
  variable
    a b c  : Level
    A B : Set a

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

open import Data.Product.Base public

------------------------------------------------------------------------
-- 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