I might not add much to the formal expression of the situation, but a less formal way I intuited the “power” of Functor was by thinking about “what information” the implementation of `Functor`

requires (said, differently, how does the information encoded in the implementation of `Functor`

augment the system).

The quick answer is that it doesn’t. The type *is* a `Functor`

regardless of whether a programmer chose to implement the type class. In other words, it’s an *inherent* property of a subset of types “out there”. It’s an interpretation that requires a little blurring of the eyes. Notwithstanding, I hold to this view because when given that a type can be known by it’s constructor, a generic truth in a few computing contexts, it so happens to be precisely what is required to implement `Functor`

. The “subset” nature of `Functor`

comes from the fact that is is not just any old constructor, but a type constructor.

The programmatic “job” of implementing a `Functor`

requires the information required to both deconstruct and reconstruct the value. An implementation of `Functor`

must host the type constructor logic that *is* what makes a type a `Functor`

; one in the same. That “promise” to deconstruct and re-construct the value without distorting the payload, is accomplished with the first law.

I suspect the statement:

… lies in the fact that in the “computing” context and in any language where the type aligns with the its constructor (so where there can only be *one* constructor for a given value), we get the second law for free.

Does that mean the only context in which we need to demonstrate the second law is one in which the interaction between the type constructor and the value of the payload is not “linear”/constant?