Non-trivial examples of dependent sum ($\Sigma$-types) in Lean?

Question

I am trying to understand the concept of dependent sum types ($\Sigma$ types) using concrete examples. The example given in Theorem Proving in Lean 4 seems to be a degenerate case rendering the regular Cartesian product (if I understand it correctly):

universe u v

def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
  ⟨a, b⟩

def h1 (x : Nat) : Nat :=
  (f Type (fun α => α) Nat x).2

Searching around, I found some interesting Agda examples that the $\Sigma$ type can be used to express:

• disjoint unions
• subsets, and
• existential quantification.

I don't know Agda and cannot understand the examples there.

Can someone help explain the $\Sigma$ types in those examples in Lean 4?

Answer 1

I would like to warn you that dependent product type is usually used for the dependent function type, while the dependent version of the product type is referred to as the dependent sum type. Personally, I would try my best to avoid confusions, so I use the names "Pi types" and "Sigma types".

I wrote this answer to learn some Lean4, as I've never used Lean4 before. I appreciate nitpicks on my code.

Disjoint union

This is a disjoint union of the type A and B, represented using a Sigma type:

def DisjointUnion (A B : Type) : Bool → Type
| true => A
| false => B

def disjoint_union (A B : Type) :=
  (b : Bool) × DisjointUnion A B b

To pattern match on a disjoint union defined above, we use Bool as the "type tag" of usual disjoint unions:

def use_disjoint_union : (disjoint_union Bool Nat) → Nat
| ⟨true, true⟩ => 0
| ⟨true, false⟩ => 1
| ⟨false, n⟩ => n -- `n` is of type `Nat`, so this checks

Note how the second component of the sigma type vary by the first component's value.

Subsets

Here's a subset of Nat that only have numbers less than or equal to 3:

def Subset := (a : Nat) ×' (a ≤ 3)
def subset_instance : Subset := ⟨2, Nat.le_step (Nat.le_refl 2)⟩

In other words, when you construct an instance of Subset, you need to show a natural number and prove it to be less than or equal to 3. This is, in my understanding, similar to defining a subset using an injective map.

This is also an existential quantification: that there exists natural numbers less than or equal to 3. You may replace the right hand side of × with any proposition about a to make your own favorite existential quantification.

Here's a minor addition: if you want to understand the sigma types in the Agda code, for example Σ ℕ (λ x → x < n) this expression, you split it into three parts with the Σ symbol ignored: ℕ, λ x →, and x < n; and then you reform it as (x : ℕ) × (x < n).

Answer 2

Here an example from group theory:

Consider a family of groups Π (i : ι), G i (which is using the Pi-type to say that for every index i of some index type ι we have a group G i, and you want to work with words built from the elements of all the groups.

A good data type to for words is of course list …, but what is the type of the elements? list (G i) would be words with elements from just G i, for some fixed i.

This is where the Sigma-type comes into play: It allows us to say “an element of G i of some i“, and we end up with list (Σ (i : ι), G i) as the type of words with elements from all the groups.

(Of course, in this example I didn’t actually use that the G i are groups, and this could be phrased as “words over an alphabet”, but maybe with groups it is a bit more intuitively useful.)