Added imports to description

Ah. I just meant "Prove collections of universal arrows equivalent to Adjoint functor". Maybe I should use more specific phrasing. : )

Actually, this kind of kata is always encouraged to first solve locally. So you can use various tools provided by your proof assistant to construct the proof. As the name "interactive theorem prover" suggested.

And because the only thing test case doing is verify the type is correct. Thence your proof isn't actually "running" anyways. Only the "compiler" is doing the jobs making sure your proof "compiles".

Therefor if your proof assistant accepted your proof locally. You can pretty sure your proof is correct and verified. Because the sample test case is exactly same as real test case.

I think rather we should greatly increase the global timeout limit for proof assistant related languages. Because in general the above applied to most of them.

Best regards <3

Thanks for your translation! I'm not familiar with Coq. So there is a little question. Is there a reason to have r of nat -> Prop? Can this type be more general?

Great kata! Last task is easy to prove by "Type Driven Proof". But took me relatively long time to get it looks pretty and clear for myself.

Approved!

Approved. Thanks for translation!

Approved.

But fix is not total and it has type of (a -> a) -> a. And you really want your proof to be total and avoid self-reference proof.

And generally there is no common way to check whether given function is total. Beacause halting problem is undecidable.

Edit: And there is another function that can have type of Void -> Void. It's id.

But let me tell a story. We got detective and criminal fighting with each other. The bad thing is:

1. Detective can't treat a person who has not committed a crime as a criminal.
2. Detective should brought all criminals to justice.
3. Criminal can always find new ways to circumvent detective.
4. There is no ultimate way to prevent criminal from committing crimes.

Then detective carfully using axioms and modus ponens to find the solution. So... :p

Thx for suggestion. Grammar corrected.

And we got another kata for proving elementary math is correct! :p

This one is definitely harder than addition one. Because induction on right is not by definition. And proving it is harder than addition.

I am not very familiar with the beta process. Did it require some amount of completion. Or how can I approve katas?