Proving the Functor laws for free monads; am I doing it right?

Question

I'm having a bit of a hard time understanding how to prove the Functor and Monad laws for free monads. First off, let me put up the definitions I'm using:

data Free f a = Pure a | Free (f (Free f a))

instance Functor f => Functor (Free f) where
    fmap f (Pure a) = Pure (f a)
    fmap f (Free fa) = Free (fmap (fmap f) fa)

instance Functor f => Monad (Free f) where
    return = Pure
    Pure a >>= f = f a
    Free fa >>= f = Free (fmap (>>=f) fa)

{-

Functor laws:
(1) fmap id x == x
(2) fmap f (fmap g x) = fmap (f . g) x

Monad laws:
(1) return a >>= f   ==  f a
(2) m >>= return     ==  m
(3) (m >>= f) >>= g  ==  m >>= (\x -> f x >>= g)

-}

If I understand things correctly, the equational proofs require appeal to a coinductive hypothesis, and it goes more or less like this example:

Proof: fmap id == id

Case 1: x := Pure a
fmap id (Pure a)
  == Pure (id a)   -- Functor instance for Free
  == Pure a        -- id a == a

Case 2: x := Free fa
fmap id (Free fa)
  == Free (fmap (fmap id) fa)  -- Functor instance for Free f
  == Free (fmap id fa)         -- By coinductive hypothesis; is this step right?
  == Free fa                   -- Functor f => Functor (Free f), + functor law 

I've highlighted the step where I'm not sure if I'm doing things right.

If that proof is right, then the proof for the Free constructor case of the second law is as follows:

fmap f (fmap g (Free fa))
  == fmap f (Free (fmap (fmap g) fa))
  == Free (fmap (fmap f) (fmap (fmap g) fa))
  == Free (fmap (fmap f . fmap g) fa)
  == Free (fmap (fmap (f . g)) fa)           -- By coinductive hypothesis
  == fmap (f . g) (Free fa)

Answer 1

Yes, this is correct. The 'base case' for the coinduction is the Pure constructor, and the induction is over levels of nesting of the Free constructor.

The complete proofs are

-- 1. First functor law

--   a. Base case

fmap id (Pure a) = Pure (id a) -- Functor instance for Free
                 = Pure a      -- definition of id

--   b. Inductive case

fmap id (Free fa) = Free (fmap (fmap id) fa) -- Functor instance for Free
                  = Free (fmap id fa)        -- coinductive hypothesis
                  = Free fa                  -- 1st functor law for f

-- 2. Second functor law

--   a. Base case

fmap f (fmap g (Pure a)) = fmap f (Pure (g a))   -- Functor instance for Free
                         = Pure (f (g a))        -- Functor instance for Free
                         = Pure ((f . g) a)      -- Definition of (.)
                         = fmap (f . g) (Pure a) -- Functor instance for Free

--   b. Inductive case

fmap f (fmap g (Free fa)) = fmap f (Free (fmap (fmap g) fa))        -- Functor instance for Free
                          = Free (fmap (fmap f) (fmap (fmap g) fa)) -- Functor instance for Free
                          = Free (fmap (fmap f . fmap g) fa)        -- 2nd functor law for f
                          = Free (fmap (fmap (f . g) fa))           -- Coinductive hypothesis
                          = fmap (f . g) (Free fa)                  -- Functor instance for Free