2 papers
cs.PL2025
From Semantics to Syntax: A Type Theory for Comprehension Categories
Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens +1
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial…
cs.LO2024
Intrinsically Correct Sorting in Cubical Agda
Cass Alexandru, Vikraman Choudhury, Jurriaan Rot +1
The paper "Sorting with Bialgebras and Distributive Laws" by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between f…