type × (A : Type) (B : Type)Source#

uncurry : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → A × B → CSource#

fst : {A : Type} → {B : Type} → A × B → ASource#

snd : {A : Type} → {B : Type} → A × B → BSource#

swap : {A : Type} → {B : Type} → A × B → B × ASource#

first : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A × B → A' × BSource#

second : {A : Type} → {B : Type} → {B' : Type} → (B → B') → A × B → A × B'Source#

both : {A : Type} → {B : Type} → (A → B) → A × A → B × BSource#