Do Functors preserve identities?

Stream: lean4

[Thomas Murrills]

I was reading through the Lean 4 manual entry for Functor (which is very nice, by the way!), and noticed that it doesn’t seem to be required that Functors preserve the identity function. Or is it? If so, where do we provide a proof of that? If not, shouldn’t this be required somehow? Or are Functors not really functors (though it seems to say so in the docs)?

[Kyle Miller]

The additional axioms are in the docs4#LawfulFunctor typeclass. I think the idea is that it separates the concerns of programs and proofs -- while a program might depend on the axioms of a Functor to be correct, I think it's rare that you need to use the axioms of a functor in the middle of a program.

[Kyle Miller]

This means that docs4#Functor is something more general than a functor, but you're meant to only use it for actual functors.

[Thomas Murrills]

Hmm, ok…is that a more typical definition for functional programmers? That would make sense…it is a bit of a gotcha coming from the math side, though! I might want to suggest a parenthetical be thrown into the part of the lean manual that says it’s the same as a categorical functor, like “(with the exception that a Functor in this context is not required to preserve identities)” or something.

[Thomas Murrills]

(Oh wait, is the manual contributable-to? It’s a minor change but maybe I could PR it…)

[Kyle Miller]

Lean 3's mathlib has both docs#functor (with its docs#is_lawful_functor) and docs#category_theory.functor

The first isn't really used in math as far as I am aware

[Kyle Miller]

Thomas Murrills said:

(Oh wait, is the manual contributable-to? It’s a minor change but maybe I could PR it…)

My understanding is that you can contribute to it! https://github.com/leanprover/lean4/blob/master/doc/monads/functors.lean (I believe @Chris Lovett wrote these sections)

[Thomas Murrills]

Anyway, it’s neat to know that LawfulFunctor is there if I need it, so thanks!

Practically, if I define something as an instance of LawfulFunctor, can I feed it to everything that requires a Functor? (Still learning how classes work…part of me would expect to see an extends somewhere in the source, but since I don’t, I’m not really sure.)

[Kyle Miller]

The LawfulFunctor class is using a pattern where it takes the [Functor F] as an additional argument. That way the data of the functor is not actually part of the class, and it's free to be a Prop. A tradeoff is that to define a lawful functor you have to first define the Functor instance and then follow up with the LawfulFunctor instance.

[Thomas Murrills]

Oh, I see…I would have thought it would be called isLawfulFunctor or something! Are there conventions in Lean for naming Props? Might it make sense to instead have LawfulFunctor be a typeclass that extends Functor with an inhabitant of isLawfulFunctor? Or is that bad/unnecessary/unconventional in Lean for some reason?

[Kevin Buzzard]

I totally agree that these prop classes should all be called is_.... This is apparently what's done in Isabelle and it's a very easy way to avoid confusion.

[Thomas Murrills]

Convention Proposal: natural-language-named prop classes should start with a present-tense third person singular verb, such as Is, Has, or a more specific one suited to the context. Linguistically, this means the type is read as a statement, and therefore interpreted as a proposition-as-type which can only sensibly be inhabited by (a proof of its own) truth—instead of a noun phrase, which we expect to be inhabited by data which is that noun phrase.