Nice, thanks!

]]>Done!

]]>If you feel like doing the world a service, you could create amnestic functor and add a section about strict monadicity to monadic functor, with references to amnestic functor and isofibration. (-:

]]>Ah, amnestic functors! How ironic that I forgot about them. Yes, exactly – an amnestic monadic isofibration is strictly monadic and vice versa. It corresponds nicely to the two parts of the proof too – a monadic isofibration is one where the comparison functor is strictly surjective on objects, and an amnestic monadic functor is one where the comparison functor is injective on objects. Put the two together and we get a strictly monadic functor. Thanks!

]]>Well, asking for the domain of a morphism to be unique but not the morphism itself is pretty bizarre, categorically speaking. I think “strict isofibration” would naturally mean the stronger sense. Also there is the notion of an “amnestic functor”, which reflects the property of an isomorphism being an identity; I think that isofibration + amnestic should be equivalent to what you want.

]]>Well, it seems to be the smallest modification to the definition of isofibration needed to make things work. A monadic functor is automatically faithful (can we prove this directly from the assumptions of the monadicity theorem?) so the isomorphism, once it exists, is unique up to the choice of endpoints – so we only need to add a uniqueness hypothesis on the object part of the lifting problem. But I’m also happy to consider names for functors where isomorphisms lift uniquely in the stronger sense.

]]>Your second bullet point confuses me. Are you looking for a name for a functor such that for any isomorphism $f:C\to U D$ there exists a unique $\tilde{C}$ such that there exists some (not necessarily unique) isomorphism $\tilde{f}:\tilde{C}\to D$ with $U\tilde{f} = f$? If so, why? As you mentioned, in your motivating example of a strictly monadic functor, also $\tilde{f}$ is unique.

]]>As far as I can tell, the difference between a monadic functor and a strictly monadic functor boils down to this: a strictly monadic functor $U : \mathcal{D} \to \mathcal{C}$ has the property that, for any object $D$ in $\mathcal{D}$ and any isomorphism $f : C \to U D$ in $\mathcal{C}$, there is a *unique* object $\tilde{C}$ and an (automatically unique) isomorphism $\tilde{f} : \tilde{C} \to D$ such that $U \tilde{f} = f$. Conversely, any monadic functor with this property is strictly monadic. This is very reminiscent of the definition of isofibration, but a monadic isofibration need not be strictly monadic. What’s a good phrase to describe functors like these for which isomorphisms lift uniquely?

- “Creates isomorphisms” on its own might be construed as “conservative”.
- “Isomorphisms lift uniquely” suggests something a little bit stronger than what I’m going for – the unique functor from a group to the terminal category admits unique solutions to the object part of the lifting problem (for obvious reasons) but not the isomorphism part.
- Maybe “strong/strict isofibration”…?