Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
Strict Equality in Higher Identity Types: Axioms, Completeness, Decidability
Keri D'Angelo, Liron Cohen, Luke Serafin +1
Reasoning about higher identity types uses two equalities, strict equality and equivalence of cells witnessed by a path. Strict equality is a congruence for every operation on cell…
cs.LO2025
Morita Rigidity for Kleene Algebras
Luke Serafin
We introduce Morita equivalence to the study of Kleene algebras and modules. Classical characterizations of Morita-equivalent semirings such as having equivalent categories of modu…