Homotopy Cardinality and Entropy

This paper establishes a bridge between homotopy type theory and information theory by defining probability types, demonstrating that homotopy cardinality respects dependent sums but not products, and deriving Shannon entropy and its chain rule as the homotopy cardinality of specific types constructed via deloopings of finite cyclic groups.

The Gist

Imagine you are trying to measure the "size" of a shape, but not just its physical area or volume. You want to measure its complexity and uncertainty.

This paper, written by Andrés Ortiz-Muñoz, is a bridge between two very different worlds:

1. Homotopy Type Theory: A branch of math that treats logical statements as shapes and spaces.
2. Information Theory: The science of data, probability, and how much "surprise" is in a message (Entropy).

The author's big discovery? Shannon Entropy (the standard measure of uncertainty in information theory) is actually just a specific way of counting the "size" of a mathematical shape.

Here is the breakdown using simple analogies:

1. The "Weighted" Size of a Shape

In normal math, if you have a set of 3 apples, the size is 3.
In this paper's world (Homotopy Cardinality), things are more like a bouncy castle.

• If you have a simple apple, it counts as 1.
• If you have a shape that can wiggle or rotate in specific ways (like a spinning top), it counts as a fraction.
• The Rule: The more ways a shape can wiggle (its symmetries), the smaller its "cardinality" (size) becomes.
  • Analogy: Imagine a fair coin. It has two sides (Heads, Tails). But it also has a "flip" symmetry. In this math, the "size" of the coin isn't 2; it's actually 1 (because the two sides are balanced by the flip). This is called a Probability Type. It's a shape that perfectly represents a 100% chance of something happening.

2. The "Surprise" Machine (Entropy)

Entropy is a measure of how much you don't know.

• If you know a coin is rigged to always land on Heads, there is zero surprise (Zero Entropy).
• If you have a fair coin, there is maximum surprise (High Entropy).

The paper asks: Can we build a shape where the "size" of the shape equals the "surprise" of the coin?

The Answer: Yes.
The author builds a weird, abstract shape using "loops" and "cycles" (think of a necklace made of beads).

• He uses a mathematical trick involving logarithms (the math behind compound interest and information).
• He constructs a shape that represents "everything that is not the current outcome."
• When he calculates the "size" (Homotopy Cardinality) of this specific shape, the number that pops out is exactly the Shannon Entropy.

The Metaphor:
Imagine you are trying to guess a secret code.

• Entropy is how many questions you need to ask to figure it out.
• The author built a giant, abstract "Question Machine" (a type).
• The "weight" of this machine is exactly equal to the number of questions you need to ask.

3. The Chain Rule (The "Lego" Problem)

In information theory, there is a famous rule called the Chain Rule. It says:

The total surprise of a story is the surprise of the first sentence, plus the average surprise of the rest of the story, given the first sentence.

The paper proves that this rule works in their shape-world, BUT with a catch.

• The Catch: The "rest of the story" must be independent of the "first sentence."
• The Analogy: Imagine building a tower out of Lego blocks.
  • If the blocks just stack on top of each other (independent), the total height is just the sum of the parts.
  • But if the blocks are twisted or glued together in a weird way (dependent), the total height changes.
  • In the math paper, this "twisting" is called Transport Action. If the shape twists as you move through it, the simple addition rule (Chain Rule) breaks. The paper shows exactly when the rule works (when there is no twisting) and when it fails.

4. What This Means for Us

This isn't just abstract math for math's sake. It suggests that uncertainty is a geometric property.

• Old View: Entropy is a formula you calculate with numbers.
• New View: Entropy is the physical "volume" of a shape made of logic and probability.

The author also points out where this math gets tricky. Sometimes, when you try to combine shapes (like multiplying functions), the "size" doesn't behave the way you expect. It's like trying to measure the volume of a shadow; sometimes the shadow disappears even though the object is there.

Summary

• The Goal: To find the "size" of uncertainty.
• The Method: Build a mathematical shape that represents a probability distribution.
• The Result: The "size" of this shape is exactly the Shannon Entropy.
• The Lesson: Information theory and the geometry of shapes are secretly the same language. When you understand the shape of a probability, you understand the information it carries.

It's like discovering that the "weight" of a mystery novel is exactly equal to the number of pages you have to turn to solve the mystery. The paper gives us the ruler to measure that weight.

Technical Summary

Here is a detailed technical summary of the paper "Homotopy Cardinality and Entropy" by Andrés Ortiz-Muñoz.

1. Problem Statement

The paper addresses the intersection of Homotopy Type Theory (HoTT) and Information Theory. Specifically, it investigates whether fundamental information-theoretic quantities, such as Shannon entropy, can be expressed as homotopy cardinalities of specific types.

While homotopy cardinality generalizes the cardinality of finite sets and groupoid cardinality (assigning a real number to a homotopy type), it is not immediately obvious how to capture the logarithmic nature of entropy ($H = -\sum p \ln p$) within the additive and multiplicative structure of type theory. The author seeks to:

1. Define probability distributions and random variables purely within HoTT.
2. Construct a type whose homotopy cardinality equals the Shannon entropy of a distribution.
3. Determine how homotopy cardinality interacts with dependent sums and products to derive the chain rule for entropy.

2. Methodology

The author works informally within the framework of Homotopy Type Theory (HoTT), utilizing the following core concepts:

• Homotopy Cardinality: Defined as $|X| := \sum_{x \in [X]} \frac{1}{|x=x|}$, where the sum is over the set truncation of $X$, and $|x=x|$ is the cardinality of the identity type (automorphism group).
• Truncation Levels: Utilizing $n$-truncated types (e.g., sets are 0-truncated, groupoids are 1-truncated) to manage path information.
• Dependent Types: Using dependent sums ($\sum$) and products ($\prod$) to model probabilistic structures.
• Power Series Expansion: Leveraging the Taylor series expansion of the natural logarithm: $-\ln(1-t) = \sum_{n=1}^{\infty} \frac{t^n}{n}$.
• Deloopings: Using the delooping of finite cyclic groups ($B\mathbb{Z}_n$) to represent the terms of the logarithmic series type-theoretically.

3. Key Contributions and Results

A. Foundations: Probability and Random Variable Types

• Probability Types: A type $X$ is defined as a probability type if $|X| = 1$. The probability of a term $x$ is defined as $p_x = 1/|x=x|$.
• Random Variable Types: A type family $P: X \to \mathcal{U}$ is a random variable type if the total space $\sum_{x:X} P(x)$ has cardinality 1. The induced probability distribution is $p_x = |P(x)|/|x=x|$.
• Closure under Dependent Sums: The paper proves that the dependent sum of probability types (under specific conditions) yields a new probability type, modeling the composition of distributions.

B. Homotopy Cardinality of Dependent Types

• Dependent Sums (Theorem 3.4): The author proves (attributed to Omer Cantor) that for a 1-truncated type $X$ and a family $P$ with decidable equality and bounded truncation, the cardinality respects the dependent sum:
  $$\left| \sum_{x:X} P(x) \right| = \sum_{x \in X} \frac{|P(x)|}{|x=x|}$$
  This formula relies on the orbit-stabilizer theorem applied to the action of the automorphism group of $x$ on the fibers.
• Failure of Dependent Products (Remark 3.6): The paper explicitly corrects a previous assumption, showing that $|X \to Y| = |Y|^{|X|}$ does not hold in general for homotopy types. A counterexample is provided using the type of 2-element sets ($Fin(2)$), where the naive formula fails due to non-trivial automorphisms.

C. Shannon Entropy as Homotopy Cardinality (Theorem 5.3)

This is the central result of the paper. The author constructs a specific type whose homotopy cardinality is exactly the Shannon entropy $H(p)$.

• Construction:
  1. Cycle Type ($C$): Defined as $\sum_{n \ge 1} B\mathbb{Z}_n$, representing the power series terms.
  2. Complement Type ($\bar{X}(x)$): For a probability type $X$, the complement at $x$ is the subtype of $X$ excluding the connected component of $x$. Its cardinality is $1 - p_x$.
  3. Entropy Type: The type is defined as $\sum_{x:X} \sum_{c:C} (c=c) \to \bar{X}(x)$.
• Derivation: By applying the power series expansion of $-\ln(1-t)$ and the properties of function types between sets (Remark 3.7), the cardinality of this constructed type evaluates to:
  $$\sum_{x \in X} p_x (-\ln(1 - (1-p_x))) = \sum_{x \in X} p_x (-\ln p_x) = H(p)$$

D. The Chain Rule for Entropy (Proposition 5.6)

The paper derives the chain rule for entropy: $H(A, B) = H(A) + \sum p_a H(B(a))$.

• Condition: This holds under the hypothesis that the transport action of the automorphism group $[a=a]$ on the fibers $[B(a)]$ is trivial.
• Significance: When the action is trivial, the set truncation of the dependent sum decomposes cleanly, allowing the joint distribution to factorize.
• Counterexample: If the transport action is non-trivial (twisted fiber bundles), the chain rule fails because the joint distribution is not a simple product of marginals.

4. Significance and Discussion

• Unification of Fields: The paper provides a rigorous type-theoretic foundation for Shannon entropy, showing it is not just an analogy but a direct consequence of homotopy cardinality.
• Connection to Operadic Composition: The results link HoTT to the Faddeev–Leinster characterization of entropy. The dependent sum of probability types corresponds to the operadic composition of distributions, and the chain rule corresponds to the derivation property in this framework.
• Limitations and Open Questions:
  • The chain rule for entropy types (lifting the equality of values to an equivalence of types) remains an open problem. The author suggests this is obstructed by the combinatorial complexity of "mixed necklaces" (cyclic sequences) which require Möbius inversion to resolve, preventing a simple bijective proof of $\ln(xy) = \ln x + \ln y$ at the type level.
  • The necessity of the 1-truncation and decidable equality hypotheses for the dependent sum formula is still under investigation.

Conclusion

Ortiz-Muñoz successfully demonstrates that Shannon entropy is the homotopy cardinality of a specific, explicitly constructed type involving deloopings of cyclic groups and complement types. This work bridges the gap between the structural properties of homotopy types and the axiomatic foundations of information theory, while carefully delineating the boundaries where standard cardinality formulas (like those for function types) break down in the homotopical setting.