Zulip Chat Archive

Stream: mathlib4

Topic: !4#2969

Jeremy Tan (Mar 18 2023 at 07:58):

!4#2969 aesop_cat can only just about prove the Category ((co)Monad C) instances here, and it fails on the later declarations. Can someone help with all of this?

Jeremy Tan (Mar 18 2023 at 07:58):

I can't extract less-time-consuming proofs for the Category ((co)Monad C)instances

Jeremy Tan (Mar 18 2023 at 15:02):

(.)

Joël Riou (Mar 18 2023 at 22:29):

I have made some fixes https://github.com/leanprover-community/mathlib4/pull/2969/commits/73a87a14ca50e80e39fd5f70fff44639eee82c2b . In order to ease automation, I have added the @[ext] lemma MonadHom.ext' so that it applies to morphisms in the category Monad C (rather than the type synonym MonadHom). To make the Category instances compile in a reasonable time, I have mostly taken the proofs that were in mathlib.

Jeremy Tan (Mar 19 2023 at 03:15):

Joël Riou said:

I have made some fixes https://github.com/leanprover-community/mathlib4/pull/2969/commits/73a87a14ca50e80e39fd5f70fff44639eee82c2b . In order to ease automation, I have added the @[ext] lemma MonadHom.ext' so that it applies to morphisms in the category Monad C (rather than the type synonym MonadHom). To make the Category instances compile in a reasonable time, I have mostly taken the proofs that were in mathlib.

:squared_ok:

Jeremy Tan (Mar 23 2023 at 17:12):

OK, I'm totally stumped on how the simplified LHS from the simpNF linter needs extra hypotheses to even type-check, and then after adding the new hypotheses the same linter reports another error

Jeremy Tan (Mar 23 2023 at 17:12):

Can someone help me out on this?

Last updated: Dec 20 2023 at 11:08 UTC