Comonad as comonoid on hask with composition and identity as monoidal structure

Test.hs

{-# LANGUAGE
    TypeOperators
  , RankNTypes
  , MultiParamTypeClasses
  , ConstraintKinds
  , QuantifiedConstraints
  , KindSignatures
#-}

module Main where

import Data.Coerce
import Data.Maybe
import Data.List
import Control.Monad
import Data.Functor.Identity
import Data.Functor.Compose
import GHC.Exts (Constraint)

type f :~> g = forall x. f x -> g x

bimapC ::
  (Functor f, Functor g) =>
  (f :~> f') ->
  (g :~> g') ->
  (Compose f g :~> Compose f' g')
bimapC ff' gg' (Compose fga) = Compose . ff' . fmap gg' $ fga

lmapC ::
  (Functor f, Functor g) =>
  (f :~> f') ->
  (Compose f g :~> Compose f' g)
lmapC f = bimapC f id

rmapC ::
  (Functor f, Functor g) =>
  (g :~> g') ->
  (Compose f g :~> Compose f g')
rmapC g = bimapC id g

type Parametric f = (forall a b. (Coercible a b => Coercible (f a) (f b)) :: Constraint)

alpha_1 ::
  (Parametric f, Parametric g, Parametric h) =>
  (Compose f (Compose g h) :~> Compose (Compose f g) h)
alpha_1 = coerce

alpha_2 ::
  (Parametric f, Parametric g, Parametric h) =>
  (Compose (Compose f g) h :~> Compose f (Compose g h))
alpha_2 = coerce

lambda_1 ::
  (Parametric f) =>
  f :~> Compose Identity f
lambda_1 = coerce

lambda_2 ::
  (Parametric f) =>
  Compose Identity f :~> f
lambda_2 = coerce

rho_1 ::
  (Parametric f) =>
  f :~> Compose f Identity
rho_1 = coerce

rho_2 ::
  (Parametric f) =>
  Compose f Identity :~> f
rho_2 = coerce

class (Parametric f, Functor f) => Comonad f where
  extract   :: f :~> Identity
  duplicate :: f :~> (f `Compose` f)

data Equivalence x = x :=: x
infixl 4 :=:

-- Comonoid pentagon diagram
law1 :: Comonad f => Equivalence (f x -> Compose (Compose f f) f x)
law1 = lmapC duplicate . duplicate :=: alpha_1 . rmapC duplicate . duplicate

-- Comonoid unitor diagram
law2 :: Comonad f => Equivalence (f x -> Compose Identity f x)
law2 = lmapC extract . duplicate :=: lambda_1

law3 :: Comonad f => Equivalence (f x -> Compose f Identity x)
law3 = rmapC extract . duplicate :=: rho_1