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.

翻译：本文通过同伦基数探讨同伦类型论与信息论之间的联系。我们定义了概率类型与随机变量类型，证明了在截断与可判定性假设下同伦基数保持依赖和，并表明其通常不保持依赖积。利用对数的幂级数展开（通过有限循环群的分环在类型论中表达），我们将香农熵表述为类型的同伦基数，并在平凡作用假设下推导出熵的链式法则。