definitional inversion 1dependent type theory 1domain theory 1injectivity 1non-normalising systems 1
From the 1 of 10 linked papers with an AI index.
Showing math.ACShow all
2 papers · 1 filter
math.AC2026
Azumaya algebras and Barr Theorem
Thierry Coquand, Henri Lombardi, Stefan Neuwirth
We study etale topology and the notion of Azumaya algebra over a commutative ring constructively. As an application of the syntactic version of Barr's Theorem, we show the equivale…
math.AC2025
Heitmann dimension of distributive lattices and commutative rings
Thierry Coquand, Henri Lombardi, Claude Quitté
This paper is the English translation of the first 4 sections of the article ``Dimension de Heitmann des treillis distributifs et des anneaux commutatifs. Publications Mathématiqu…