module Data.Product.Record where
open import Data.Function
infixr 4 _,_
infixr 2 _×_ _-×-_ _-,-_
record Σ (a : Set) (b : a → Set) : Set where
field
proj₁ : a
proj₂ : b proj₁
open Σ public
_×_ : (a b : Set) → Set
a × b = Σ a (λ _ → b)
_,_ : ∀ {a b} → (x : a) → b x → Σ a b
(x , y) = record {proj₁ = x; proj₂ = y}
<_,_> : ∀ {A} {B : A → Set} {C : ∀ {x} → B x → Set}
(f : (x : A) → B x) → ((x : A) → C (f x)) →
((x : A) → Σ (B x) C)
< f , g > x = (f x , g x)
map : ∀ {A B P Q} →
(f : A → B) → (∀ {x} → P x → Q (f x)) →
Σ A P → Σ B Q
map f g = < f ∘ proj₁ , g ∘ proj₂ >
swap : ∀ {a b} → a × b → b × a
swap = < proj₂ , proj₁ >
_-×-_ : ∀ {a b} → (a → b → Set) → (a → b → Set) → (a → b → Set)
f -×- g = f -[ _×_ ]₁- g
_-,-_ : ∀ {a b c d} → (a → b → c) → (a → b → d) → (a → b → c × d)
f -,- g = f -[ _,_ ]- g
curry : {a : Set} {b : a → Set} {c : Σ a b → Set} →
((p : Σ a b) → c p) →
((x : a) → (y : b x) → c (x , y))
curry f x y = f (x , y)
uncurry : {a : Set} {b : a → Set} {c : Σ a b → Set} →
((x : a) → (y : b x) → c (x , y)) →
((p : Σ a b) → c p)
uncurry f p = f (proj₁ p) (proj₂ p)