9 papers
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…
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 $…
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…
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…
Ultrafilters over Successor Cardinals and the Tukey Order
Tom Benhamou, Justin T. Moore, Luke Serafin
We study ultrafilters on regular uncountable cardinals, with a primary focus on , and particularly in relation to the Tukey order on directed sets. Results include the indepen…
On Strongly-equitable Social Welfare Orders Without the Axiom of Choice
Luke Serafin
Social welfare orders seek to combine the disparate preferences of an infinite sequence of generations into a single, societal preference order in some reasonably-equitable way. In…
Ultrafilters, Transversals, and the Hat Game
Luke Serafin
Geschke, Lubarsky, and Rahn in ``Choice and the Hat Game''~\cite{choice-and-the-hat-game} generalize the classic hat game puzzle to infinitely-many players and ask whether every mo…
On generalizations of separating and splitting families
Daniel Condon, Samuel Coskey, Luke Serafin +1
The work in this article is concerned with two different types of families of finite sets: separating families and splitting families (they are also called "systems"). These famili…
A formally verified proof of the Central Limit Theorem
Jeremy Avigad, Johannes Hölzl, Luke Serafin
We describe a proof of the Central Limit Theorem that has been formally verified in the Isabelle proof assistant. Our formalization builds upon and extends Isabelle's libraries for…