3 papers
math.CT2026
The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
Tom de Jong, Nicolai Kraus, Axel Ljungström
Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can…
math.AT2024
Symmetric Monoidal Smash Products in Homotopy Type Theory
Axel Ljungström
In Homotopy Type Theory, few constructions have proved as troublesome as the smash product. While its definition is just as direct as in classical mathematics, one quickly realises…
math.AT2024
Computational Synthetic Cohomology Theory in Homotopy Type Theory
Axel Ljungström, Anders Mörtberg
This paper discusses the development of synthetic cohomology in Homotopy Type Theory (HoTT), as well as its computer formalisation. The objectives of this paper are (1) to generali…