3 papers
cs.LO2026
Constructive higher sheaf models with applications to synthetic mathematics
Thierry Coquand, Jonas Höfer, Christian Sattler
There have recently been several developments in synthetic mathematics using extensions of dependent type theory with univalence and higher inductive types: simplicial homotopy typ…
cs.LO2026
Univalence without function extensionality
Evan Cavallo, Jonas Höfer
It is a well-known theorem of homotopy type theory, originally due to Voevodsky, that function extensionality holds inside any univalent universe. We consider a weaker variant of t…
math.CO2023
--Factorization and the Binary Case of Simon's Congruence
Pamela Fleischmann, Jonas Höfer, Annika Huch +1
In 1991 Hébrard introduced a factorization of words that turned out to be a powerful tool for the investigation of a word's scattered factors (also known as (scattered) subwords or…