{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, TypeOperators, UndecidableInstances, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Simplex
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-- The (augmented) simplex category.
-----------------------------------------------------------------------------
module Data.Category.Simplex (
  
  -- * Simplex Category
    Simplex(..)
  , Z, S
  , suc
  
  -- * Functor
  , Forget(..)
  , Fin(..)
  , Add(..)
  
  -- * The universal monoid
  , universalMonoid
  , Replicate(..)
        
) where
  
import Data.Category
import Data.Category.Product
import Data.Category.Functor
import Data.Category.Monoidal
import Data.Category.Limit


data Z
data S n


-- A Simplex x y structure plots a non-decreasing line, ending with Z
--
--   ^  +-----Z
--   |  |   XXY
--   y  |   Y |
--      |XXXY |
--      XY----+
--         x ->

data Simplex :: * -> * -> * where
  Z ::                    Simplex    Z     Z
  Y :: Simplex x    y  -> Simplex    x  (S y)
  X :: Simplex x (S y) -> Simplex (S x) (S y)

suc :: Obj Simplex n -> Obj Simplex (S n)
suc :: Obj Simplex n -> Obj Simplex (S n)
suc = Simplex n (S n) -> Obj Simplex (S n)
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex n (S n) -> Obj Simplex (S n))
-> (Obj Simplex n -> Simplex n (S n))
-> Obj Simplex n
-> Obj Simplex (S n)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj Simplex n -> Simplex n (S n)
forall x y. Simplex x y -> Simplex x (S y)
Y
-- Note: Objects are represented by their identity arrows,
-- which are in the shape of the elements of `iterate suc Z`.

-- | The (augmented) simplex category is the category of finite ordinals and order preserving maps.
instance Category Simplex where
  src :: Simplex a b -> Obj Simplex a
src Simplex a b
Z = Obj Simplex a
Simplex Z Z
Z
  src (Y Simplex a y
f) = Simplex a y -> Obj Simplex a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Simplex a y
f
  src (X Simplex x (S y)
f) = Obj Simplex x -> Obj Simplex (S x)
forall n. Obj Simplex n -> Obj Simplex (S n)
suc (Simplex x (S y) -> Obj Simplex x
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Simplex x (S y)
f)
  
  tgt :: Simplex a b -> Obj Simplex b
tgt Simplex a b
Z = Obj Simplex b
Simplex Z Z
Z
  tgt (Y Simplex a y
f) = Obj Simplex y -> Obj Simplex (S y)
forall n. Obj Simplex n -> Obj Simplex (S n)
suc (Simplex a y -> Obj Simplex y
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Simplex a y
f)
  tgt (X Simplex x (S y)
f) = Simplex x (S y) -> Obj Simplex (S y)
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Simplex x (S y)
f
  
  Simplex b c
Z   . :: Simplex b c -> Simplex a b -> Simplex a c
.   Simplex a b
f = Simplex a b
Simplex a c
f
  Simplex b c
f   .   Simplex a b
Z = Simplex b c
Simplex a c
f
  Y Simplex b y
f .   Simplex a b
g = Simplex a y -> Simplex a (S y)
forall x y. Simplex x y -> Simplex x (S y)
Y (Simplex b y
f Simplex b y -> Simplex a b -> Simplex a y
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Simplex a b
g)
  X Simplex x (S y)
f . Y Simplex a y
g = Simplex x (S y)
f Simplex x (S y) -> Simplex a x -> Simplex a (S y)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Simplex a x
Simplex a y
g
  X Simplex x (S y)
f . X Simplex x (S y)
g = Simplex x (S y) -> Simplex (S x) (S y)
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex x (S y) -> Simplex (S x) (S y)
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X Simplex x (S y)
f Simplex (S x) (S y) -> Simplex x (S x) -> Simplex x (S y)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Simplex x (S x)
Simplex x (S y)
g)


-- | The ordinal @0@ is the initial object of the simplex category.
instance HasInitialObject Simplex where
  type InitialObject Simplex = Z
  
  initialObject :: Obj Simplex (InitialObject Simplex)
initialObject = Obj Simplex (InitialObject Simplex)
Simplex Z Z
Z
  
  initialize :: Obj Simplex a -> Simplex (InitialObject Simplex) a
initialize Obj Simplex a
Z = Simplex (InitialObject Simplex) a
Simplex Z Z
Z
  initialize (X (Y Simplex x y
f)) = Simplex Z x -> Simplex Z (S x)
forall x y. Simplex x y -> Simplex x (S y)
Y (Obj Simplex x -> Simplex (InitialObject Simplex) x
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj Simplex x
Simplex x y
f)

-- | The ordinal @1@ is the terminal object of the simplex category.
instance HasTerminalObject Simplex where
  type TerminalObject Simplex = S Z

  terminalObject :: Obj Simplex (TerminalObject Simplex)
terminalObject = Simplex Z Z -> Obj Simplex (S Z)
forall n. Obj Simplex n -> Obj Simplex (S n)
suc Simplex Z Z
Z

  terminate :: Obj Simplex a -> Simplex a (TerminalObject Simplex)
terminate Obj Simplex a
Z = Simplex Z Z -> Simplex Z (S Z)
forall x y. Simplex x y -> Simplex x (S y)
Y Simplex Z Z
Z
  terminate (X (Y Simplex x y
f)) = Simplex x (S Z) -> Simplex (S x) (S Z)
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Obj Simplex x -> Simplex x (TerminalObject Simplex)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj Simplex x
Simplex x y
f)


data Fin :: * -> * where
  Fz ::          Fin (S n)
  Fs :: Fin n -> Fin (S n)

data Forget = Forget
-- | Turn @Simplex x y@ arrows into @Fin x -> Fin y@ functions.
instance Functor Forget where
  type Dom Forget = Simplex
  type Cod Forget = (->)
  type Forget :% n = Fin n
  Forget
Forget % :: Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b)
% Dom Forget a b
Z   = \Fin Z
x -> Fin Z
x
  Forget
Forget % Y f = \Fin a
x -> Fin y -> Fin (S y)
forall n. Fin n -> Fin (S n)
Fs ((Forget
Forget Forget -> Dom Forget a y -> Cod Forget (Forget :% a) (Forget :% y)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom Forget a y
Simplex a y
f) Fin a
x)
  Forget
Forget % X f = \Fin (S x)
x -> case Fin (S x)
x of
    Fin (S x)
Fz -> Fin (S y)
forall n. Fin (S n)
Fz
    Fs Fin n
n -> (Forget
Forget Forget
-> Dom Forget x (S y) -> Cod Forget (Forget :% x) (Forget :% S y)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom Forget x (S y)
Simplex x (S y)
f) Fin n
n


data Add = Add
-- | Ordinal addition is a bifuntor, it concattenates the maps as it were.
instance Functor Add where
  type Dom Add = Simplex :**: Simplex
  type Cod Add = Simplex
  type Add :% (Z  , n) = n
  type Add :% (S m, n) = S (Add :% (m, n))
  Add
Add % :: Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b)
% (Z   :**: g) = Cod Add (Add :% a) (Add :% b)
Simplex a2 b2
g
  Add
Add % (Y f :**: g) = Simplex (Add :% (a1, a2)) (Add :% (y, b2))
-> Simplex (Add :% (a1, a2)) (S (Add :% (y, b2)))
forall x y. Simplex x y -> Simplex x (S y)
Y (Add
Add Add
-> Dom Add (a1, a2) (y, b2)
-> Cod Add (Add :% (a1, a2)) (Add :% (y, b2))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Simplex a1 y
f Simplex a1 y
-> Simplex a2 b2 -> (:**:) Simplex Simplex (a1, a2) (y, b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Simplex a2 b2
g))
  Add
Add % (X f :**: g) = Simplex (Add :% (x, a2)) (S (Add :% (y, b2)))
-> Simplex (S (Add :% (x, a2))) (S (Add :% (y, b2)))
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Add
Add Add
-> Dom Add (x, a2) (S y, b2)
-> Cod Add (Add :% (x, a2)) (Add :% (S y, b2))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Simplex x (S y)
f Simplex x (S y)
-> Simplex a2 b2 -> (:**:) Simplex Simplex (x, a2) (S y, b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Simplex a2 b2
g))

-- | Ordinal addition makes the simplex category a monoidal category, with @0@ as unit.
instance TensorProduct Add where
  type Unit Add = Z
  unitObject :: Add -> Obj (Cod Add) (Unit Add)
unitObject Add
Add = Obj (Cod Add) (Unit Add)
Simplex Z Z
Z
  
  leftUnitor :: Add -> Obj k a -> k (Add :% (Unit Add, a)) a
leftUnitor     Add
Add       Obj k a
a   = Obj k a
k (Add :% (Unit Add, a)) a
a
  leftUnitorInv :: Add -> Obj k a -> k a (Add :% (Unit Add, a))
leftUnitorInv  Add
Add       Obj k a
a   = Obj k a
k a (Add :% (Unit Add, a))
a
  rightUnitor :: Add -> Obj k a -> k (Add :% (a, Unit Add)) a
rightUnitor    Add
Add       Obj k a
Z   = k (Add :% (a, Unit Add)) a
Simplex Z Z
Z
  rightUnitor    Add
Add (X (Y n)) = Simplex (Add :% (y, Z)) (S x) -> Simplex (S (Add :% (y, Z))) (S x)
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex (Add :% (y, Z)) x -> Simplex (Add :% (y, Z)) (S x)
forall x y. Simplex x y -> Simplex x (S y)
Y (Add -> Obj Simplex x -> Simplex (Add :% (x, Unit Add)) x
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (a, Unit f)) a
rightUnitor Add
Add Obj Simplex x
Simplex x y
n))
  rightUnitorInv :: Add -> Obj k a -> k a (Add :% (a, Unit Add))
rightUnitorInv Add
Add       Obj k a
Z   = k a (Add :% (a, Unit Add))
Simplex Z Z
Z
  rightUnitorInv Add
Add (X (Y n)) = Simplex x (S (Add :% (y, Z))) -> Simplex (S x) (S (Add :% (y, Z)))
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex x (Add :% (y, Z)) -> Simplex x (S (Add :% (y, Z)))
forall x y. Simplex x y -> Simplex x (S y)
Y (Add -> Obj Simplex x -> Simplex x (Add :% (x, Unit Add))
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (a, Unit f))
rightUnitorInv Add
Add Obj Simplex x
Simplex x y
n))
  associator :: Add
-> Obj k a
-> Obj k b
-> Obj k c
-> k (Add :% (Add :% (a, b), c)) (Add :% (a, Add :% (b, c)))
associator     Add
Add Obj k a
Z       Obj k b
Z   Obj k c
n = Obj k c
k (Add :% (Add :% (a, b), c)) (Add :% (a, Add :% (b, c)))
n
  associator     Add
Add Obj k a
Z (X (Y m)) Obj k c
n = Simplex (Add :% (y, c)) (S (Add :% (y, c)))
-> Simplex (S (Add :% (y, c))) (S (Add :% (y, c)))
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex (Add :% (y, c)) (Add :% (y, c))
-> Simplex (Add :% (y, c)) (S (Add :% (y, c)))
forall x y. Simplex x y -> Simplex x (S y)
Y (Add
-> Simplex Z Z
-> Obj Simplex x
-> Obj Simplex c
-> Simplex (Add :% (Add :% (Z, x), c)) (Add :% (Z, Add :% (x, c)))
forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c)))
associator Add
Add Simplex Z Z
Z Obj Simplex x
Simplex x y
m Obj k c
Obj Simplex c
n))
  associator     Add
Add (X (Y l)) Obj k b
m Obj k c
n = Simplex (Add :% (Add :% (y, b), c)) (S (Add :% (y, Add :% (b, c))))
-> Simplex
     (S (Add :% (Add :% (y, b), c))) (S (Add :% (y, Add :% (b, c))))
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex (Add :% (Add :% (y, b), c)) (Add :% (y, Add :% (b, c)))
-> Simplex
     (Add :% (Add :% (y, b), c)) (S (Add :% (y, Add :% (b, c))))
forall x y. Simplex x y -> Simplex x (S y)
Y (Add
-> Obj Simplex x
-> Obj Simplex b
-> Obj Simplex c
-> Simplex (Add :% (Add :% (x, b), c)) (Add :% (x, Add :% (b, c)))
forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c)))
associator Add
Add Obj Simplex x
Simplex x y
l Obj k b
Obj Simplex b
m Obj k c
Obj Simplex c
n))
  associatorInv :: Add
-> Obj k a
-> Obj k b
-> Obj k c
-> k (Add :% (a, Add :% (b, c))) (Add :% (Add :% (a, b), c))
associatorInv  Add
Add Obj k a
Z       Obj k b
Z   Obj k c
n = Obj k c
k (Add :% (a, Add :% (b, c))) (Add :% (Add :% (a, b), c))
n
  associatorInv  Add
Add Obj k a
Z (X (Y m)) Obj k c
n = Simplex (Add :% (y, c)) (S (Add :% (y, c)))
-> Simplex (S (Add :% (y, c))) (S (Add :% (y, c)))
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex (Add :% (y, c)) (Add :% (y, c))
-> Simplex (Add :% (y, c)) (S (Add :% (y, c)))
forall x y. Simplex x y -> Simplex x (S y)
Y (Add
-> Simplex Z Z
-> Obj Simplex x
-> Obj Simplex c
-> Simplex (Add :% (Z, Add :% (x, c))) (Add :% (Add :% (Z, x), c))
forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c))
associatorInv Add
Add Simplex Z Z
Z Obj Simplex x
Simplex x y
m Obj k c
Obj Simplex c
n))
  associatorInv  Add
Add (X (Y l)) Obj k b
m Obj k c
n = Simplex (Add :% (y, Add :% (b, c))) (S (Add :% (Add :% (y, b), c)))
-> Simplex
     (S (Add :% (y, Add :% (b, c)))) (S (Add :% (Add :% (y, b), c)))
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex (Add :% (y, Add :% (b, c))) (Add :% (Add :% (y, b), c))
-> Simplex
     (Add :% (y, Add :% (b, c))) (S (Add :% (Add :% (y, b), c)))
forall x y. Simplex x y -> Simplex x (S y)
Y (Add
-> Obj Simplex x
-> Obj Simplex b
-> Obj Simplex c
-> Simplex (Add :% (x, Add :% (b, c))) (Add :% (Add :% (x, b), c))
forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c))
associatorInv Add
Add Obj Simplex x
Simplex x y
l Obj k b
Obj Simplex b
m Obj k c
Obj Simplex c
n))


-- | The maps @0 -> 1@ and @2 -> 1@ form a monoid, which is universal, c.f. `Replicate`.
universalMonoid :: MonoidObject Add (S Z)
universalMonoid :: MonoidObject Add (S Z)
universalMonoid = MonoidObject :: forall f a.
Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
MonoidObject { unit :: Cod Add (Unit Add) (S Z)
unit = Simplex Z Z -> Simplex Z (S Z)
forall x y. Simplex x y -> Simplex x (S y)
Y Simplex Z Z
Z, multiply :: Cod Add (Add :% (S Z, S Z)) (S Z)
multiply = Obj Simplex (S Z) -> Simplex (S (S Z)) (S Z)
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex Z (S Z) -> Obj Simplex (S Z)
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex Z Z -> Simplex Z (S Z)
forall x y. Simplex x y -> Simplex x (S y)
Y Simplex Z Z
Z)) }

data Replicate f a = Replicate f (MonoidObject f a)
-- | Replicate a monoid a number of times.
instance TensorProduct f => Functor (Replicate f a) where
  type Dom (Replicate f a) = Simplex
  type Cod (Replicate f a) = Cod f
  type Replicate f a :% Z = Unit f
  type Replicate f a :% S n = f :% (a, Replicate f a :% n)
  Replicate f
f MonoidObject f a
_ % :: Replicate f a
-> Dom (Replicate f a) a b
-> Cod (Replicate f a) (Replicate f a :% a) (Replicate f a :% b)
% Dom (Replicate f a) a b
Z = f -> Obj (Cod f) (Unit f)
forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject f
f
  Replicate f
f MonoidObject f a
m % Y n = f
f f
-> Dom f (Unit f, Replicate f a :% y) (a, Replicate f a :% y)
-> Cod
     f
     (f :% (Unit f, Replicate f a :% y))
     (f :% (a, Replicate f a :% y))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (MonoidObject f a -> Cod f (Unit f) a
forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject f a
m Cod f (Unit f) a
-> Cod f (Replicate f a :% y) (Replicate f a :% y)
-> (:**:)
     (Cod f)
     (Cod f)
     (Unit f, Replicate f a :% y)
     (a, Replicate f a :% y)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Cod f (Replicate f a :% a) (Replicate f a :% y)
-> Cod f (Replicate f a :% y) (Replicate f a :% y)
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Cod f (Replicate f a :% a) (Replicate f a :% y)
Cod (Replicate f a) (Replicate f a :% a) (Replicate f a :% y)
n') Cod
  f
  (f :% (Unit f, Replicate f a :% y))
  (f :% (a, Replicate f a :% y))
-> Cod f (Replicate f a :% a) (f :% (Unit f, Replicate f a :% y))
-> Cod f (Replicate f a :% a) (f :% (a, Replicate f a :% y))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. f
-> Cod f (Replicate f a :% y) (Replicate f a :% y)
-> Cod f (Replicate f a :% y) (f :% (Unit f, Replicate f a :% y))
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (Unit f, a))
leftUnitorInv f
f (Cod f (Replicate f a :% a) (Replicate f a :% y)
-> Cod f (Replicate f a :% y) (Replicate f a :% y)
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Cod f (Replicate f a :% a) (Replicate f a :% y)
Cod (Replicate f a) (Replicate f a :% a) (Replicate f a :% y)
n') Cod f (Replicate f a :% y) (f :% (Unit f, Replicate f a :% y))
-> Cod f (Replicate f a :% a) (Replicate f a :% y)
-> Cod f (Replicate f a :% a) (f :% (Unit f, Replicate f a :% y))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cod f (Replicate f a :% a) (Replicate f a :% y)
Cod (Replicate f a) (Replicate f a :% a) (Replicate f a :% y)
n' where n' :: Cod (Replicate f a) (Replicate f a :% a) (Replicate f a :% y)
n' = f -> MonoidObject f a -> Replicate f a
forall f a. f -> MonoidObject f a -> Replicate f a
Replicate f
f MonoidObject f a
m Replicate f a
-> Dom (Replicate f a) a y
-> Cod (Replicate f a) (Replicate f a :% a) (Replicate f a :% y)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom (Replicate f a) a y
Simplex a y
n
  Replicate f
f MonoidObject f a
m % X (Y n) = f
f f
-> Dom f (a, Replicate f a :% x) (a, Replicate f a :% y)
-> Cod
     f (f :% (a, Replicate f a :% x)) (f :% (a, Replicate f a :% y))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cod f (Unit f) a -> Obj (Cod f) a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt (MonoidObject f a -> Cod f (Unit f) a
forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject f a
m) Obj (Cod f) a
-> Cod f (Replicate f a :% x) (Replicate f a :% y)
-> (:**:)
     (Cod f) (Cod f) (a, Replicate f a :% x) (a, Replicate f a :% y)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (f -> MonoidObject f a -> Replicate f a
forall f a. f -> MonoidObject f a -> Replicate f a
Replicate f
f MonoidObject f a
m Replicate f a
-> Dom (Replicate f a) x y
-> Cod (Replicate f a) (Replicate f a :% x) (Replicate f a :% y)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom (Replicate f a) x y
Simplex x y
n))
  Replicate f
f MonoidObject f a
m % X (X n) = Cod f (f :% (a, Replicate f a :% x)) (f :% (a, Replicate f a :% y))
Cod (Replicate f a) (Replicate f a :% S x) (Replicate f a :% S y)
n' Cod f (f :% (a, Replicate f a :% x)) (f :% (a, Replicate f a :% y))
-> Cod
     f
     (f :% (a, f :% (a, Replicate f a :% x)))
     (f :% (a, Replicate f a :% x))
-> Cod
     f
     (f :% (a, f :% (a, Replicate f a :% x)))
     (f :% (a, Replicate f a :% y))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (f
f f
-> Dom f (f :% (a, a), Replicate f a :% x) (a, Replicate f a :% x)
-> Cod
     f
     (f :% (f :% (a, a), Replicate f a :% x))
     (f :% (a, Replicate f a :% x))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (MonoidObject f a -> Cod f (f :% (a, a)) a
forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
multiply MonoidObject f a
m Cod f (f :% (a, a)) a
-> Cod f (Replicate f a :% x) (Replicate f a :% x)
-> (:**:)
     (Cod f)
     (Cod f)
     (f :% (a, a), Replicate f a :% x)
     (a, Replicate f a :% x)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Cod f (Replicate f a :% x) (Replicate f a :% x)
b)) Cod
  f
  (f :% (f :% (a, a), Replicate f a :% x))
  (f :% (a, Replicate f a :% x))
-> Cod
     f
     (f :% (a, f :% (a, Replicate f a :% x)))
     (f :% (f :% (a, a), Replicate f a :% x))
-> Cod
     f
     (f :% (a, f :% (a, Replicate f a :% x)))
     (f :% (a, Replicate f a :% x))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. f
-> Obj (Cod f) a
-> Obj (Cod f) a
-> Cod f (Replicate f a :% x) (Replicate f a :% x)
-> Cod
     f
     (f :% (a, f :% (a, Replicate f a :% x)))
     (f :% (f :% (a, a), Replicate f a :% x))
forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c))
associatorInv f
f Obj (Cod f) a
a Obj (Cod f) a
a Cod f (Replicate f a :% x) (Replicate f a :% x)
b
    where
      n' :: Cod (Replicate f a) (Replicate f a :% S x) (Replicate f a :% S y)
n' = f -> MonoidObject f a -> Replicate f a
forall f a. f -> MonoidObject f a -> Replicate f a
Replicate f
f MonoidObject f a
m Replicate f a
-> Dom (Replicate f a) (S x) (S y)
-> Cod
     (Replicate f a) (Replicate f a :% S x) (Replicate f a :% S y)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Simplex x (S y) -> Simplex (S x) (S y)
forall x y. Simplex x (S y) -> Simplex (S x) (S y)
X Simplex x (S y)
n
      a :: Obj (Cod f) a
a = Cod f (Unit f) a -> Obj (Cod f) a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt (MonoidObject f a -> Cod f (Unit f) a
forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject f a
m)
      b :: Cod f (Replicate f a :% x) (Replicate f a :% x)
b = Cod f (Replicate f a :% x) (f :% (a, Replicate f a :% y))
-> Cod f (Replicate f a :% x) (Replicate f a :% x)
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src (f -> MonoidObject f a -> Replicate f a
forall f a. f -> MonoidObject f a -> Replicate f a
Replicate f
f MonoidObject f a
m Replicate f a
-> Dom (Replicate f a) x (S y)
-> Cod (Replicate f a) (Replicate f a :% x) (Replicate f a :% S y)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom (Replicate f a) x (S y)
Simplex x (S y)
n)