<div dir="ltr">Hi,<div><br></div><div>Suppose you have something like:</div><div><br></div><div>data Tree a = Leaf a | Branch (Tree a) (Tree a)</div><div><br></div><div>instance Functor Tree where</div><div>  fmap f (Leaf a) = Leaf $ f a</div><div>  fmap f (Branch l r) = Branch (fmap f l) (fmap f r)</div><div><br></div><div>To check that fmap id = id, I can see that the case for Leaf is ok:</div><div>  fmap id (Leaf a) = Leaf $ id a = Leaf a</div><div><br></div><div>How would you prove it for the second case? Is some sort of inductive proof necessary? I found this: <a href="http://ssomayyajula.github.io/posts/2015-11-07-proofs-of-functor-laws-with-Haskell.html">http://ssomayyajula.github.io/posts/2015-11-07-proofs-of-functor-laws-with-Haskell.html</a>, which goes over an inductive (on the length of the list) proof for the list type, but I'm not sure how to do it for a Tree.</div><div><br></div><div>Thanks,</div><div><br></div><div>toz</div><div><br></div></div>