functor shapes

Stream: maths

[David A]

Intuitively, it seems like the following ought to be provable. predictable f g h seems to say that when y is "in" f x, g y = h x.

universe u
-- g measures from the "inside" of (f x) what h can measure from x alone.
def predictable {α β γ : Type u}
    {F : Type u → Type u} [functor F] [is_lawful_functor F]
    (f : α → F β) (g : β → γ) (h : α → γ) :=
  ∀ x : α, g <$> f x = h x <$ f x

theorem fork_predictable {α β γ δ : Type u}
    {F : Type u → Type u} [functor F] [is_lawful_functor F]
    (f : α → F β) (g : β → γ) (h : α → γ)
    (p : predictable f g h)
    (φ : β → γ → δ) (x : α) :
    (λ y, φ y (g y)) <$> f x = (λ y, φ y (h x)) <$> f x :=
sorry

However, working with it a bit I'm fairly confident it is not provable. First of all, x is the only possible α term in this scope. So, having fixed x, g <$> f x simply does not appear as a possible subterm of any expansion of (λ y, φ y (g y)) <$> f x. When you apply g you no longer have access to the "contents" of f x. But if you don't apply g right away, you'll never recover that exact subterm. This seems to eliminate any possibility of using the p x equality.

So, my questions are, is it correct this is unprovable, and does the statement fork_predictable have a counterexample?

Is there a reason for functor laws not to be able to prove this? Further investigation suggests that my fundamental problem is that I can't relate facts about g <$> f x back to f x: e.g. I can prove predictable f g h → functor.liftp (λ y, y = h x) (g <$> f x) but I don't think I can prove predictable f g h → functor.liftp (λ y, g y = h x) (f x). Without an inverse for g, it's as if g <$> f x might "contain" values which are not of the form g y for some y "in" f x, and might not contain all such values; i.e., as if map may not preserve shape.