Homotopy Cardinality and Entropy
This work provides a theoretical bridge between abstract mathematics and information theory, but it is incremental as it builds on existing homotopy type theory concepts without broad practical applications.
The paper tackles the problem of connecting homotopy type theory with information theory by defining probability and random variable types, proving that homotopy cardinality respects dependent sums under certain conditions but not dependent products, and formulating Shannon entropy as homotopy cardinality to derive the chain rule.
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.