Product Type Has one constructor (formation) and multiple ways of deconstructing (elimination) (projections).

Notation
In type theory the product of A and B is denoted A×B. In logic the product is 'and' often denoted /\ .
An element of A×B is denoted (a,b) where 'a' is an element of 'A' and 'b' is an element of 'B'.
Rules
Types are defined by their formation, term introduction, term eliminator and computation rules:
Introduction  Elimination  



This is discussed on the propositional logic page here.
In type theory types are defined in terms of:
This picture shows how programming language constructs (In this case: Idris) relate to this theory: 
βreduction and ηreduction
βreduction
construction followed by deconstruction:
 a = fst(a,b)
 b = snd(a,b)
ηreduction
deconstruction followed by construction:
 P = (fst P,snd P)
Implementations in Idris
Product terms can be defined using 'data' but there is also a specific mechanism for products using 'record'.
Here we start with a product type 'M'. We can deconstruct it by using 'fst' and 'snd' then construct it to get back to 'M'  Idris> :let M = MkPair 2 "2" Idris> MkPair (fst M) (snd M) (2, "2") : (Integer, String) 
Here we start with two terms 'x' and 'y' if we first construct using MkPair then deconstruct we get back to 'x' and 'y'.  Idris> :let x = 3 Idris> :let y = "3" Idris> fst (MkPair x y) 3 : Integer Idris> snd (MkPair x y) "3" : String 
Other implementations of product
Idris 
We can have a type which corresponds to conjunction:


from : Idrisdev/libs/prelude/Builtins.idr 
 The nondependent pair type, also known as conjunction.  @A the type of the left elements in the pair  @B the type of the right elements in the pair data Pair : (A : Type) > (B : Type) > Type where  A pair of elements  @a the left element of the pair  @b the right element of the pair MkPair : {A, B : Type} > (1 a : A) > (1 b : B) > Pair A B 

from : Idrisdev/libs/prelude/ Prelude/Basics.idr   Return the first element of a pair. fst : (a, b) > a fst (x, y) = x  Return the second element of a pair. snd : (a, b) > b snd (x, y) = y 

from : coq/theories/Init/Datatypes.v 
(** [prod A B], written [A * B], is the product of [A] and [B]; the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) #[universes(template)] Inductive prod (A B:Type) : Type := pair : A > B > A * B where "x * y" := (prod x y) : type_scope. Add Printing Let prod. Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. Arguments pair {A B} _ _. Register prod as core.prod.type. Register pair as core.prod.intro. Register prod_rect as core.prod.rect. Section projections. Context {A : Type} {B : Type}. Definition fst (p:A * B) := match p with (x, y) => x end. Definition snd (p:A * B) := match p with (x, y) => y end. Register fst as core.prod.proj1. Register snd as core.prod.proj2. End projections. 
Logic
In logic the product is 'and' denoted /\
Relationship to Category Theory
Category theory is deeply related to type theory.
On this page is product is approached from the category theory direction and on this page is generalsed to the concept of a limit.
Next Steps
Other types are discussed on the following pages: