{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, TypeOperators, UndecidableInstances, LambdaCase, FlexibleContexts, 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.Kind (Type)

import Data.Category
import Data.Category.Product
import Data.Category.Functor
import Data.Category.NaturalTransformation
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 :: Type -> Type -> Type 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 :: forall n. Obj Simplex n -> Obj Simplex (S n)
suc = forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall x a1. Simplex x a1 -> Simplex x (S a1)
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 :: forall a b. Simplex a b -> Obj Simplex a
src Simplex a b
Z = Simplex Z Z
Z
  src (Y Simplex a y
f) = 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) = forall n. Obj Simplex n -> Obj Simplex (S n)
suc (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Simplex x (S y)
f)

  tgt :: forall a b. Simplex a b -> Obj Simplex b
tgt Simplex a b
Z = Simplex Z Z
Z
  tgt (Y Simplex a y
f) = forall n. Obj Simplex n -> Obj Simplex (S n)
suc (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) = 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   . :: forall b c a. Simplex b c -> Simplex a b -> Simplex a c
.   Simplex a b
f = Simplex a b
f
  Simplex b c
f   .   Simplex a b
Z = Simplex b c
f
  Y Simplex b y
f .   Simplex a b
g = forall x a1. Simplex x a1 -> Simplex x (S a1)
Y (Simplex b y
f 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 forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Simplex a y
g
  X Simplex x (S y)
f . X Simplex x (S y)
g = forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X (forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X Simplex x (S y)
f 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 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 = Simplex Z Z
Z

  initialize :: forall a. Obj Simplex a -> Simplex (InitialObject Simplex) a
initialize Simplex a a
Z = Simplex Z Z
Z
  initialize (X (Y Simplex x y
f)) = forall x a1. Simplex x a1 -> Simplex x (S a1)
Y (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize 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 = forall n. Obj Simplex n -> Obj Simplex (S n)
suc Simplex Z Z
Z

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


data Fin :: Type -> Type 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 % :: forall a b.
Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b)
% Dom Forget a b
Simplex a b
Z   = forall a. Obj (->) a
obj
  Forget
Forget % Y Simplex a y
f = forall a1. Fin a1 -> Fin (S a1)
Fs forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Forget
Forget forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Simplex a y
f)
  Forget
Forget % X Simplex x (S y)
f = \case
    Fin (S x)
Fz -> forall a1. Fin (S a1)
Fz
    Fs Fin n
n -> (Forget
Forget forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% 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 % :: forall a b. Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b)
% (Simplex a1 b1
Z   :**: Simplex a2 b2
g) = Simplex a2 b2
g
  Add
Add % (Y Simplex a1 y
f :**: Simplex a2 b2
g) = forall x a1. Simplex x a1 -> Simplex x (S a1)
Y (Add
Add forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Simplex a1 y
f 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 Simplex x (S y)
f :**: Simplex a2 b2
g) = forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X (Add
Add forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Simplex x (S y)
f 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 = Simplex Z Z
Z

  leftUnitor :: forall (k :: * -> * -> *) a.
(Cod Add ~ k) =>
Add -> Obj k a -> k (Add :% (Unit Add, a)) a
leftUnitor     Add
Add       Obj k a
a   = Obj k a
a
  leftUnitorInv :: forall (k :: * -> * -> *) a.
(Cod Add ~ k) =>
Add -> Obj k a -> k a (Add :% (Unit Add, a))
leftUnitorInv  Add
Add       Obj k a
a   = Obj k a
a
  rightUnitor :: forall (k :: * -> * -> *) a.
(Cod Add ~ k) =>
Add -> Obj k a -> k (Add :% (a, Unit Add)) a
rightUnitor    Add
Add       Obj k a
Simplex a a
Z   = Simplex Z Z
Z
  rightUnitor    Add
Add (X (Y Simplex x y
n)) = forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X (forall x a1. Simplex x a1 -> Simplex x (S a1)
Y (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (a, Unit f)) a
rightUnitor Add
Add Simplex x y
n))
  rightUnitorInv :: forall (k :: * -> * -> *) a.
(Cod Add ~ k) =>
Add -> Obj k a -> k a (Add :% (a, Unit Add))
rightUnitorInv Add
Add       Obj k a
Simplex a a
Z   = Simplex Z Z
Z
  rightUnitorInv Add
Add (X (Y Simplex x y
n)) = forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X (forall x a1. Simplex x a1 -> Simplex x (S a1)
Y (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (a, Unit f))
rightUnitorInv Add
Add Simplex x y
n))
  associator :: forall (k :: * -> * -> *) a b c.
(Cod Add ~ k) =>
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
Simplex a a
Z       Obj k b
Simplex b b
Z   Obj k c
n = Obj k c
n
  associator     Add
Add Obj k a
Simplex a a
Z (X (Y Simplex x y
m)) Obj k c
n = forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X (forall x a1. Simplex x a1 -> Simplex x (S a1)
Y (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 Simplex x y
m Obj k c
n))
  associator     Add
Add (X (Y Simplex x y
l)) Obj k b
m Obj k c
n = forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X (forall x a1. Simplex x a1 -> Simplex x (S a1)
Y (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 x y
l Obj k b
m Obj k c
n))
  associatorInv :: forall (k :: * -> * -> *) a b c.
(Cod Add ~ k) =>
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
Simplex a a
Z       Obj k b
Simplex b b
Z   Obj k c
n = Obj k c
n
  associatorInv  Add
Add Obj k a
Simplex a a
Z (X (Y Simplex x y
m)) Obj k c
n = forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X (forall x a1. Simplex x a1 -> Simplex x (S a1)
Y (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 Simplex x y
m Obj k c
n))
  associatorInv  Add
Add (X (Y Simplex x y
l)) Obj k b
m Obj k c
n = forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X (forall x a1. Simplex x a1 -> Simplex x (S a1)
Y (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 x y
l Obj k b
m Obj k 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 { unit :: Cod Add (Unit Add) (S Z)
unit = forall x a1. Simplex x a1 -> Simplex x (S a1)
Y Simplex Z Z
Z, multiply :: Cod Add (Add :% (S Z, S Z)) (S Z)
multiply = forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X (forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X (forall x a1. Simplex x a1 -> Simplex x (S a1)
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
_ % :: forall a b.
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
Simplex a b
Z = forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject f
f
  Replicate f
f MonoidObject f a
m % Y Simplex a y
n = f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject f a
m forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Cod (Replicate f a) (Replicate f a :% a) (Replicate f a :% y)
n') forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (Unit f, a))
leftUnitorInv f
f (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Cod (Replicate f a) (Replicate f a :% a) (Replicate f a :% y)
n') forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. 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' = forall f a. f -> MonoidObject f a -> Replicate f a
Replicate f
f MonoidObject f a
m forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Simplex a y
n
  Replicate f
f MonoidObject f a
m % X (Y Simplex x y
n) = f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt (forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject f a
m) forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (forall f a. f -> MonoidObject f a -> Replicate f a
Replicate f
f MonoidObject f a
m forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Simplex x y
n))
  Replicate f
f MonoidObject f a
m % X (X Simplex x (S y)
n) = Cod (Replicate f a) (Replicate f a :% S x) (Replicate f a :% S y)
n' forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
multiply MonoidObject f a
m forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj (Cod f) (Replicate f a :% x)
b)) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a 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 f
f Obj (Cod f) a
a Obj (Cod f) a
a Obj (Cod f) (Replicate f a :% x)
b
    where
      n' :: Cod (Replicate f a) (Replicate f a :% S x) (Replicate f a :% S y)
n' = forall f a. f -> MonoidObject f a -> Replicate f a
Replicate f
f MonoidObject f a
m forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall a1 b1. Simplex a1 (S b1) -> Simplex (S a1) (S b1)
X Simplex x (S y)
n
      a :: Obj (Cod f) a
a = forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt (forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject f a
m)
      b :: Obj (Cod f) (Replicate f a :% x)
b = forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src (forall f a. f -> MonoidObject f a -> Replicate f a
Replicate f
f MonoidObject f a
m forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Simplex x (S y)
n)

data Cobar f d = Cobar (Monad f) (Obj (Dom f) d)
-- | The cobar construction
instance Category (Dom f) => Functor (Cobar f d) where
  type Dom (Cobar f d) = Simplex
  type Cod (Cobar f d) = Dom f
  type Cobar f d :% s = (Replicate (EndoFunctorCompose (Dom f)) f :% s) :% d
  Cobar Monad f
f Obj (Dom f) d
d % :: forall a b.
Cobar f d
-> Dom (Cobar f d) a b
-> Cod (Cobar f d) (Cobar f d :% a) (Cobar f d :% b)
% Dom (Cobar f d) a b
s = (forall f a. f -> MonoidObject f a -> Replicate f a
Replicate forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *).
FunctorCompose c d e
FunctorCompose Monad f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom (Cobar f d) a b
s) forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj (Dom f) d
d