{-# OPTIONS --without-K --safe #-}
module Data.Product where
open import Function.Base
open import Level
open import Relation.Nullary
open import Agda.Builtin.Equality
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
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₂)
infix 2 Σ-syntax
Σ-syntax : (A : Set a) → (A → Set b) → Set (a ⊔ b)
Σ-syntax = Σ
syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B
infixr 4 _,′_
infixr 2 _×_
_×_ : ∀ (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ[ x ∈ A ] B
_,′_ : A → B → A × B
_,′_ = _,_
∃ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _
∄ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
∄ P = ¬ ∃ P
∃₂ : ∀ {A : Set a} {B : A → Set b}
(C : (x : A) → B x → Set c) → Set (a ⊔ b ⊔ c)
∃₂ C = ∃ λ a → ∃ λ b → C a b
∃! : {A : Set a} → (A → A → Set ℓ) → (A → Set b) → Set (a ⊔ b ⊔ ℓ)
∃! _≈_ B = ∃ λ x → B x × (∀ {y} → B y → x ≈ y)
infix 2 ∃-syntax
∃-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃-syntax = ∃
syntax ∃-syntax (λ x → B) = ∃[ x ] B
infix 2 ∄-syntax
∄-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
∄-syntax = ∄
syntax ∄-syntax (λ x → B) = ∄[ x ] B
infix 4 -,_
infixr 2 _-×-_ _-,-_
infixl 2 _<*>_
-,_ : ∀ {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
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
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)
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)
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
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′
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
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)