DHoTT: A Temporal Extension of Homotopy Type Theory for Semantic Drift
By: Iman Poernomo
Potential Business Impact:
Helps computers understand changing ideas over time.
We introduce Dynamic Homotopy Type Theory (DHoTT), a temporal extension of Homotopy Type Theory (HoTT) designed to reason formally about concepts whose meanings evolve continuously or rupture discontinuously over time. While traditional HoTT captures identity and equivalence within a fixed semantic landscape, DHoTT enriches this framework by explicitly indexing types with a temporal parameter, allowing types themselves to deform, rupture, and reassemble as contexts shift. Formally, we show that DHoTT serves as the internal language of a presheaf topos over the linearly ordered time category. As a result, DHoTT (1) conservatively extends HoTT, recovering standard homotopy-theoretic reasoning when time is held constant; (2) preserves foundational structures such as univalence and higher inductive types; and (3) introduces new constructs (drift paths and rupture types) for precisely capturing semantic evolution and discontinuity. We illustrate the expressiveness of DHoTT through a worked example derived from conversational dynamics in large language models, highlighting its relevance to posthuman intelligence and the formal modeling of evolving meaning.
Similar Papers
Subtyping in DHOL -- Extended preprint
Logic in Computer Science
Lets computers prove harder math problems.
2-Coherent Internal Models of Homotopical Type Theory
Logic in Computer Science
Makes math logic work inside itself.
The Yoneda embedding in simplicial type theory
Logic in Computer Science
Builds math tools for complex shapes.