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.
Cite
@article{arxiv.2501.10672,
title = {Homotopy Cardinality and Entropy},
author = {Andrés Ortiz-Muñoz},
journal= {arXiv preprint arXiv:2501.10672},
year = {2026}
}
Comments
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