Showing 2026Show all
2 papers · 1 filter
math.CT2026
Directed univalence for simplicial objects in an -topos
Evan Cavallo, Emily Riehl, Christian Sattler
A fundamental component of homotopy type theory, a synthetic theory of -groupoids, is Voevodsky's univalence axiom. Univalence characterizes the identity types in the unive…
cs.LO2026
Eliminating reversals from cubical type theories
Evan Cavallo, Christian Sattler
Cubical type theories are designed around an abstract unit interval from which types of paths, used to represent equalities, are defined. Varying the operations available on this i…