Homotopy Cardinality and Entropy

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.

v2: Major revision; new title, rigorous proofs, Theorems 3.4 and 5.3, Proposition 5.6, counterexamples in Remarks 3.6--3.7; thanks to Omer Cantor. v3: Corrected Remark 3.8 (figure-eight cardinality is infinitesimal, not -1); added arXiv:1811.07437, arXiv:2104.11399; thanks to N. C. Favier. v4: Added Remark 4.5 on homotopy quotients; added arXiv:2412.16386; updated affiliation. 8 pages