
  0 | module Data.Product
  1 | 
  2 | import public Data.Ops
  3 | import Data.Vect
  4 | 
  5 | %default total
  6 | %hide Prelude.(&&)
  7 | %hide Prelude.Num.(*)
  8 | 
  9 | ||| Pairs of types
 10 | public export
 11 | record (*) (a, b : Type) where
 12 |   constructor (&&)
 13 |   π1 : a
 14 |   π2 : b
 15 | 
 16 | %pair (*) π1 π2
 17 | 
 18 | public export
 19 | elim : (a -> a') -> (b -> b') -> (a' -> b' -> c) -> a * b -> c
 20 | elim f g m x = f x.π1 `m` g x.π2
 21 | 
 22 | ||| Map each element of the pair and combine the results into one using
 23 | 
 24 | ||| Products have a bifunctor insttance
 25 | public export
 26 | Bifunctor (*) where
 27 |   bimap f1 f2 = elim f1 f2 (&&)
 28 | 
 29 | 
 30 | ||| From arity 2 to arity 1 with pair
 31 | public export
 32 | curry : (a * b -> c) -> a -> b -> c
 33 | curry f a b = f (a && b)
 34 | 
 35 | ||| From arity 2 to arity 1 with pair
 36 | public export
 37 | uncurry : (a -> b -> c) -> a * b -> c
 38 | uncurry f x = f x.π1 x.π2
 39 | 
 40 | public export
 41 | projIdentity : (x : a * b) -> (x.π1 && x.π2) === x
 42 | projIdentity (a && b) = Refl
 43 |