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

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

module Data.Product.Base where

open import Function.Base
open import Level using (Level; _⊔_)

private
  variable
    a b c d e f  p q r : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d
    E : Set e
    F : Set f

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

open import Agda.Builtin.Sigma public
  renaming (fst to proj₁; snd to proj₂)
  hiding (module Σ)

module Σ = Agda.Builtin.Sigma.Σ
  renaming (fst to proj₁; snd to proj₂)

------------------------------------------------------------------------
-- Existential quantifiers

 :  {A : Set a}  (A  Set b)  Set (a  b)
 = Σ _

∃₂ :  {A : Set a} {B : A  Set b}
     (C : (x : A)  B x  Set c)  Set (a  b  c)
∃₂ C =  λ a   λ b  C a b

------------------------------------------------------------------------
-- Syntaxes

-- The syntax declaration below is attached to Σ-syntax, to make it
-- easy to import Σ without the special syntax.

infix 2 Σ-syntax

Σ-syntax : (A : Set a)  (A  Set b)  Set (a  b)
Σ-syntax = Σ

syntax Σ-syntax A  x  B) = Σ[ x  A ] B

infix 2 ∃-syntax

∃-syntax :  {A : Set a}  (A  Set b)  Set (a  b)
∃-syntax = 

syntax ∃-syntax  x  B) = ∃[ x ] B

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

infixr 4 _,′_
infixr 2 _×_

_×_ :  (A : Set a) (B : Set b)  Set (a  b)
A × B = Σ[ x  A ] B

_,′_ : A  B  A × B
_,′_ = _,_

------------------------------------------------------------------------
-- Operations over dependent products

infix  4 -,_
infixr 2 _-×-_ _-,-_
infixl 2 _<*>_

-- Sometimes the first component can be inferred.

-,_ :  {A : Set a} {B : A  Set b} {x}  B x  Σ _ B
-, y = _ , y

<_,_> :  {A : Set a} {B : A  Set b} {C :  {x}  B x  Set c}
        (f : (x : A)  B x)  ((x : A)  C (f x)) 
        ((x : A)  Σ (B x) C)
< f , g > x = (f x , g x)

map :  {P : A  Set p} {Q : B  Set q} 
      (f : A  B)  (∀ {x}  P x  Q (f x)) 
      Σ A P  Σ B Q
map f g (x , y) = (f x , g y)

map₁ : (A  B)  A × C  B × C
map₁ f = map f id

map₂ :  {A : Set a} {B : A  Set b} {C : A  Set c} 
       (∀ {x}  B x  C x)  Σ A B  Σ A C
map₂ f = map id f

-- A version of map where the output can depend on the input
dmap :  {B : A  Set b} {P : A  Set p} {Q :  {a}  P a  B a  Set q} 
       (f : (a : A)  B a)  (∀ {a} (b : P a)  Q b (f a)) 
       ((a , b) : Σ A P)  Σ (B a) (Q b)
dmap f g (x , y) = f x , g y

zip :  {P : A  Set p} {Q : B  Set q} {R : C  Set r} 
      (_∙_ : A  B  C) 
      (∀ {x y}  P x  Q y  R (x  y)) 
      Σ A P  Σ B Q  Σ C R
zip _∙_ _∘_ (a , p) (b , q) = ((a  b) , (p  q))

curry :  {A : Set a} {B : A  Set b} {C : Σ A B  Set c} 
        ((p : Σ A B)  C p) 
        ((x : A)  (y : B x)  C (x , y))
curry f x y = f (x , y)

uncurry :  {A : Set a} {B : A  Set b} {C : Σ A B  Set c} 
          ((x : A)  (y : B x)  C (x , y)) 
          ((p : Σ A B)  C p)
uncurry f (x , y) = f x y

-- Rewriting dependent products
assocʳ : {B : A  Set b} {C : (a : A)  B a  Set c} 
          Σ (Σ A B) (uncurry C)  Σ A  a  Σ (B a) (C a))
assocʳ ((a , b) , c) = (a , (b , c))

assocˡ : {B : A  Set b} {C : (a : A)  B a  Set c} 
          Σ A  a  Σ (B a) (C a))  Σ (Σ A B) (uncurry C)
assocˡ (a , (b , c)) = ((a , b) , c)

-- Alternate form of associativity for dependent products
-- where the C parameter is uncurried.
assocʳ-curried : {B : A  Set b} {C : Σ A B  Set c} 
                 Σ (Σ A B) C  Σ A  a  Σ (B a) (curry C a))
assocʳ-curried ((a , b) , c) = (a , (b , c))

assocˡ-curried : {B : A  Set b} {C : Σ A B  Set c} 
          Σ A  a  Σ (B a) (curry C a))  Σ (Σ A B) C
assocˡ-curried (a , (b , c)) = ((a , b) , c)

------------------------------------------------------------------------
-- Operations for non-dependent products

-- Any of the above operations for dependent products will also work for
-- non-dependent products but sometimes Agda has difficulty inferring
-- the non-dependency. Primed (′ = \prime) versions of the operations
-- are therefore provided below that sometimes have better inference
-- properties.

zip′ : (A  B  C)  (D  E  F)  A × D  B × E  C × F
zip′ f g = zip f g

curry′ : (A × B  C)  (A  B  C)
curry′ = curry

uncurry′ : (A  B  C)  (A × B  C)
uncurry′ = uncurry

map₂′ : (B  C)  A × B  A × C
map₂′ f = map₂ f

dmap′ :  {x y} {X : A  Set x} {Y : B  Set y} 
        ((a : A)  X a)  ((b : B)  Y b) 
        ((a , b) : A × B)  X a × Y b
dmap′ f g = dmap f g

_<*>_ :  {x y} {X : A  Set x} {Y : B  Set y} 
        ((a : A)  X a) × ((b : B)  Y b) 
        ((a , b) : A × B)  X a × Y b
_<*>_ = uncurry dmap′

-- Operations that can only be defined for non-dependent products

swap : A × B  B × A
swap (x , y) = (y , x)

_-×-_ : (A  B  Set p)  (A  B  Set q)  (A  B  Set _)
f -×- g = f -⟪ _×_ ⟫- g

_-,-_ : (A  B  C)  (A  B  D)  (A  B  C × D)
f -,- g = f -⟪ _,_ ⟫- g

-- Rewriting non-dependent products
assocʳ′ : (A × B) × C  A × (B × C)
assocʳ′ ((a , b) , c) = (a , (b , c))

assocˡ′ : A × (B × C)  (A × B) × C
assocˡ′ (a , (b , c)) = ((a , b) , c)