Algebraic closures and arithmetic universes

Hi, There's a question at MathOverflow on the construction of algebraic closures in constructive mathematics by Joyal. The idea as far as I can tell is to construct the classifying arithmetic universe for the theory of the algebraic closure. People might either be interested or have something to contribute https://mathoverflow.net/q/277551/4177 I repeat my respectful call for André to release his notes of arithmetic universes for us all to use, or at the least confirm that Maietti et al found the same definition :-) Best regards, David [For admin and other information see: http://www.mta.ca/~cat-dist/ ]