Id vs id as a monad

Stream: mathlib4

[Eric Wieser]

Currently docs#instULiftableIdTypeIdType is stated about id instead of Id. Is id ever used as a Monad, or does this only really make sense for Id?

[Mario Carneiro]

id is not used as a monad to my knowledge. Is there even an instance for it?

[Eric Wieser]

I guess ULiftable is used for monads but doesn't actually enforce that use; so maybe id is a porting typo?

[Mario Carneiro]

there doesn't seem to be, although I didn't try it with import Mathlib

[Mario Carneiro]

seems likely

[Eric Wieser]

#5796 currently adds the Id version

[Eric Wieser]

Should I delete the id version?

[Eric Wieser]

Done