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.

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