Understanding Identity functor

Question

I am working my way through this tutorial. As documented in the tutorial, I copied some code as below, to represent functor composition and identity functor:

{-# LANGUAGE FlexibleContexts #-}
module Test where

newtype FComp f g a = C { unC :: f (g a) }

instance (Show (f (g a))) => Show (FComp f g a) where
  show (C x) = "FComp " ++ show x

instance (Functor f, Functor g) => Functor (FComp f g) where
  fmap h (C x) = C (fmap (fmap h) x)

newtype Id a = Identity { unId :: a } deriving Show

instance Functor Id where
    fmap f x = Identity (f (unId x))

Now, this is what the tutorial states about identity functor:

Composition with the identity functor in the same category is as expected.
F∘IdB = F  
IdA∘F = F

What I am stuck at is trying to think of it in terms of functor composition as represented by FComp in the code above. An example below:

$ let a = C (Identity (Just (5::Int)))
$ :t a
a :: FComp Id Maybe Int
$ let b = C (Just (Identity (5::Int)))
$ :t b
b :: FComp Maybe Id Int

I can't think of a way to assert that types of a and b as represented in example above are identical. I will appreciate pointers on how to think of identity functor in terms of functor composition.

Answer 1

Like many equations in Haskell-applied category theory, F ∘ Id_B ≡ Id_A ∘ F ≡ F should really just be read as equivalences. FComp Id Maybe Int is very much not the same thing as FComp Maybe Id Int to the type checker; however you can easily write

idFunctorIso :: Functor f => FComp f Id a -> f a
idFunctorIso (C fIdca) = fmap unId fIdca

idFunctorIso' :: Functor f => f a -> FComp f Id a
idFunctorIso' fa = C $ fmap Identity fIdc

which implies that both types contain the same information¹. That's what we mean by saying they're isomorphic.

---

¹No information is lost in either direction, since idFunctorIso' . idFunctorIso ≡ id (as follows from the functor law fmap id ≡ id, together with the fact that unC and unId are simple inverses of the newtype constructors).