Kata style

Stream: Codewars

[Bhavik Mehta]

Question for anyone: what sort of kata would be most interesting to see?
In my case, the task would be to prove no_double_powerset_monad below:

import category_theory.types
import category_theory.monad.basic

open category_theory monad

@[simps]
def P : Type ⥤ Type :=
{ obj := λ X, set X,
  map := λ X Y, set.image }

def no_double_powerset_monad : Prop := monad (P ⋙ P) → false

Now this isn't an easy proof: my lean version is over 500 lines (though I'm sure it can be condensed by at least a factor of 4), and the maths proof was only published in December 2018. That said, it doesn't involve any particularly advanced lean or maths, only a rough idea of the sets API and a very basic understanding of monads. As I see them, the options here are: 1) Present the kata essentially as above, with no hints. 2) Provide a link to the paper but no other information. 3) Provide an approximate lean framework for how the proof might look, so that users can fill in the gaps (but not enforce that the framework must be followed). Any suggestions?

[Donald Sebastian Leung]

I think (1) or (2) would be good, currently leaning towards (2). For (3), solvers can always ask for additional hints on the general structure of the proof if they are really stuck.

[Bhavik Mehta]

Fair enough - my concern is that solvers would struggle to come up with the proof: it was mentioned in the category theory literature before 2003 but not solved until 2018 - seems a little unfair to make solvers figure this out for the sake of a kata!