Pi and Sigma in Homotopy Type Theory

In Homotopy Type Theory (HoTT), “pi” and “sigma” typically refer to specific type constructions: Pi-types and Sigma-types. These are fundamental building blocks in type theory, and they take on interesting meanings in the homotopical setting of HoTT. Let me break it down naturally:

• Pi-types (Π-types) are like “generalized function types.” They represent the type of functions where, given some index (from a type A), you get an element of a type that might depend on that index (a family of types B(a)). Think of it as “for all x in A, give me a y in B(x).” In HoTT, Pi-types correspond to universal quantification in logic, but they also have a geometric flavor—they can be thought of as “sections” of a fibration, tying into the homotopy perspective.

• Sigma-types (Σ-types) are like “dependent pairs” or “generalized product types.” They consist of pairs (a, b) where a is from type A, and b is from a type B(a) that depends on a. It’s a way to bundle together an element and some additional data that depends on it. In logic, Sigma-types align with existential quantification (“there exists an a in A such that b in B(a)”), and in HoTT, they’re interpreted as “total spaces” of fibrations, again connecting to the geometric intuition.

In HoTT, these types gain extra depth because of the interplay with paths, homotopies, and higher-dimensional structures. For example, the identity types (paths between elements) allow you to reason about how elements of Pi- and Sigma-types relate through equivalence or deformation, which is where the “homotopy” part shines.

Examples of Sigma-types

Let’s dive into an example of a Sigma-type (Σ-type) in Homotopy Type Theory (HoTT). Since HoTT builds on dependent type theory, a Sigma-type represents a dependent pair—think of it as a way to package an element of one type with an element of another type that depends on the first. I’ll keep it concrete and intuitive.

Example: Pairs of People and Their Ages

Imagine we’re modeling people and their ages. We’ll define:

• A type Person, which could include elements like Alice, Bob, and Charlie.

• For each person, a type Age(p) that depends on the person p : Person. For simplicity, let’s say Age(p) is just the type of natural numbers, Nat, representing possible ages.

In this setup:

• Person is the base type (let’s call it A).

• Age : Person → Type is a family of types indexed by Person (let’s call it B(p)).

The Sigma-type here is written as:

    Σ (p : Person), Age(p)

This type consists of all pairs (p, a) where:

• p is a person (an element of Person),

• a is a natural number (an element of Age(p)), representing p’s age.

So, some elements of this Sigma-type might look like:

• (Alice, 25): Alice is 25 years old.

• (Bob, 30): Bob is 30 years old.

• (Charlie, 42): Charlie is 42 years old.

What’s Happening?

• The first component, p : Person, picks a specific person.

• The second component, a : Age(p), gives an age that’s valid for that person. Since Age(p) is Nat here, it’s just a number, but in a more complex example, Age(p) could vary (e.g., Age(Child) might be numbers 0–17, while Age(Adult) might be 18 and up).

• The Sigma-type collects all such pairs into one type.

Notation and Intuition

In type theory syntax, you might see it written as:

    Σ[p : Person] Age(p)

or in a more programming-like style (e.g., in Agda or Coq):

    (p : Person) × Age(p)

The Σ symbol emphasizes the dependency: the second type depends on the value of the first. In HoTT, this isn’t just a static pair—it has a geometric interpretation as the “total space” of a fibration over Person, but for now, think of it as a structured way to pair data.

A Twist: Adding a Condition

Let’s make it more interesting. Suppose we only want pairs where the person’s age is even. We could define a type family IsEvenAge(p) : Nat → Type that checks if a number is even. Then the Sigma-type becomes:

    Σ (p : Person), Σ (a : Age(p)), IsEvenAge(p)(a)

Now an element might be:

• (Alice, (20, proof_that_20_is_even)): Alice is 20, and we include evidence that 20 is even. This nests Sigma-types, showing how flexible they are for encoding constraints.

Why It’s Useful

Sigma-types let you bundle related data with its dependencies explicit. In HoTT, they also play nicely with paths: you can define equivalences between such pairs (e.g., (Alice, 25) might be “the same” as (Alice, 25) via an identity path).

Examples of Pi-types

Let’s explore a Pi-type (Π-type) in Homotopy Type Theory (HoTT) with a concrete example. In HoTT, Pi-types represent dependent function types—think of them as functions where the output type depends on the input. They’re like “for all” statements: given any input from one type, you produce an output in a type that can vary with that input. Here’s a natural example to bring it to life.

Example: A Greeting Function for People

Suppose we have:

• A type Person with elements like Alice, Bob, and Charlie.

• A type family Greeting(p) that depends on the person p : Person. Let’s say Greeting(p) is the type of strings (String) tailored for each person. For instance, the greeting might need to be specific to their name or preferences, but for simplicity, we’ll keep it as String for all.

The Pi-type is written as:

    Π (p : Person), Greeting(p)

This type represents functions that, for every person p in Person, return a greeting string in Greeting(p). In other words, it’s the type of all possible functions that can assign a greeting to each person.

An element of this Pi-type—a specific function—might look like:

• Define greet : Π (p : Person), Greeting(p) where:

  • greet(Alice) = “Hello, Alice!”

  • greet(Bob) = “Hi, Bob!”

  • greet(Charlie) = “Hey, Charlie!”

What’s Happening?

• The input is p : Person, so the function must handle any person.

• The output is in Greeting(p), a type that depends on p. Here, it’s just String, but it could be more restrictive (e.g., Greeting(Alice) could be positive strings only, while Greeting(Bob) allows any string).

• The Pi-type ensures the function works universally across all inputs from Person.

Notation and Intuition

In type theory, you might see it as:

    Π[p : Person] Greeting(p)

or in a programming-like style (e.g., Agda or Coq):

    (p : Person) → Greeting(p)

The Π symbol highlights the dependency: the output type can change based on the input. In HoTT, Pi-types have a geometric twist—they correspond to “sections” of a fibration, but for now, think of them as a way to define consistent behavior over a whole domain.

A Twist: Personalized Length Constraints

Let’s spice it up. Suppose Greeting(p) isn’t just any string, but a string with a length constraint that depends on the person:

• Greeting(Alice) = strings of length 10 or less.

• Greeting(Bob) = strings of length 5 or less.

• Greeting(Charlie) = any string (no length limit).

Now the Pi-type Π (p : Person), Greeting(p) is the type of functions that, for each person, return a string meeting that person’s specific length rule. An example function might be:

• greet(Alice) = “Hi Alice!” (length 9 ≤ 10),

• greet(Bob) = “Bob!” (length 4 ≤ 5),

• greet(Charlie) = “Charlie, you rock!” (any length works).

This shows how the output type depends on the input, making Pi-types more expressive than plain function types like Person → String.

Why It’s Useful

Pi-types encode universal properties or behaviors. In HoTT, they interact with paths and homotopies—e.g., you could ask if two greeting functions are “equivalent” via a path that transforms one into the other, preserving the dependency structure.