    {-# LANGUAGE CPP #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    -----------------------------------------------------------------------------

    -- |

    -- License     :  BSD-style (see the file LICENSE)

    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>

    -- Stability   :  provisional

    -- Portability :  portable

    --

    -----------------------------------------------------------------------------

    module Linear.Algebra
      ( Algebra(..)
      , Coalgebra(..)
      , multRep, unitalRep
      , comultRep, counitalRep
      ) where

    import Control.Lens hiding (index)
    import Data.Functor.Rep
    import Data.Complex
    import Data.Void
    import Linear.Vector
    import Linear.Quaternion
    import Linear.Conjugate
    import Linear.V0
    import Linear.V1
    import Linear.V2
    import Linear.V3
    import Linear.V4

    -- | An associative unital algebra over a ring

    class Num r => Algebra r m where
      mult :: (m -> m -> r) -> m -> r
      unital :: r -> m -> r

    multRep :: (Representable f, Algebra r (Rep f)) => f (f r) -> f r
    multRep :: forall (f :: * -> *) r.
    (Representable f, Algebra r (Rep f)) =>
    f (f r) -> f r
    multRep f (f r)
    ffr = (Rep f -> r) -> f r
    forall a. (Rep f -> a) -> f a
    forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
    tabulate ((Rep f -> r) -> f r) -> (Rep f -> r) -> f r
    forall a b. (a -> b) -> a -> b
    $ (Rep f -> Rep f -> r) -> Rep f -> r
    forall r m. Algebra r m => (m -> m -> r) -> m -> r
    mult (f r -> Rep f -> r
    forall a. f a -> Rep f -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index (f r -> Rep f -> r) -> (Rep f -> f r) -> Rep f -> Rep f -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f (f r) -> Rep f -> f r
    forall a. f a -> Rep f -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index f (f r)
    ffr)

    unitalRep :: (Representable f, Algebra r (Rep f)) => r -> f r
    unitalRep :: forall (f :: * -> *) r.
    (Representable f, Algebra r (Rep f)) =>
    r -> f r
    unitalRep = (Rep f -> r) -> f r
    forall a. (Rep f -> a) -> f a
    forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
    tabulate ((Rep f -> r) -> f r) -> (r -> Rep f -> r) -> r -> f r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . r -> Rep f -> r
    forall r m. Algebra r m => r -> m -> r
    unital

    instance Num r => Algebra r Void where
      mult :: (Void -> Void -> r) -> Void -> r
    mult Void -> Void -> r
    _ Void
    _ = r
    0
      unital :: r -> Void -> r
    unital r
    _ Void
    _ = r
    0

    instance Num r => Algebra r (E V0) where
      mult :: (E V0 -> E V0 -> r) -> E V0 -> r
    mult E V0 -> E V0 -> r
    _ E V0
    _ = r
    0
      unital :: r -> E V0 -> r
    unital r
    _ E V0
    _ = r
    0

    instance Num r => Algebra r (E V1) where
      mult :: (E V1 -> E V1 -> r) -> E V1 -> r
    mult E V1 -> E V1 -> r
    f E V1
    _ = E V1 -> E V1 -> r
    f E V1
    forall (t :: * -> *). R1 t => E t
    ex E V1
    forall (t :: * -> *). R1 t => E t
    ex
      unital :: r -> E V1 -> r
    unital r
    r E V1
    _ = r
    r

    instance Num r => Algebra r () where
      mult :: (() -> () -> r) -> () -> r
    mult () -> () -> r
    f () = () -> () -> r
    f () ()
      unital :: r -> () -> r
    unital r
    r () = r
    r

    instance (Algebra r a, Algebra r b) => Algebra r (a, b) where
      mult :: ((a, b) -> (a, b) -> r) -> (a, b) -> r
    mult (a, b) -> (a, b) -> r
    f (a
    a,b
    b) = (a -> a -> r) -> a -> r
    forall r m. Algebra r m => (m -> m -> r) -> m -> r
    mult (\a
    a1 a
    a2 -> (b -> b -> r) -> b -> r
    forall r m. Algebra r m => (m -> m -> r) -> m -> r
    mult (\b
    b1 b
    b2 -> (a, b) -> (a, b) -> r
    f (a
    a1,b
    b1) (a
    a2,b
    b2)) b
    b) a
    a
      unital :: r -> (a, b) -> r
    unital r
    r (a
    a,b
    b) = r -> a -> r
    forall r m. Algebra r m => r -> m -> r
    unital r
    r a
    a r -> r -> r
    forall a. Num a => a -> a -> a
    * r -> b -> r
    forall r m. Algebra r m => r -> m -> r
    unital r
    r b
    b

    instance Num r => Algebra r (E Complex) where
      mult :: (E Complex -> E Complex -> r) -> E Complex -> r
    mult E Complex -> E Complex -> r
    f = \ E Complex
    i -> Complex r
    cComplex r -> Getting r (Complex r) r -> r
    forall s a. s -> Getting a s a -> a
    ^.E Complex -> forall x. Lens' (Complex x) x
    forall (t :: * -> *). E t -> forall x. Lens' (t x) x
    el E Complex
    i where
       c :: Complex r
    c = (E Complex -> E Complex -> r
    f E Complex
    forall (t :: * -> *). Complicated t => E t
    ee E Complex
    forall (t :: * -> *). Complicated t => E t
    ee r -> r -> r
    forall a. Num a => a -> a -> a
    - E Complex -> E Complex -> r
    f E Complex
    forall (t :: * -> *). Complicated t => E t
    ei E Complex
    forall (t :: * -> *). Complicated t => E t
    ei) r -> r -> Complex r
    forall a. a -> a -> Complex a
    :+ (E Complex -> E Complex -> r
    f E Complex
    forall (t :: * -> *). Complicated t => E t
    ee E Complex
    forall (t :: * -> *). Complicated t => E t
    ei r -> r -> r
    forall a. Num a => a -> a -> a
    + E Complex -> E Complex -> r
    f E Complex
    forall (t :: * -> *). Complicated t => E t
    ei E Complex
    forall (t :: * -> *). Complicated t => E t
    ee)
      unital :: r -> E Complex -> r
    unital r
    r E Complex
    i = (r
    r r -> r -> Complex r
    forall a. a -> a -> Complex a
    :+ r
    0)Complex r -> Getting r (Complex r) r -> r
    forall s a. s -> Getting a s a -> a
    ^.E Complex -> forall x. Lens' (Complex x) x
    forall (t :: * -> *). E t -> forall x. Lens' (t x) x
    el E Complex
    i

    instance (Num r, TrivialConjugate r) => Algebra r (E Quaternion) where
      mult :: (E Quaternion -> E Quaternion -> r) -> E Quaternion -> r
    mult E Quaternion -> E Quaternion -> r
    f = Quaternion r -> Rep Quaternion -> r
    forall a. Quaternion a -> Rep Quaternion -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index (Quaternion r -> Rep Quaternion -> r)
    -> Quaternion r -> Rep Quaternion -> r
    forall a b. (a -> b) -> a -> b
    $ r -> V3 r -> Quaternion r
    forall a. a -> V3 a -> Quaternion a
    Quaternion
        (E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ee E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ee r -> r -> r
    forall a. Num a => a -> a -> a
    - (E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ei E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ei r -> r -> r
    forall a. Num a => a -> a -> a
    + E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ej E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ej r -> r -> r
    forall a. Num a => a -> a -> a
    + E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ek E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ek))
        (r -> r -> r -> V3 r
    forall a. a -> a -> a -> V3 a
    V3 (E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ee E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ei r -> r -> r
    forall a. Num a => a -> a -> a
    + E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ei E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ee r -> r -> r
    forall a. Num a => a -> a -> a
    + E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ej E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ek r -> r -> r
    forall a. Num a => a -> a -> a
    - E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ek E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ej)
            (E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ee E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ej r -> r -> r
    forall a. Num a => a -> a -> a
    + E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ej E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ee r -> r -> r
    forall a. Num a => a -> a -> a
    + E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ek E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ei r -> r -> r
    forall a. Num a => a -> a -> a
    - E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ei E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ek)
            (E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ee E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ek r -> r -> r
    forall a. Num a => a -> a -> a
    + E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ek E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ee r -> r -> r
    forall a. Num a => a -> a -> a
    + E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ei E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ej r -> r -> r
    forall a. Num a => a -> a -> a
    - E Quaternion -> E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ej E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ei))
      unital :: r -> E Quaternion -> r
    unital r
    r = Quaternion r -> Rep Quaternion -> r
    forall a. Quaternion a -> Rep Quaternion -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index (r -> V3 r -> Quaternion r
    forall a. a -> V3 a -> Quaternion a
    Quaternion r
    r V3 r
    0)

    -- | A coassociative counital coalgebra over a ring

    class Num r => Coalgebra r m where
      comult :: (m -> r) -> m -> m -> r
      counital :: (m -> r) -> r

    comultRep :: (Representable f, Coalgebra r (Rep f)) => f r -> f (f r)
    comultRep :: forall (f :: * -> *) r.
    (Representable f, Coalgebra r (Rep f)) =>
    f r -> f (f r)
    comultRep f r
    fr = (Rep f -> f r) -> f (f r)
    forall a. (Rep f -> a) -> f a
    forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
    tabulate ((Rep f -> f r) -> f (f r)) -> (Rep f -> f r) -> f (f r)
    forall a b. (a -> b) -> a -> b
    $ \Rep f
    i -> (Rep f -> r) -> f r
    forall a. (Rep f -> a) -> f a
    forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
    tabulate ((Rep f -> r) -> f r) -> (Rep f -> r) -> f r
    forall a b. (a -> b) -> a -> b
    $ \Rep f
    j -> (Rep f -> r) -> Rep f -> Rep f -> r
    forall r m. Coalgebra r m => (m -> r) -> m -> m -> r
    comult (f r -> Rep f -> r
    forall a. f a -> Rep f -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index f r
    fr) Rep f
    i Rep f
    j

    counitalRep :: (Representable f, Coalgebra r (Rep f)) => f r -> r
    counitalRep :: forall (f :: * -> *) r.
    (Representable f, Coalgebra r (Rep f)) =>
    f r -> r
    counitalRep = (Rep f -> r) -> r
    forall r m. Coalgebra r m => (m -> r) -> r
    counital ((Rep f -> r) -> r) -> (f r -> Rep f -> r) -> f r -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f r -> Rep f -> r
    forall a. f a -> Rep f -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index

    instance Num r => Coalgebra r Void where
      comult :: (Void -> r) -> Void -> Void -> r
    comult Void -> r
    _ Void
    _ Void
    _ = r
    0
      counital :: (Void -> r) -> r
    counital Void -> r
    _ = r
    0

    instance Num r => Coalgebra r () where
      comult :: (() -> r) -> () -> () -> r
    comult () -> r
    f () () = () -> r
    f ()
      counital :: (() -> r) -> r
    counital () -> r
    f = () -> r
    f ()

    instance Num r => Coalgebra r (E V0) where
      comult :: (E V0 -> r) -> E V0 -> E V0 -> r
    comult E V0 -> r
    _ E V0
    _ E V0
    _ = r
    0
      counital :: (E V0 -> r) -> r
    counital E V0 -> r
    _ = r
    0

    instance Num r => Coalgebra r (E V1) where
      comult :: (E V1 -> r) -> E V1 -> E V1 -> r
    comult E V1 -> r
    f E V1
    _ E V1
    _ = E V1 -> r
    f E V1
    forall (t :: * -> *). R1 t => E t
    ex
      counital :: (E V1 -> r) -> r
    counital E V1 -> r
    f = E V1 -> r
    f E V1
    forall (t :: * -> *). R1 t => E t
    ex

    instance Num r => Coalgebra r (E V2) where
      comult :: (E V2 -> r) -> E V2 -> E V2 -> r
    comult E V2 -> r
    f = V2 r -> Rep V2 -> r
    V2 r -> E V2 -> r
    forall a. V2 a -> Rep V2 -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index (V2 r -> E V2 -> r) -> (E V2 -> V2 r) -> E V2 -> E V2 -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . V2 (V2 r) -> Rep V2 -> V2 r
    forall a. V2 a -> Rep V2 -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index V2 (V2 r)
    v where
        v :: V2 (V2 r)
    v = V2 r -> V2 r -> V2 (V2 r)
    forall a. a -> a -> V2 a
    V2 (r -> r -> V2 r
    forall a. a -> a -> V2 a
    V2 (E V2 -> r
    f E V2
    forall (t :: * -> *). R1 t => E t
    ex) r
    0) (r -> r -> V2 r
    forall a. a -> a -> V2 a
    V2 r
    0 (E V2 -> r
    f E V2
    forall (t :: * -> *). R2 t => E t
    ey))
      counital :: (E V2 -> r) -> r
    counital E V2 -> r
    f = E V2 -> r
    f E V2
    forall (t :: * -> *). R1 t => E t
    ex r -> r -> r
    forall a. Num a => a -> a -> a
    + E V2 -> r
    f E V2
    forall (t :: * -> *). R2 t => E t
    ey

    instance Num r => Coalgebra r (E V3) where
      comult :: (E V3 -> r) -> E V3 -> E V3 -> r
    comult E V3 -> r
    f = V3 r -> Rep V3 -> r
    V3 r -> E V3 -> r
    forall a. V3 a -> Rep V3 -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index (V3 r -> E V3 -> r) -> (E V3 -> V3 r) -> E V3 -> E V3 -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . V3 (V3 r) -> Rep V3 -> V3 r
    forall a. V3 a -> Rep V3 -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index V3 (V3 r)
    q where
        q :: V3 (V3 r)
    q = V3 r -> V3 r -> V3 r -> V3 (V3 r)
    forall a. a -> a -> a -> V3 a
    V3 (r -> r -> r -> V3 r
    forall a. a -> a -> a -> V3 a
    V3 (E V3 -> r
    f E V3
    forall (t :: * -> *). R1 t => E t
    ex) r
    0 r
    0)
               (r -> r -> r -> V3 r
    forall a. a -> a -> a -> V3 a
    V3 r
    0 (E V3 -> r
    f E V3
    forall (t :: * -> *). R2 t => E t
    ey) r
    0)
               (r -> r -> r -> V3 r
    forall a. a -> a -> a -> V3 a
    V3 r
    0 r
    0 (E V3 -> r
    f E V3
    forall (t :: * -> *). R3 t => E t
    ez))
      counital :: (E V3 -> r) -> r
    counital E V3 -> r
    f = E V3 -> r
    f E V3
    forall (t :: * -> *). R1 t => E t
    ex r -> r -> r
    forall a. Num a => a -> a -> a
    + E V3 -> r
    f E V3
    forall (t :: * -> *). R2 t => E t
    ey r -> r -> r
    forall a. Num a => a -> a -> a
    + E V3 -> r
    f E V3
    forall (t :: * -> *). R3 t => E t
    ez

    instance Num r => Coalgebra r (E V4) where
      comult :: (E V4 -> r) -> E V4 -> E V4 -> r
    comult E V4 -> r
    f = V4 r -> Rep V4 -> r
    V4 r -> E V4 -> r
    forall a. V4 a -> Rep V4 -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index (V4 r -> E V4 -> r) -> (E V4 -> V4 r) -> E V4 -> E V4 -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . V4 (V4 r) -> Rep V4 -> V4 r
    forall a. V4 a -> Rep V4 -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index V4 (V4 r)
    v where
        v :: V4 (V4 r)
    v = V4 r -> V4 r -> V4 r -> V4 r -> V4 (V4 r)
    forall a. a -> a -> a -> a -> V4 a
    V4 (r -> r -> r -> r -> V4 r
    forall a. a -> a -> a -> a -> V4 a
    V4 (E V4 -> r
    f E V4
    forall (t :: * -> *). R1 t => E t
    ex) r
    0 r
    0 r
    0) (r -> r -> r -> r -> V4 r
    forall a. a -> a -> a -> a -> V4 a
    V4 r
    0 (E V4 -> r
    f E V4
    forall (t :: * -> *). R2 t => E t
    ey) r
    0 r
    0) (r -> r -> r -> r -> V4 r
    forall a. a -> a -> a -> a -> V4 a
    V4 r
    0 r
    0 (E V4 -> r
    f E V4
    forall (t :: * -> *). R3 t => E t
    ez) r
    0) (r -> r -> r -> r -> V4 r
    forall a. a -> a -> a -> a -> V4 a
    V4 r
    0 r
    0 r
    0 (E V4 -> r
    f E V4
    forall (t :: * -> *). R4 t => E t
    ew))
      counital :: (E V4 -> r) -> r
    counital E V4 -> r
    f = E V4 -> r
    f E V4
    forall (t :: * -> *). R1 t => E t
    ex r -> r -> r
    forall a. Num a => a -> a -> a
    + E V4 -> r
    f E V4
    forall (t :: * -> *). R2 t => E t
    ey r -> r -> r
    forall a. Num a => a -> a -> a
    + E V4 -> r
    f E V4
    forall (t :: * -> *). R3 t => E t
    ez r -> r -> r
    forall a. Num a => a -> a -> a
    + E V4 -> r
    f E V4
    forall (t :: * -> *). R4 t => E t
    ew

    instance Num r => Coalgebra r (E Complex) where
      comult :: (E Complex -> r) -> E Complex -> E Complex -> r
    comult E Complex -> r
    f = \E Complex
    i E Complex
    j -> Complex (Complex r)
    cComplex (Complex r) -> Getting r (Complex (Complex r)) r -> r
    forall s a. s -> Getting a s a -> a
    ^.E Complex -> forall x. Lens' (Complex x) x
    forall (t :: * -> *). E t -> forall x. Lens' (t x) x
    el E Complex
    i((Complex r -> Const r (Complex r))
     -> Complex (Complex r) -> Const r (Complex (Complex r)))
    -> ((r -> Const r r) -> Complex r -> Const r (Complex r))
    -> Getting r (Complex (Complex r)) r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .E Complex -> forall x. Lens' (Complex x) x
    forall (t :: * -> *). E t -> forall x. Lens' (t x) x
    el E Complex
    j where
        c :: Complex (Complex r)
    c = (E Complex -> r
    f E Complex
    forall (t :: * -> *). Complicated t => E t
    ee r -> r -> Complex r
    forall a. a -> a -> Complex a
    :+ r
    0) Complex r -> Complex r -> Complex (Complex r)
    forall a. a -> a -> Complex a
    :+ (r
    0 r -> r -> Complex r
    forall a. a -> a -> Complex a
    :+ E Complex -> r
    f E Complex
    forall (t :: * -> *). Complicated t => E t
    ei)
      counital :: (E Complex -> r) -> r
    counital E Complex -> r
    f = E Complex -> r
    f E Complex
    forall (t :: * -> *). Complicated t => E t
    ee r -> r -> r
    forall a. Num a => a -> a -> a
    + E Complex -> r
    f E Complex
    forall (t :: * -> *). Complicated t => E t
    ei

    instance (Num r, TrivialConjugate r) => Coalgebra r (E Quaternion) where
      comult :: (E Quaternion -> r) -> E Quaternion -> E Quaternion -> r
    comult E Quaternion -> r
    f = Quaternion r -> Rep Quaternion -> r
    Quaternion r -> E Quaternion -> r
    forall a. Quaternion a -> Rep Quaternion -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index (Quaternion r -> E Quaternion -> r)
    -> (E Quaternion -> Quaternion r)
    -> E Quaternion
    -> E Quaternion
    -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Quaternion (Quaternion r) -> Rep Quaternion -> Quaternion r
    forall a. Quaternion a -> Rep Quaternion -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index
        (Quaternion r -> V3 (Quaternion r) -> Quaternion (Quaternion r)
    forall a. a -> V3 a -> Quaternion a
    Quaternion (r -> V3 r -> Quaternion r
    forall a. a -> V3 a -> Quaternion a
    Quaternion (E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ee) (r -> r -> r -> V3 r
    forall a. a -> a -> a -> V3 a
    V3 r
    0 r
    0 r
    0))
                (Quaternion r -> Quaternion r -> Quaternion r -> V3 (Quaternion r)
    forall a. a -> a -> a -> V3 a
    V3 (r -> V3 r -> Quaternion r
    forall a. a -> V3 a -> Quaternion a
    Quaternion r
    0 (r -> r -> r -> V3 r
    forall a. a -> a -> a -> V3 a
    V3 (E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ei) r
    0 r
    0))
                    (r -> V3 r -> Quaternion r
    forall a. a -> V3 a -> Quaternion a
    Quaternion r
    0 (r -> r -> r -> V3 r
    forall a. a -> a -> a -> V3 a
    V3 r
    0 (E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ej) r
    0))
                    (r -> V3 r -> Quaternion r
    forall a. a -> V3 a -> Quaternion a
    Quaternion r
    0 (r -> r -> r -> V3 r
    forall a. a -> a -> a -> V3 a
    V3 r
    0 r
    0 (E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ek)))))
      counital :: (E Quaternion -> r) -> r
    counital E Quaternion -> r
    f = E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ee r -> r -> r
    forall a. Num a => a -> a -> a
    + E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Complicated t => E t
    ei r -> r -> r
    forall a. Num a => a -> a -> a
    + E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ej r -> r -> r
    forall a. Num a => a -> a -> a
    + E Quaternion -> r
    f E Quaternion
    forall (t :: * -> *). Hamiltonian t => E t
    ek

    instance (Coalgebra r m, Coalgebra r n) => Coalgebra r (m, n) where
      comult :: ((m, n) -> r) -> (m, n) -> (m, n) -> r
    comult (m, n) -> r
    f (m
    a1, n
    b1) (m
    a2, n
    b2) = (m -> r) -> m -> m -> r
    forall r m. Coalgebra r m => (m -> r) -> m -> m -> r
    comult (\m
    a -> (n -> r) -> n -> n -> r
    forall r m. Coalgebra r m => (m -> r) -> m -> m -> r
    comult (\n
    b -> (m, n) -> r
    f (m
    a, n
    b)) n
    b1 n
    b2) m
    a1 m
    a2
      counital :: ((m, n) -> r) -> r
    counital (m, n) -> r
    k = (m -> r) -> r
    forall r m. Coalgebra r m => (m -> r) -> r
    counital ((m -> r) -> r) -> (m -> r) -> r
    forall a b. (a -> b) -> a -> b
    $ \m
    a -> (n -> r) -> r
    forall r m. Coalgebra r m => (m -> r) -> r
    counital ((n -> r) -> r) -> (n -> r) -> r
    forall a b. (a -> b) -> a -> b
    $ \n
    b -> (m, n) -> r
    k (m
    a,n
    b)