```
module Types.product where
open import Lang.dataStructures using (
Bool; true; false;
⊥; ⊤; singleton; ℕ; List;
one; two; three; four; five; six; seven; eight; nine; ten; zero; succ;
_::_; [])
open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
```

A cartesian product of two types `A`

and `B`

can be defined as a pair of objects `(a, b)`

, where `a`

∈ `A`

, and `b`

∈ `B`

.

and cartesian products constructed as

While being intuitively familiar with what a cartesian product is, it’s algebraic definition captures the most abstract aspect of a product:

A cartesian product, in set theory, for two sets `A`

and `B`

is defined as:

`A x B = { (a , b) | a ∈ A and b ∈ B }`

In type theory, we look at another way of defining product types, just by looking at them as objects in themselves: For an object `X`

, we call `X`

a product type if:

- There exists two functions, lets call them
`proj₁`

and`proj₂`

such that they can be used to “extract” the contents of the product`X`

:

- If there is any another object
`A`

, such that the functions`proj₁ₐ`

and`proj₂ₐ`

satisfied the above condition for`A`

, then there exists a function,`fₐ₀`

such that:

Note: The above is pseudo-code, the proof is below.

The second condition is the unique-ness condition, .i.e. for all objects having projections to `A`

and `B`

, there is one through which all projections go through. We call this one object the “Product” This is better visualized in this diagram:

Dependent types are products where the 2nd type is dependent on the first one. They are of the form `(x : A, B(x))`

. The notation in type theory looks like this for binary dependent pairs:

\[ \sum_{x : A} B(x) \]

with ternary dependent pair types being represented as:

\[ \sum_{x : A} \sum_{y : B(x)} C(y) \]

and so on.

Agda’s `record`

types provides encapsulation for this definition and some syntactic sugars like constructors:

```
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
constructor _,_
field
fst : A
snd : B fst
open Σ public
infixr 4 _,_
```

While constructing complex mathematical structures, a fairly general pattern is that a bunch of properties can be bundled together to form objects, and then structures are built on top of them. Since all of those properties are types, a record containing a bunch of properties would by construction ensure the objects of such a record belong to the type represented. A lot of implementation of mathematical structures can be done in this form of `record`

s of bundled properties.

Hence if, say `Prop₁`

and `Prop₂`

are two properties, an object that satisfies both is a record with both properties as fields:

```
data prop1 : Set where
data prop2 : Set where
record Satisfies (x : prop1)(y : prop2) : Set where
field
p1 : prop1
p2 : prop2
```

The `record`

type is a special syntax for representing dependent or Σ (sigma) types in Agda, though they can very well also be represented in other ways such as using the `data`

keyword.

```
<_,_> : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ {x} → B x → Set c}
(f : (x : A) → B x)
→ ((x : A) → C (f x))
→ ((x : A) → Σ (B x) C)
< f , g > x = (f x , g x)
```

Mapping a pair of functions `f`

and `g`

over a product:

```
map : ∀ {a b p q} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q}
→ (f : A → B)
→ (∀ {x} → P x → Q (f x))
→ Σ A P
→ Σ B Q
map f g (x , y) = (f x , g y)
```

Co-products, also called as “sum” types can be thought of as a disjoint uinon of two objects.

Mathematically, an object `X ⋃ Y`

is a co-product of objects `X`

and `Y`

if,

- There exists two functions
`inj_₁`

and`inj₂`

such that:

- If there is any another object
`A`

, such that the functions`inj₁ₐ`

and`inj₂ₐ`

satisfied the above condition, then there exists a function,`fₐ₀`

such that:

```
data _∪_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
inj₁ : (x : A) → A ∪ B
inj₂ : (y : B) → A ∪ B
```

Co-product types are similar to product types, except with reversed arrows:

Just like the cartesian product is the representative type of a product, the `Maybe`

type fills that role for the co-product. This happens to be a very popular datatype in functional programming languages like haskell `Maybe`

, scala `Option`

etc and is widely used to error handling.

```
maybe : ∀ {a b} {A : Set a} {B : Maybe A → Set b}
→ ((x : A) → B (just x))
→ B nothing
→ (x : Maybe A)
→ B x
maybe j n (just x) = j x
maybe j n nothing = n
```

A `Maybe`

is also a structure which can be map-ed over:

```
smap : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Maybe A → Maybe B
smap f (just x) = just (f x)
smap f nothing = nothing
```

```
zip : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ Maybe A
→ Maybe B
→ Maybe (A × B)
zip (just a) (just b) = just (a , b)
zip _ _ = nothing
```