Saved in:
Bibliographic Details
Main Author: Ortiz-Muñoz, Andrés
Format: Preprint
Published: 2025
Subjects:
Online Access:https://arxiv.org/abs/2501.10672
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866914391650205696
author Ortiz-Muñoz, Andrés
author_facet Ortiz-Muñoz, Andrés
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2501_10672
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Homotopy Cardinality and Entropy
Ortiz-Muñoz, Andrés
Category Theory
Information Theory
Mathematical Physics
94A17, 03B38, 18B40
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.
title Homotopy Cardinality and Entropy
topic Category Theory
Information Theory
Mathematical Physics
94A17, 03B38, 18B40
url https://arxiv.org/abs/2501.10672