The models in that book are non-trivial models of CZF + a ring R satisfying the principles of smooth infinitesimal analysis, e.g., that all total functions from R to R are differentiable. Since the model is non-trivial this proves that assuming one exists in CZF is consistent.

Yes there's entire books about such models: link.springer.com/book/10.1007/978-1-4757-4143-8

Isn't the fact that it is the category of algebras for the ultrafilter monad already a universal property?

What unit and counit are you asking to be invertible?

I think "admissible" is the wrong word here. You probably mean consistent?

By groupoidification do you mean the "core" where you take the isomorphisms that already exist or the "free groupoid" which freely adds inverses to all morphisms (the right and left adjoints respectively to the inclusion of groupoids into categories)?