Homotopy Cardinality and Entropy

TL;DR

This paper investigates the relationship between homotopy type theory and information theory by defining homotopy cardinality for types, formulating Shannon entropy within this framework, and deriving related properties like the chain rule.

Contribution

It introduces a novel type-theoretic formulation of entropy using homotopy cardinality and explores its properties, including how it respects dependent sums but not dependent products.

Findings

Homotopy cardinality respects dependent sums under certain conditions.

Shannon entropy can be expressed as homotopy cardinality of a type.

Derived the chain rule for entropy in the homotopy type-theoretic setting.

Abstract

We explore connections between homotopy type theory and information theory through homotopy cardinality. We define probability types and random variable types, prove that homotopy cardinality respects dependent sums under truncation and decidability hypotheses, and show that it does not respect dependent products in general. Using the power series expansion of the logarithm, expressed type-theoretically through deloopings of finite cyclic groups, we formulate Shannon entropy as the homotopy cardinality of a type and derive the chain rule for entropy under a trivial-action hypothesis.