2025/10/17 by Emily Riehl, Riehl, Emily
Mathematics · Computer Science · #Homotopy and Cohomology in Algebraic Topology #Logic, programming, and type systems #Algebraic structures and combinatorial models
paper · pdf · doi:10.1137/25m1806569
Recently discovered domain-specific formal systems -- specifically homotopy type theory and simplicial type theory -- provide new perspectives on spaces and categories in a natively equivalence-invariant setting. In this note, we expose fundamental proof techniques from these parallel settings: describing induction principles over paths or arrows and constructions involving universes that are either univalent or directed univalent.