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