Product and Sum types

This chapter explores product and sum types, two foundational constructs in type theory.

We begin with the product type, which models the combination of two types into a single type whose elements are pairs. The section introduces the construction of product types, how to access their components, and their role in structuring data. The universal property of the product is then presented, characterizing the product as the type that uniquely supports projections and pairing. The concept is extended to the product of a family of types, generalizing the binary product to arbitrary indexed collections.

Next, we examine the sum type, which represents a value that belongs to one of several types. It captures alternatives or choices between types and is central to defining tagged unions. The universal property of the sum provides its defining characteristic: a type that uniquely supports case analysis using injections. This is generalized to the sum of a family of types, where each summand is indexed, enabling more expressive and flexible type constructions.

The chapter concludes with a set of exercises aimed at reinforcing understanding through practical applications and formal reasoning about product and sum types.

Product type

A product type combines two types into a single type whose values consist of pairs drawn from each component. In Lean, the product type of A and B is written as Prod A B or, alternatively as, A × B, using the × symbol (typed as \times).

If we #print Prod, Lean returns:

structure Prod.{u, v} : Type u → Type v → Type (max u v)
number of parameters: 2
constructor:
Prod.mk : {α : Type u} → {β : Type v} → α → β → α × β
fields:
fst : α
snd : β

Lean defines the product type internally using the Prod structure. This definition shows that Prod takes two types—one from universe u and one from universe v—and returns a type in the larger of the two universes, max u v. The constructor Prod.mk builds a pair from values of types α and β, and the resulting pair belongs to the product type α × β. The structure has two fields: fst, which retrieves the first component of the pair, and snd, which retrieves the second component.

This definition implies that to construct a value of type A × B, we must provide both a value of type A and a value of type B. The constructor Prod.mk enforces this requirement: given a : A and b : B, the expression Prod.mk a b (or simply ⟨a, b⟩ using Lean’s pair notation) yields a value of type A × B. This reflects the nature of product types as containers of exactly one value from each of their component types. In other words, a product type does not represent a choice between A and B, but rather a combination of the two.

toPair

def toPair {A B : Type} : A → B → A × B := by
  intro a b
  exact Prod.mk a b -- alternatively ⟨a, b⟩

The Prod type provides two projections, π1 and π1, or, alternatively, fst and snd, which allow us to extract the individual components of a product. Given a value p : A × B, the expression p.fst retrieves the first element (of type A), and p.snd retrieves the second element (of type B).

projections

-- projection on the first component
def π1 {A B : Type} : (A × B) → A := by
  intro p
  exact p.fst
-- projection on the second component
def π2 {A B : Type} : (A × B) → B := by
  intro p
  exact p.snd

Two values of type A × B are equal if, and only if, their respective components are equal. That is, given p1 p2 : A × B, we have p1 = p2 precisely when p1.fst = p2.fst and p1.snd = p2.snd. Lean provides the theorem Prod.ext to formalize and prove such equalities.

prodEq

theorem prodEq {A B : Type} (p1 p2 : A × B) : (p1 = p2) ↔ (π1 p1 = π1 p2) ∧ (π2 p1 = π2 p2) := by
  apply Iff.intro
  -- p1 = p2 → π1 p1 = π1 p2 ∧ π2 p1 = π2 p2
  intro h
  apply And.intro
  exact congrArg π1 h
  exact congrArg π2 h
  -- π1 p1 = π1 p2 ∧ π2 p1 = π2 p2 → p1 = p2
  intro ⟨h1, h2⟩
  apply Prod.ext
  exact h1
  exact h2

Universal property of the product

The universal property of the product type characterizes it as the best type that supports pairing of data. Specifically, given types A, B, and C, and functions f : C → A and g : C → B, there exists a unique function h : C → A × B such that the projections of h recover f and g; that is, π₁ ∘ h = f and π₂ ∘ h = g. In Lean, this function h is constructed by sending each c : C to the pair (f c, g c).

toProd

def toProd {A B C : Type} (f : C → A) (g : C → B) : (C → A × B) := by
  intro c
  exact Prod.mk (f c) (g c)

This function has the key property that composing it with the product projections recovers the original functions.

toProd

-- Composition with π1
theorem toProdp1 {A B C : Type} (f : C → A) (g : C → B) : π1 ∘ (toProd f g) = f := by
  funext c
  exact rfl
-- Composition with π2
theorem toProdp2 {A B C : Type} (f : C → A) (g : C → B) : π2 ∘ (toProd f g) = g := by
  funext c
  exact rfl

The universal property of the product type not only guarantees the existence of the function toProd f g : C → A × B satisfying the projection identities, but also ensures its uniqueness. That is, if we have a function h : C → A × B such that π₁ ∘ h = f and π₂ ∘ h = g, then h must be equal to toProd f g. This uniqueness clause completes the universal property: it tells us that toProd f g is the only function from C to A × B whose projections are f and g. This powerful principle often allows us to characterize and prove properties about functions into product types by reasoning solely about their projections.

toProd

theorem toProdUnique {A B C : Type} {f : C → A} {g : C → B} {h : C → A × B} : 
(π1 ∘ h = f) → (π2 ∘ h = g) → (h = toProd f g) := by
  intro h1 h2
  funext c
  apply Prod.ext
  exact congrFun h1 c
  exact congrFun h2 c

Generalized product type

Given an index type I and a family of types 𝔸 : I → Type, the product type consists of a collection of values, each corresponding to a type in the family 𝔸 i for every index i : I. In Lean, this is expressed as the dependent function type ∀ (i : I), 𝔸 i, which can be thought of as the type of functions that assign a value of type 𝔸 i to each index i : I.

GeneralizedProduct

variable (I : Type)
variable (𝔸 : I → Type)
#check ∀ (i : I), 𝔸 i

To produce a value of type ∀ (i : I), 𝔸 i, we must provide a value of type 𝔸 i for each i : I.

GeneralizedtoPair

def toPairg {I : Type} {𝔸 : I → Type} : ((i : I) → 𝔸 i) → ∀ (i : I), 𝔸 i := by
  intro 𝕗 i
  exact 𝕗 i

The type ∀ (i : I), 𝔸 i has a natural projection that allows us to extract the value of type 𝔸 i for a specific index i : I. This projection is a function that, given an element of type ∀ (i : I), 𝔸 i, returns the corresponding value of type 𝔸 i for a particular index i.

GeneralizedProjection

def π {I : Type} {𝔸 : I → Type} (i : I) : (∀ (i : I), 𝔸 i) → 𝔸 i := by
  intro 𝕒
  exact 𝕒 i

Two values of type ∀ (i : I), 𝔸 i are equal if and only if their corresponding i-th components are equal for every index i : I.

GeneralizedProdEq

theorem prodEqg {I : Type} {𝔸 : I → Type} (𝕒1 𝕒2 : ∀ (i : I), 𝔸 i) : 
(𝕒1 = 𝕒2) ↔ ∀ (i : I), π i 𝕒1 = π i 𝕒2 := by
  apply Iff.intro
  -- 𝕒1 = 𝕒2 → ∀ (i : I), π i 𝕒1 = π i 𝕒2
  intro h i
  exact congrArg (π i) h
  -- (∀ (i : I), π i 𝕒1 = π i 𝕒2) → 𝕒1 = 𝕒2
  intro h
  funext i
  exact h i

Universal property of the generalized product

The universal property of the product type ∀ (i : I), 𝔸 i is a key characteristic that allows us to construct a function from a given family of functions. Specifically, if we have a family of functions 𝕗 i : C → 𝔸 i for each i : I, the universal property guarantees the existence of a unique function h : C → ∀ (i : I), 𝔸 i such that for every i : I, π i ∘ h = 𝕗 i.

GeneralizedtoProd

def toProdg {I C : Type} {𝔸 : I → Type} (𝕗 : (i : I) → C → 𝔸 i) : 
C → (∀ (i : I), 𝔸 i) := by
  intro c i
  exact (𝕗 i) c

Applying the projection π i to the result of toProdg𝕗 yields the corresponding function 𝕗 i.

GeneralizedtoProd

theorem toProdpg {I C : Type} {𝔸 : I → Type} (𝕗 : (i : I) → C → 𝔸 i) (i : I) : 
(π i) ∘ (toProdg 𝕗) = 𝕗 i := by
  funext c
  exact rfl

The universal property of the product type also asserts a uniqueness condition: if we have a function h : C → ∀ (i : I), 𝔸 i such that, for every i : I, the composition of h with the projection π i satisfies the equality π i ∘ h = 𝕗 i, then the function h must be equal to the function constructed by toProdg𝕗.

GeneralizedtoProd

theorem toProdgUnique {I C : Type} {𝔸 : I → Type} {𝕗 : (i : I) → C → 𝔸 i} 
{h : C → ∀ (i : I), 𝔸 i} : (∀ (i : I), (π i) ∘ h = (𝕗 i)) → (h = toProdg 𝕗) := by
  intro hp
  funext c
  funext i
  exact congrFun (hp i) c

Sum type

A sum type combines two types into a single type whose values are drawn from some component. In Lean, the sum type of A and B is written as Sum A B or, alternatively as, A ⊕ B, using the ⊕ symbol (typed as \oplus).

If we #print Sum, Lean returns:

inductive Sum.{u, v} : Type u → Type v → Type (max u v)
number of parameters: 2
constructors:
Sum.inl : {α : Type u} → {β : Type v} → α → α ⊕ β
Sum.inr : {α : Type u} → {β : Type v} → β → α ⊕ β

Lean defines the sum type internally using the inductive Sum type. This definition shows that Sum takes two types—one from universe u and one from universe v—and returns a type in the larger of the two universes, max u v. It includes two constructors: Sum.inl, which wraps a value of type α, and Sum.inr, which wraps a value of type β. The type Sum ensures that values can be of one type or the other.

The Sum type provides two injections, ι1 and ι2 or, alternatively, Sum.inl and Sum.inr, which allows us to insert the individual components on a sum. Given a value a : A, the expression Sum.inl a retrieves an element of type A ⊕ B. Given a value b : B, the expression Sum.inr b retrieves an element of type A ⊕ B.

injections

-- injection on the first component
def ι1 {A B : Type} : A → A ⊕ B := by
  intro a
  exact Sum.inl a
-- injection on the second component
def ι2 {A B : Type} : B → A ⊕ B := by
  intro b
  exact Sum.inr b

Two values of type A ⊕ B are considered equal if and only if they are both injections on the same element. This means that if we have two elements p1, p2 : A ⊕ B, we say p1 = p2 if, for both elements, either both are wrapped using the Sum.inl constructor (i.e., both come from type A), or both are wrapped using the Sum.inr constructor (i.e., both come from type B), and, in each case, the underlying values are equal.

sumEq

theorem sumEq {A B : Type} (p1 p2 : A ⊕ B) : (p1 = p2) ↔ 
(∃ (a : A), (((ι1 a) = p1) ∧ ((ι1 a) = p2))) ∨
(∃ (b : B), (((ι2 b) = p1) ∧ ((ι2 b) = p2))) := by
  apply Iff.intro
  -- p1 = p2 → (∃ a, ι1 a = p1 ∧ ι1 a = p2) ∨ ∃ b, ι2 b = p1 ∧ ι2 b = p2
  intro h
  cases p1 with
  | inl a => cases p2 with
    | inl b =>
      injection h with h1
      apply Or.inl
      apply Exists.intro a
      apply And.intro rfl
      rw [h1]
      exact rfl
    | inr b =>
      exact Sum.noConfusion h
  | inr a => cases p2 with
    | inl b =>
      exact Sum.noConfusion h
    | inr b =>
      injection h with h1
      apply Or.inr
      apply Exists.intro a
      apply And.intro rfl
      rw [h1]
      exact rfl
  -- ((∃ a, ι1 a = p1 ∧ ι1 a = p2) ∨ ∃ b, ι2 b = p1 ∧ ι2 b = p2) → p1 = p2
  intro h
  cases h with
  | inl h =>
    apply Exists.elim h
    intro a ⟨h1, h2⟩
    exact h1.symm.trans h2
  | inr h =>
    apply Exists.elim h
    intro b ⟨h1, h2⟩
    exact h1.symm.trans h2

Universal property of the sum

The universal property of the sum type characterizes it as the best type that supports pairing of data. Specifically, given types A, B, and C, and functions f : A → C and g : B → C, there exists a unique function h : A ⊕ B → C such that h , when composed with the injections, recover f and g; that is, h ∘ ι1 = f and h ∘ ι2 = g. In Lean, this function h is constructed by sending o : A ⊕ B to f o or to g o depending on its nature.

fromSum

def fromSum {A B C : Type} (f : A → C) (g : B → C) : (A ⊕ B) → C := by
  intro o
  cases o with
  | inl a => exact f a
  | inr b => exact g b

This function has the key property that composing it with the sum injections recovers the original functions.

fromSum

-- Composition with ι1
theorem fromSumi1 {A B C : Type} (f : A → C) (g : B → C) : (fromSum f g) ∘ ι1 = f := by
  funext a
  exact rfl
-- Composition with ι2
theorem fromSumi2 {A B C : Type} (f : A → C) (g : B → C) : (fromSum f g) ∘ ι2 = g := by
  funext b
  exact rfl

The universal property of the sum type not only guarantees the existence of the function fromSum f g : A ⊕ B → C satisfying the injection identities, but also ensures its uniqueness. That is, if we have a function h : A ⊕ B → C such that h ∘ ι1 = f and h ∘ ι2 = g, then h must be equal to fromSum f g. This uniqueness clause completes the universal property: it tells us that fromSum f g is the only function from A ⊕ B to C whose injections are f and g. This powerful principle often allows us to characterize and prove properties about functions from sum types by reasoning solely about their injections.

fromSum

theorem fromSumUnique {A B C : Type} {f : A → C} {g : B → C} {h : (A ⊕ B) → C} :
(h ∘ ι1 = f) → (h ∘ ι2 = g) → (h = fromSum f g) := by
  intro h1 h2
  funext o
  cases o with
  | inl a => exact congrFun h1 a
  | inr b => exact congrFun h2 b

Generalized sum type

Given an index type I and a family of types 𝔸 : I → Type, the sum type consists of a collection of values, corresponding to some type in the family 𝔸 i for some index i : I. In Lean, this is expressed as the type Sigma 𝔸 or, alternatively, (Σ (i : I), 𝔸 i), which can be thought of as the type of functions that assign a value of type 𝔸 i to some index i : I.

GeneralizedSum

variable (I : Type)
variable (𝔸 : I → Type)
#check (Σ (i : I), 𝔸 i)

The type (Σ (i : I), 𝔸 i) has a natural injection that allows us to insert the value of type 𝔸 i for an specific index i : I. This injection is a function that, given an index i : I and an element of type 𝔸 i, returns an element of type (Σ (i : I), 𝔸 i).

GeneralizedInjection

def ι {I : Type} {𝔸 : I → Type} (i : I) : 𝔸 i → (Σ (i : I), 𝔸 i) := by
  intro a
  exact ⟨i, a⟩

Two values of type (Σ (i : I), 𝔸 i) are equal if and only if they are injected from the same index i : I on the same element. For this we will use Sigma.ext keyword.

GeneralizedSumEq

theorem sumEqg {I : Type} {𝔸 : I → Type} (𝕒1 𝕒2 : (Σ (i : I), 𝔸 i)) : (𝕒1 = 𝕒2) ↔ ∃ (i : I), ∃ (a : 𝔸 i), (𝕒1 = ι i a) ∧ (𝕒2 = ι i a) := by
  apply Iff.intro
  -- 𝕒1 = 𝕒2 → ∃ i a, 𝕒1 = ι i a ∧ 𝕒2 = ι i a
  intro h
  cases 𝕒1 with
  | mk i a => cases 𝕒2 with
    | mk j b =>
      injection h with h1 h2
      apply Exists.intro i
      apply Exists.intro a
      apply And.intro rfl
      exact Sigma.ext h1.symm h2.symm
  -- ∃ i a, 𝕒1 = ι i a ∧ 𝕒2 = ι i a → 𝕒1 = 𝕒2
  intro ⟨i, ⟨a, ⟨h1, h2⟩⟩⟩
  exact  h1.trans h2.symm

Universal property of the generalized sum

The universal property of the sum type (Σ (i : I), 𝔸 i) is a key characteristic that allows us to construct a function from a given family of functions. Specifically, if we have a family of functions 𝕗 i :𝔸 i → C for each i : I, the universal property guarantees the existence of a unique function h : (Σ (i : I), 𝔸 i) → C such that for every i : I, h ∘ (ι i) = 𝕗 i.

GeneralizedfromSum

def fromSumg {I C : Type} {𝔸 : I → Type} (𝕗 : (i : I) → 𝔸 i → C) : 
(Σ (i : I), 𝔸 i) → C := by
  intro ⟨i, a⟩
  exact 𝕗 i a

Applying the injection ι iand then fromSum 𝕗 yields the corresponding function 𝕗 i.

GeneralizedtoProd

theorem fromSumig {I C : Type} {𝔸 : I → Type} (𝕗 : (i : I) → 𝔸 i → C) (i : I) : 
(fromSumg 𝕗) ∘ (ι i) = 𝕗 i := by
  funext c
  exact rfl

The universal property of the sum type also asserts a uniqueness condition: if we have a function h : (Σ (i : I), 𝔸 i) → C such that, for every i : I, the composition of h with the injection ι i satisfies the equality h ∘ (ι i) = 𝕗 i, then the function h must be equal to the function constructed by fromSumg𝕗.

GeneralizedtoProd

theorem fromSumgUnique {I C : Type} {𝔸 : I → Type} {𝕗 : (i : I) → 𝔸 i → C} 
{h : (Σ (i : I), 𝔸 i) → C} : (∀ (i : I), h ∘ (ι i) = (𝕗 i)) → (h = fromSumg 𝕗) := by
  intro hs
  funext ⟨i, a⟩
  exact congrFun (hs i) a

Exercises

Product

Exercises.lean

-- The product is commutative
theorem prodComm {A B : Type} : (A × B) ≅ (B × A) := by sorry

-- The product is associative
theorem prodAssoc {A B C : Type} : ((A × B) × C) ≅ (A × (B × C)) := by sorry

-- Empty is a left zero
theorem TEmptyProdL {A : Type} : (Empty × A) ≅ Empty := by sorry

-- Empty is a right zero
theorem TEmptyProdR {A : Type} : (A × Empty) ≅ Empty := by sorry

-- Unit is a right unit
theorem TUnitProdR {A : Type} : (A × Unit) ≅ A := by sorry

-- Unit is a left unit
theorem TUnitProdL {A : Type} : (Unit × A) ≅ A := by sorry

Sum

Exercises.lean

-- The sum is commutative
theorem sumComm {A B : Type} : (A ⊕ B) ≅ (B ⊕ A) := by sorry

-- The sum is associative
theorem sumAssoc {A B C : Type} : ((A ⊕ B) ⊕ C) ≅ (A ⊕ (B ⊕ C)) := by sorry

-- Empty is a left unit
theorem TEmptySumL {A : Type} : (Empty ⊕ A) ≅ A := by sorry

-- Empty is a right unit
theorem TEmptySumR {A : Type} : (A ⊕ Empty) ≅ A := by sorry

-- Product distributes over sum on the right
theorem TProdSumDistR {A B C : Type} : (A × (B ⊕ C)) ≅ ((A × B) ⊕ (A × C)) := by sorry

-- Product distributes over sum on the left
theorem TProdSumDistL {A B C : Type} : ((A ⊕ B) × C) ≅ ((A × C) ⊕ (B × C)) := by sorry