I don't know the Arens-Michael envelope, but I do know that many constructions described using the word "envelope" are not functorial unless one makes a dramatic adjustment. For example, neither the injective envelope/hull of a module, nor the Dedekind-MacNeille completion of a poset, nor the algebraic closure of a field, are functorial in the ordinary sense. Is the Arens-Michael envelope functorial?

When are realizability toposes cocomplete? Are there any nondegenerate examples?

@DavidRoberts As best I know: coherent toposes are sheaf toposes by definition; I don't think realizability toposes are sheaf toposes.

I wasn't really recommending the paper; I was just pointing out one answer that Mathias might give to the title question. I acknowledge that the question as asked in your post is looking at something else.

One reason that Mathias gives -- I do not recall which paper -- is that Bourbaki doesn't honestly use the $\tau$-calculus because it is wildly convoluted and impractical. Ah, here it is: dpmms.cam.ac.uk/~ardm/inefff.pdf The length of the term that defines $1$ is $4,523,659,424,929$.

Some pretty awesome snark there.

The fact that the group of integer points is infinite cyclic (or at least the torsionfree part is) is nicely seen from the fact that you get a discrete subgroup of the positive branch that is an isomorph of $\mathbb{R}$.

Comments are not for extended discussion; this conversation has been moved to chat.

A side note: it's a bit of a stretch to call the proof of impossibility of trisecting an angle (like 60 degrees) "Galois theory". All you really need is that for two extension fields $E \subseteq F \subseteq K$, the degree $\dim_E F$ divides $\dim_E K$.

But for what I did write: I think it more or less boils down to saying that conjugating (the identity functor say) by different maps usually results in different functors. If we just consider the full subcategory on a single $n$-dimensional object $V$, then two such functors, corresponding to two inner automorphisms $g \mapsto SgS^{-1}, TgT^{-1}$ on $GL(V)$, are the same iff $S$ is a scalar multiple of $T$.

Mainly I was answering to pin down a precise content to the oft-repeated statement, arriving at: there is no natural isomorphism from the identity to the standard (covariant) dual functor $f \mapsto (f^{-1})^\ast$. So it would have been better to write: "they will never produce the standard dual functor". That seems perfectly formal, and formally provable: it's enough to work in $GL_2$ and show that $f \mapsto (f^{-1})^\ast$ is not an inner automorphism; for example, you can never conjugate $2\cdot I$ into $(1/2) \cdot I$.

Thanks very much.

I think we agree on the fundamentals: that in order to make sense of an assertion that the identity functor is or isn't isomorphic to the dual functor, one must first be clear on what exactly the dual functor is, including how it is defined on morphisms. I would still appreciate it if you would strike through where you say (my objection) isn't fair, which you now agree isn't the case, but you've still let it stand in your answer. This could be confusing to some readers.