Showing 2026Show all
4 papers · 1 filter
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
Two Remarks about Game Semantics of Classical Logic
Thierry Coquand
We present and explain two unpublished remarks of Stefano Berardi connected to game semantics.
cs.LO2026
A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
Marc Bezem, Thierry Coquand, Peter Dybjer +1
We present generalized algebraic theories corresponding to slightly modified versions of two of the type theories in our paper Type Theory with Explicit Universe Polymorphism. We f…
math.AC2026
Local structure of etale algebras
Thierry Coquand
The goal of this note is to provide a constructive version of the proof of local structure of etale algebras.