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…