Showing 2026Show all
3 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…
math.LO2026
Projective Chromatic Numbers
Adrian Rettich, Luke Serafin
We extend classical notions of definable colourability of graphs to the general projective setting and investigate whether known results, mainly about the dichotomy and the $…
math.LO2026
Funicular preorders can be prelinearized without nonprincipal ultrafilters over
Azul Fatalini, Luke Serafin
It is a consequence of the axiom of choice that every preorder can be extended to a total preorder while respecting the strict preorder relation. We call such an extension a prelin…