Homotopical Entropy

TL;DR

The paper addresses rewriting entropy and relative entropy in a homotopy-type-theoretic framework by replacing probability spaces with probability types and random variables with dependent types, connected via homotopy cardinality. It defines the exponential of entropy $2^{H(p)}$ and the exponential of relative entropy $2^{D(p\parallel q)}$ using dependent-type cardinalities and natural-transformations, notably linking $2^{H(p)}$ to $|\\texttt{Id}_X=\\texttt{Id}_X|$. Key constructs include probability types ($|X|=1$), random variable types ($|\\sum P_x|=1$), and a diversity interpretation $2^{H(p)}=|\\texttt{Id}_X=\\texttt{Id}_X|$, which grounds entropy in the homotopical structure of types. If successful, the program aims to transfer analytic notions into HoTT as real-valued quantities, enable a vector-like interpretation of dependent types, and broaden access to higher mathematics by treating homotopy types as numerical objects and dependent types as structured data.

Abstract

We present a "homotopification" of fundamental concepts from information theory. Using homotopy type theory, we define homotopy types that behave analogously to probability spaces, random variables, and the exponentials of Shannon entropy and relative entropy. The original analytic theories emerge through homotopy cardinality, which maps homotopy types to real numbers and generalizes the cardinality of sets.