Post #2346189

@dpiponi@mathstodon.xyz Very nice point of view! Also neatly visible in the construction of the free functor on a type constructor t :: Type → Type: data FreeF t a = MkFreeF (exists r. (t r, r → a)) A value of type FreeF t a consists of a type r, a value x :: t r and a function f :: r → a. We're recording which function r → a we'd like to apply to x via functorial lift at some point in the future, once we have a map from t to an actual functor.