module Stdlib.Data.Product.Base;

infixr 2 ×;
infixr 4 ,;
--- Inductive pair. I.e. a tuple with two components.
type × (A : Type) (B : Type) :=
  | , : A → B → A × B;

--- Converts a function of two arguments to a function with a product argument.
uncurry : {A : Type} -> {B : Type} -> {C : Type} -> (A -> B -> C) -> A × B -> C;
uncurry f (a, b) := f a b;

--- Converts a function with a product argument to a function of two arguments.
curry : {A : Type} -> {B : Type} -> {C : Type} -> (A × B -> C) -> A -> B -> C;
curry f a b := f (a, b);

--- Projects the first component of a tuple.
fst : {A : Type} → {B : Type} → A × B → A;
fst (a, _) := a;

--- Projects the second component of a tuple.
snd : {A : Type} → {B : Type} → A × B → B;
snd (_, b) := b;

--- Swaps the components of a tuple.
swap : {A : Type} → {B : Type} → A × B → B × A;
swap (a, b) := b, a;

--- Applies a function to the first component.
first : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A × B → A' × B;
first f (a, b) := f a, b;

--- Applies a function to the second component.
second : {A : Type} → {B : Type} → {B' : Type} → (B → B') → A × B → A × B';
second f (a, b) := a, f b;

--- Applies a function to both components.
both : {A : Type} → {B : Type} → (A → B) → A × A → B × B;
both f (a, b) := f a, f b;