{-# 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 :: f (f r) -> f r
multRep f (f r)
ffr = (Rep f -> r) -> f r
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 (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 (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 :: r -> f r
unitalRep = (Rep f -> r) -> f r
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 (f :: * -> *).
   Functor f =>
   (x -> f x) -> Complex x -> f (Complex x)
forall (t :: * -> *).
E t
-> forall x (f :: * -> *).
   Functor f =>
   (x -> f x) -> t x -> f (t 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 (f :: * -> *).
   Functor f =>
   (x -> f x) -> Complex x -> f (Complex x)
forall (t :: * -> *).
E t
-> forall x (f :: * -> *).
   Functor f =>
   (x -> f x) -> t x -> f (t 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 (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 (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 :: f r -> f (f r)
comultRep f r
fr = (Rep f -> f r) -> f (f r)
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 (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 (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 :: 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 (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 -> E V2 -> r
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 (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 -> E V3 -> r
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 (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 -> E V4 -> r
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 (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 (f :: * -> *).
   Functor f =>
   (x -> f x) -> Complex x -> f (Complex x)
forall (t :: * -> *).
E t
-> forall x (f :: * -> *).
   Functor f =>
   (x -> f x) -> t x -> f (t 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 (f :: * -> *).
   Functor f =>
   (x -> f x) -> Complex x -> f (Complex x)
forall (t :: * -> *).
E t
-> forall x (f :: * -> *).
   Functor f =>
   (x -> f x) -> t x -> f (t 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 -> E Quaternion -> r
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 (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)