[pizza]

Which is kind of ironic, because students take classes exactly because they feel 'immature' with respect to that subject.. Honestly, most of my smoothest educational experiences with hard topics assumed some immaturity on my part, and that that was OK

[dan-robertson]

People don’t generally take category theory because they don’t really understand how proofs work or how to read definitions. The maturity required is about being able to cope with proving things and following proofs based on definitions which will probably seem somewhat bizarre at first and unmotivated at first. The immaturity you seem to talk about is people taking category theory because they don’t know category theory but that’s different and not what is meant by mathematical maturity.

That said, a background in mathematics helps with category theory. Things like group theory, topology (particularly algebraic topology), Galois theory and set theory can be useful in motivating a lot of category theory. I’m yet to see much of a strong motivation from programming (where is there a functor that isn’t an endofunctor?)

[beezee]

When I first went from CT as an implementation detail of typed FP to studying CT on its own, I was very aggravated by this point: "where is there a functor that isn’t an endofunctor?"

Over time it has fallen away in two directions.

In one direction is that though you are always stuck in a category with types as objects and functions as arrows, that doesn't stop you from subdividing. This became more intuitive to me as I encountered more and more categories that are basically just Set with extra structure (just as the one we program in is basically Set with bottom). If you start putting extra structure on your arrows (that is something that carries around a function along with some extra proof-relevant structures, like say a way to show that some zero element in the domain under the function equals the zero element in the codomain and that multiplication is preserved under the function, now you have monoid-homomorphisms) then you end up in the general case with something that looks a lot like a binatural transformation of profunctors, which pretty cleanly encodes "exo"-functors between different sub-categories of the category with all types as objects and functions as arrows.

In the other direction is realizing that even imprecisely, there's quantifiable value in observing functors to and from the category of types and functions, say one between whiteboard diagrams and code, or between a specific problem domain and code, etc etc. If you have some other space with composable relationships that you want to preserve when you write code to correspond to it, or you have some other representation you want to produce based off some given codebase while preserving the structure of the code taken as input, you can gain a ton of conceptual leverage out of identifying a functor.

[exdsq]

Isn’t an endofunctor a morphism from/to the same category? So a functor would be any morphine from/to different categories, and that wouldn’t be an endofunctor?

Endofunctor: A -> A, for category A

Functor: A -> B, for categories A and B

[Twisol]

More or less. "Morphism" is defined by the category it lives in, so a functor is a morphism between categories in the category of (small) categories. (Insert technicalities about size concerns and Russell's paradox.)

In particular, a map between categories that does not preserve composition is not a functor. It is important that F(f;g) = F(f);F(g).

[dan-robertson]

In the typical functional programmers view of category theory, there is only one category of interest so all functors are endofunctors. My main issue is that category theory the thing being studied is categories plural and so I feel like the language of category theory is being used to only ever talk about a single category.

It feels like doing “group theory” entirely with the symmetric group of the integers. While it’s true that the group is very general and has interesting properties, the focus of group theory isn’t single groups but rather the relationships between groups.

Compare this to something like algebraic topology or Galois theory where you have a Galois correspondence (a functor) between objects you’re interested in and groups.