Dear cafe, We know how to derive free theorems from a type [1]. But there exist also examples where the existence of a certain function determines the type. I suppose this is a special case of a free theorem? For example, every functor that is right adjoint to another functor in Hask is representable in the sense of [2], that is, isomorphic to (r->) for some type r. [see * below] I have two type signatures where I conjecture the only functors satisfying these are the Identity functor and functors of the form (,)s. Can anyone give hints as how to tackle a proof? Signature 1: What functors t admit a function forall f. Functor f => t (f a) -> f (t a) Signature 2: What functors t admit a function t (t a -> b) -> a -> b Signature 1 is like Data.Traversable.sequence, only the Applicative constraint is weakened to Functor. It is somewhat dual to Distributive [3]. Signature 2 can, with some currying, for t = (,)s be transformed into Data.Function.flip. I am unable to comprehend the free theorem for signature 2. For signature 1, the Rank-2 type seems to cause trouble with free-theorems? Thanks, Olaf [1] https://hackage.haskell.org/package/free-theorems [2] https://hackage.haskell.org/package/adjunctions [3] https://hackage.haskell.org/package/distributive [*] The argument goes like this: (1) bottoms aside, every type x is isomorphic to () -> x. (2) f and g are adjoint if and only if (f a -> b) is isomorphic to (a -> g b). (3) g b is isomorphic to () -> g b by (1) with x = g b (4) () -> g b is isomorphic to f () -> b by (2) with a = (). (5) By (3) and (4), g b is isomorphic to f () -> b. We have found g = (r->) with r = f ().