MonadRun

Stream: mathlib4

[Kevin Buzzard]

For my sins I am porting Control.Traversable.Basic and at some point near the end of the file it uses that id is a monad. I traced this back to an instance in core Lean 3 which might not exist in Lean 4? Assuming it doesn't, I want to port init.control.id from core Lean 3 into mathlib4 (here is lean3port's opinion on the matter). However this file contains two things: the instance I want, and an instance of MonadRun id id, and MonadRun is defined in init.control.lift which is here in lean3port and here in lean3 and is full of monad-like-coercion-like things so I think it's time to confess I'm out of my depth. do I just port the monad instance and ignore monad_run or does init.control.lift need to be ported too?

[Scott Morrison]

Id is a monad, but id isn't.

[Kevin Buzzard]

I'll learn the naming convention one of these days! Thanks! I suspect there might be more to it than this but now it's time for bed; I have clearly misdiagonosed the actual problem (which I'll get back to tomorrow)

[Kevin Buzzard]

OK so the actual problem is that id.mk : α → id α but I want a term of type α → Id α; id (id.mk) works... So in fact I wasn't being completely stupid -- I think id _is_ a monad in Lean 3, and the translation of id to Lean 4 is id but then there's also Id, which is a monad in Lean 4 but which doesn't have as much API as id.

[Adam Topaz]

this (i.e. α → Id α) is pure