module Proarrow.Category.Instance.Simplex where

import Data.Kind (Type)

import Proarrow.Core (CAT, CategoryOf(..), Profunctor(..), Promonad(..), dimapDefault, PRO, Obj, obj, src)
import Proarrow.Profunctor.Representable (dimapRep, Representable(..))
import Proarrow.Object.Initial (HasInitialObject(..))
import Proarrow.Object.Terminal (HasTerminalObject(..))
import Proarrow.Category.Monoidal (Monoidal(..))
import Proarrow.Monoid (Monoid(..))

type data Nat = Z | S Nat
data SNat :: Nat -> Type where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

class IsNat (a :: Nat) where
  singNat :: SNat a
instance IsNat Z where singNat :: SNat Z
singNat = SNat Z
SZ
instance IsNat a => IsNat (S a) where singNat :: SNat (S a)
singNat = SNat a -> SNat (S a)
forall (n :: Nat). SNat n -> SNat (S n)
SS SNat a
forall (a :: Nat). IsNat a => SNat a
singNat

singNat' :: forall a. Obj a -> SNat a
singNat' :: forall (a :: Nat). Obj a -> SNat a
singNat' Obj a
a = forall (a :: Nat). IsNat a => SNat a
singNat @a ((Ob a, Ob a) => SNat a) -> Simplex a a -> SNat a
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Nat) (b :: Nat) r.
((Ob a, Ob b) => r) -> Simplex a b -> r
\\ Obj a
Simplex a a
a

singObj :: SNat a -> Obj a
singObj :: forall (a :: Nat). SNat a -> Obj a
singObj SNat a
SZ = a ~> a
Obj Z
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj
singObj (SS SNat n
n) = Simplex n n -> Simplex (S n) (S n)
forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex (S a) (S b)
suc (SNat n -> Obj n
forall (a :: Nat). SNat a -> Obj a
singObj SNat n
n)

type Simplex :: CAT Nat
data Simplex a b where
  Z ::                    Simplex    Z     Z
  Y :: Simplex x    y  -> Simplex    x  (S y)
  X :: Simplex x (S y) -> Simplex (S x) (S y)

suc :: Simplex a b -> Simplex (S a) (S b)
suc :: forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex (S a) (S b)
suc = Simplex a (S b) -> Simplex (S a) (S b)
forall (n :: Nat) (y :: Nat).
Simplex n (S y) -> Simplex (S n) (S y)
X (Simplex a (S b) -> Simplex (S a) (S b))
-> (Simplex a b -> Simplex a (S b))
-> Simplex a b
-> Simplex (S a) (S b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Simplex a b -> Simplex a (S b)
forall (x :: Nat) (n :: Nat). Simplex x n -> Simplex x (S n)
Y



instance CategoryOf Nat where
  type (~>) = Simplex
  type Ob a = IsNat a

instance Promonad Simplex where
  id :: forall a. Ob a => Simplex a a
  id :: forall (a :: Nat). Ob a => Simplex a a
id = SNat a -> Simplex a a
forall (b :: Nat). SNat b -> Simplex b b
go (forall (a :: Nat). IsNat a => SNat a
singNat @a) where
    go :: SNat b -> Simplex b b
    go :: forall (b :: Nat). SNat b -> Simplex b b
go SNat b
SZ = Simplex b b
Simplex Z Z
Z
    go (SS SNat n
n) = Simplex n n -> Simplex (S n) (S n)
forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex (S a) (S b)
suc (SNat n -> Simplex n n
forall (b :: Nat). SNat b -> Simplex b b
go SNat n
n)
  Simplex b c
Z   . :: forall (b :: Nat) (c :: Nat) (a :: Nat).
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 :: Nat) (n :: Nat). Simplex x n -> Simplex x (S n)
Y (Simplex b y
f Simplex b y -> Simplex a b -> Simplex a y
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Nat) (c :: Nat) (a :: Nat).
Simplex b c -> Simplex a b -> Simplex a c
. Simplex a b
g)
  X Simplex x (S y)
f . Y Simplex a y
g = Simplex x c
Simplex x (S y)
f Simplex x c -> Simplex a x -> Simplex a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Nat) (c :: Nat) (a :: Nat).
Simplex b c -> Simplex a b -> Simplex 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 (n :: Nat) (y :: Nat).
Simplex n (S y) -> Simplex (S n) (S y)
X (Simplex x (S y) -> Simplex (S x) (S y)
forall (n :: Nat) (y :: Nat).
Simplex n (S y) -> Simplex (S n) (S y)
X Simplex x (S y)
f Simplex (S x) (S y) -> Simplex x (S x) -> Simplex x (S y)
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Nat) (c :: Nat) (a :: Nat).
Simplex b c -> Simplex a b -> Simplex a c
. Simplex x (S x)
Simplex x (S y)
g)

instance Profunctor Simplex where
  dimap :: forall (c :: Nat) (a :: Nat) (b :: Nat) (d :: Nat).
(c ~> a) -> (b ~> d) -> Simplex a b -> Simplex c d
dimap = (c ~> a) -> (b ~> d) -> Simplex a b -> Simplex c d
Simplex c a -> Simplex b d -> Simplex a b -> Simplex c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: Nat) (b :: Nat) r.
((Ob a, Ob b) => r) -> Simplex a b -> r
\\ Simplex a b
Z = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Y Simplex a y
f = r
(Ob a, Ob b) => r
(Ob a, Ob y) => r
r ((Ob a, Ob y) => r) -> Simplex a y -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Nat) (b :: Nat) r.
((Ob a, Ob b) => r) -> Simplex a b -> r
\\ Simplex a y
f
  (Ob a, Ob b) => r
r \\ X Simplex x (S y)
f = r
(Ob a, Ob b) => r
(Ob x, Ob (S y)) => r
r ((Ob x, Ob (S y)) => r) -> Simplex x (S y) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Nat) (b :: Nat) r.
((Ob a, Ob b) => r) -> Simplex a b -> r
\\ Simplex x (S y)
f

instance HasInitialObject Nat where
  type InitialObject = Z
  initiate' :: forall (a :: Nat). Obj a -> InitialObject ~> a
initiate' Obj a
a = SNat a -> Simplex Z a
forall (b :: Nat). SNat b -> Simplex Z b
go (Obj a -> SNat a
forall (a :: Nat). Obj a -> SNat a
singNat' Obj a
a) where
    go :: SNat b -> Simplex Z b
    go :: forall (b :: Nat). SNat b -> Simplex Z b
go SNat b
SZ = Simplex Z b
Simplex Z Z
Z
    go (SS SNat n
n) = Simplex Z n -> Simplex Z (S n)
forall (x :: Nat) (n :: Nat). Simplex x n -> Simplex x (S n)
Y (SNat n -> Simplex Z n
forall (b :: Nat). SNat b -> Simplex Z b
go SNat n
n)

instance HasTerminalObject Nat where
  type TerminalObject = S Z
  terminate' :: forall (a :: Nat). Obj a -> a ~> TerminalObject
terminate' Obj a
a = SNat a -> Simplex a (S Z)
forall (b :: Nat). SNat b -> Simplex b (S Z)
go (Obj a -> SNat a
forall (a :: Nat). Obj a -> SNat a
singNat' Obj a
a) where
    go :: SNat b -> Simplex b (S Z)
    go :: forall (b :: Nat). SNat b -> Simplex b (S Z)
go SNat b
SZ = Simplex b Z -> Simplex b (S Z)
forall (x :: Nat) (n :: Nat). Simplex x n -> Simplex x (S n)
Y Simplex b Z
Simplex Z Z
Z
    go (SS SNat n
n) = Simplex n (S Z) -> Simplex (S n) (S Z)
forall (n :: Nat) (y :: Nat).
Simplex n (S y) -> Simplex (S n) (S y)
X (SNat n -> Simplex n (S Z)
forall (b :: Nat). SNat b -> Simplex b (S Z)
go SNat n
n)


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

type Forget :: PRO Type Nat
data Forget a b where
  Forget :: Ob b => { forall (b :: Nat) a. Forget a b -> a -> Fin b
getForget :: a -> Fin b } -> Forget a b

instance Profunctor Forget where
  dimap :: forall c a (b :: Nat) (d :: Nat).
(c ~> a) -> (b ~> d) -> Forget a b -> Forget c d
dimap = (c ~> a) -> (b ~> d) -> Forget a b -> Forget c d
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (c :: j) (d :: k).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall a (b :: Nat) r. ((Ob a, Ob b) => r) -> Forget a b -> r
\\ Forget a -> Fin b
f = r
(Ob a, Ob (Fin b)) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (Fin b)) => r) -> (a -> Fin b) -> r
forall a b r. ((Ob a, Ob b) => r) -> (a -> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a -> Fin b
f
instance Representable Forget where
  type Forget % n = Fin n
  index :: forall a (b :: Nat). Forget a b -> a ~> (Forget % b)
index = Forget a b -> a ~> (Forget % b)
Forget a b -> a -> Fin b
forall (b :: Nat) a. Forget a b -> a -> Fin b
getForget
  tabulate :: forall (b :: Nat) a. Ob b => (a ~> (Forget % b)) -> Forget a b
tabulate = (a ~> (Forget % b)) -> Forget a b
(a -> Fin b) -> Forget a b
forall (b :: Nat) a. Ob b => (a -> Fin b) -> Forget a b
Forget
  repMap :: forall (a :: Nat) (b :: Nat).
(a ~> b) -> (Forget % a) ~> (Forget % b)
repMap a ~> b
Simplex a b
Z = (Forget % a) ~> (Forget % b)
Fin Z -> Fin Z
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  repMap (Y Simplex a y
f) = Fin y -> Fin (S y)
forall (n :: Nat). Fin n -> Fin (S n)
Fs (Fin y -> Fin (S y)) -> (Fin a -> Fin y) -> Fin a -> Fin (S y)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO Type Nat) (a :: Nat) (b :: Nat).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @Forget a ~> y
Simplex a y
f
  repMap (X Simplex x (S y)
f) = \case
    Fin (S x)
Fz -> Fin (S y)
forall (n :: Nat). Fin (S n)
Fz
    Fs Fin n
n -> forall {j} {k} (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO Type Nat) (a :: Nat) (b :: Nat).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @Forget x ~> S y
Simplex x (S y)
f Fin n
n

type family (a :: Nat) + (b :: Nat) :: Nat where
  Z + b = b
  S a + b = S (a + b)

instance Monoidal Nat where
  type Unit = Z
  type a ** b = a + b
  a ~> b
Simplex a b
Z   par :: forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` c ~> d
g = c ~> d
(a ** c) ~> (b ** d)
g
  Y Simplex a y
f `par` c ~> d
g = Simplex (a + c) (y + d) -> Simplex (a + c) (S (y + d))
forall (x :: Nat) (n :: Nat). Simplex x n -> Simplex x (S n)
Y (a ~> y
Simplex a y
f (a ~> y) -> (c ~> d) -> (a ** c) ~> (y ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` c ~> d
g)
  X Simplex x (S y)
f `par` c ~> d
g = Simplex (x + c) (S (y + d)) -> Simplex (S (x + c)) (S (y + d))
forall (n :: Nat) (y :: Nat).
Simplex n (S y) -> Simplex (S n) (S y)
X (x ~> S y
Simplex x (S y)
f (x ~> S y) -> (c ~> d) -> (x ** c) ~> (S y ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` c ~> d
g)
  leftUnitor :: forall (a :: Nat). Obj a -> (Unit ** a) ~> a
leftUnitor Obj a
a = Obj a
(Unit ** a) ~> a
a
  leftUnitorInv :: forall (a :: Nat). Obj a -> a ~> (Unit ** a)
leftUnitorInv Obj a
a = Obj a
a ~> (Unit ** a)
a
  rightUnitor :: forall (a :: Nat). Obj a -> (a ** Unit) ~> a
rightUnitor = SNat a -> Simplex (a + Z) a
forall (b :: Nat). SNat b -> Simplex (b + Z) b
rightUnitor' (SNat a -> Simplex (a + Z) a)
-> (Simplex a a -> SNat a) -> Simplex a a -> Simplex (a + Z) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> a) -> SNat a
Simplex a a -> SNat a
forall (a :: Nat). Obj a -> SNat a
singNat'
  rightUnitorInv :: forall (a :: Nat). Obj a -> a ~> (a ** Unit)
rightUnitorInv = SNat a -> Simplex a (a + Z)
forall (b :: Nat). SNat b -> Simplex b (b + Z)
rightUnitorInv' (SNat a -> Simplex a (a + Z))
-> (Simplex a a -> SNat a) -> Simplex a a -> Simplex a (a + Z)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> a) -> SNat a
Simplex a a -> SNat a
forall (a :: Nat). Obj a -> SNat a
singNat'
  associator :: forall (a :: Nat) (b :: Nat) (c :: Nat).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Obj a
a' Obj b
b' = SNat a -> SNat b -> (c ~> c) -> Simplex ((a + b) + c) (a + (b + c))
forall (a :: Nat) (b :: Nat) (c :: Nat).
SNat a -> SNat b -> Obj c -> Simplex ((a + b) + c) (a + (b + c))
associator' (Obj a -> SNat a
forall (a :: Nat). Obj a -> SNat a
singNat' Obj a
a') (Obj b -> SNat b
forall (a :: Nat). Obj a -> SNat a
singNat' Obj b
b')
  associatorInv :: forall (a :: Nat) (b :: Nat) (c :: Nat).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj a
a' Obj b
b' = SNat a -> SNat b -> (c ~> c) -> Simplex (a + (b + c)) ((a + b) + c)
forall (a :: Nat) (b :: Nat) (c :: Nat).
SNat a -> SNat b -> Obj c -> Simplex (a + (b + c)) ((a + b) + c)
associatorInv' (Obj a -> SNat a
forall (a :: Nat). Obj a -> SNat a
singNat' Obj a
a') (Obj b -> SNat b
forall (a :: Nat). Obj a -> SNat a
singNat' Obj b
b')

rightUnitor' :: SNat b -> Simplex (b + Z) b
rightUnitor' :: forall (b :: Nat). SNat b -> Simplex (b + Z) b
rightUnitor' SNat b
SZ = Simplex (b + Z) b
Simplex Z Z
Z
rightUnitor' (SS SNat n
n) = Simplex (n + Z) n -> Simplex (S (n + Z)) (S n)
forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex (S a) (S b)
suc (SNat n -> Simplex (n + Z) n
forall (b :: Nat). SNat b -> Simplex (b + Z) b
rightUnitor' SNat n
n)

rightUnitorInv' :: SNat b -> Simplex b (b + Z)
rightUnitorInv' :: forall (b :: Nat). SNat b -> Simplex b (b + Z)
rightUnitorInv' SNat b
SZ = Simplex b (b + Z)
Simplex Z Z
Z
rightUnitorInv' (SS SNat n
n) = Simplex n (n + Z) -> Simplex (S n) (S (n + Z))
forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex (S a) (S b)
suc (SNat n -> Simplex n (n + Z)
forall (b :: Nat). SNat b -> Simplex b (b + Z)
rightUnitorInv' SNat n
n)

associator' :: SNat a -> SNat b -> Obj c -> Simplex ((a + b) + c) (a + (b + c))
associator' :: forall (a :: Nat) (b :: Nat) (c :: Nat).
SNat a -> SNat b -> Obj c -> Simplex ((a + b) + c) (a + (b + c))
associator' SNat a
SZ SNat b
SZ Obj c
c = Obj c
Simplex ((a + b) + c) (a + (b + c))
c
associator' SNat a
SZ (SS SNat n
b) Obj c
c = Simplex (n + c) (n + c) -> Simplex (S (n + c)) (S (n + c))
forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex (S a) (S b)
suc (SNat Z -> SNat n -> Obj c -> Simplex ((Z + n) + c) (Z + (n + c))
forall (a :: Nat) (b :: Nat) (c :: Nat).
SNat a -> SNat b -> Obj c -> Simplex ((a + b) + c) (a + (b + c))
associator' SNat Z
SZ SNat n
b Obj c
c)
associator' (SS SNat n
a) SNat b
b Obj c
c = Simplex ((n + b) + c) (n + (b + c))
-> Simplex (S ((n + b) + c)) (S (n + (b + c)))
forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex (S a) (S b)
suc (SNat n -> SNat b -> Obj c -> Simplex ((n + b) + c) (n + (b + c))
forall (a :: Nat) (b :: Nat) (c :: Nat).
SNat a -> SNat b -> Obj c -> Simplex ((a + b) + c) (a + (b + c))
associator' SNat n
a SNat b
b Obj c
c)

associatorInv' :: SNat a -> SNat b -> Obj c -> Simplex (a + (b + c)) ((a + b) + c)
associatorInv' :: forall (a :: Nat) (b :: Nat) (c :: Nat).
SNat a -> SNat b -> Obj c -> Simplex (a + (b + c)) ((a + b) + c)
associatorInv' SNat a
SZ SNat b
SZ Obj c
c = Obj c
Simplex (a + (b + c)) ((a + b) + c)
c
associatorInv' SNat a
SZ (SS SNat n
b) Obj c
c = Simplex (n + c) (n + c) -> Simplex (S (n + c)) (S (n + c))
forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex (S a) (S b)
suc (SNat Z -> SNat n -> Obj c -> Simplex (Z + (n + c)) ((Z + n) + c)
forall (a :: Nat) (b :: Nat) (c :: Nat).
SNat a -> SNat b -> Obj c -> Simplex (a + (b + c)) ((a + b) + c)
associatorInv' SNat Z
SZ SNat n
b Obj c
c)
associatorInv' (SS SNat n
a) SNat b
b Obj c
c = Simplex (n + (b + c)) ((n + b) + c)
-> Simplex (S (n + (b + c))) (S ((n + b) + c))
forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex (S a) (S b)
suc (SNat n -> SNat b -> Obj c -> Simplex (n + (b + c)) ((n + b) + c)
forall (a :: Nat) (b :: Nat) (c :: Nat).
SNat a -> SNat b -> Obj c -> Simplex (a + (b + c)) ((a + b) + c)
associatorInv' SNat n
a SNat b
b Obj c
c)


instance Monoid (S Z) where
  mempty :: Unit ~> S Z
mempty = Simplex Z Z -> Simplex Z (S Z)
forall (x :: Nat) (n :: Nat). Simplex x n -> Simplex x (S n)
Y Simplex Z Z
Z
  mappend :: (S Z ** S Z) ~> S Z
mappend = Simplex (S Z) (S Z) -> Simplex (S (S Z)) (S Z)
forall (n :: Nat) (y :: Nat).
Simplex n (S y) -> Simplex (S n) (S y)
X (Simplex Z (S Z) -> Simplex (S Z) (S Z)
forall (n :: Nat) (y :: Nat).
Simplex n (S y) -> Simplex (S n) (S y)
X (Simplex Z Z -> Simplex Z (S Z)
forall (x :: Nat) (n :: Nat). Simplex x n -> Simplex x (S n)
Y Simplex Z Z
Z))

type Replicate :: k -> PRO k Nat
data Replicate m a b where
  Replicate :: Ob b => a ~> (Replicate m % b) -> Replicate m a b
instance (Monoid m) => Profunctor (Replicate m) where
  dimap :: forall (c :: j) (a :: j) (b :: Nat) (d :: Nat).
(c ~> a) -> (b ~> d) -> Replicate m a b -> Replicate m c d
dimap = (c ~> a) -> (b ~> d) -> Replicate m a b -> Replicate m c d
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (c :: j) (d :: k).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: Nat) r.
((Ob a, Ob b) => r) -> Replicate m a b -> r
\\ Replicate a ~> (Replicate m % b)
f = r
(Ob a, Ob (Replicate m % b)) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (Replicate m % b)) => r)
-> (a ~> (Replicate m % b)) -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (Replicate m % b)
f
instance (Monoid m) => Representable (Replicate m) where
  type Replicate m % Z = Unit
  type Replicate m % S b = m ** (Replicate m % b)
  index :: forall (a :: j) (b :: Nat).
Replicate m a b -> a ~> (Replicate m % b)
index (Replicate a ~> (Replicate m % b)
f) = a ~> (Replicate m % b)
f
  tabulate :: forall (b :: Nat) (a :: j).
Ob b =>
(a ~> (Replicate m % b)) -> Replicate m a b
tabulate = (a ~> (Replicate m % b)) -> Replicate m a b
forall {j} (b :: Nat) (a :: j) (m :: j).
Ob b =>
(a ~> (Replicate m % b)) -> Replicate m a b
Replicate
  repMap :: forall (a :: Nat) (b :: Nat).
(a ~> b) -> (Replicate m % a) ~> (Replicate m % b)
repMap a ~> b
Simplex a b
Z = forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @Unit
  repMap (Y Simplex a y
f) = let g :: (Replicate m % a) ~> (Replicate m % y)
g = forall {j} {k} (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO j Nat) (a :: Nat) (b :: Nat).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(Replicate m) a ~> y
Simplex a y
f in (forall (m :: j). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @m (Unit ~> m)
-> ((Replicate m % a) ~> (Replicate m % y))
-> (Unit ** (Replicate m % a)) ~> (m ** (Replicate m % y))
forall (a :: j) (b :: j) (c :: j) (d :: j).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` (Replicate m % a) ~> (Replicate m % y)
g) ((Unit ** (Replicate m % a)) ~> (m ** (Replicate m % y)))
-> ((Replicate m % a) ~> (Unit ** (Replicate m % a)))
-> (Replicate m % a) ~> (m ** (Replicate m % y))
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (Replicate m % a)
-> (Replicate m % a) ~> (Unit ** (Replicate m % a))
forall (a :: j). Obj a -> a ~> (Unit ** a)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
leftUnitorInv (((Replicate m % a) ~> (Replicate m % y)) -> Obj (Replicate m % a)
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src (Replicate m % a) ~> (Replicate m % y)
g)
  repMap (X (Y Simplex x y
f)) = forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m Obj m
-> ((Replicate m % x) ~> (Replicate m % y))
-> (m ** (Replicate m % x)) ~> (m ** (Replicate m % y))
forall (a :: j) (b :: j) (c :: j) (d :: j).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` forall {j} {k} (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO j Nat) (a :: Nat) (b :: Nat).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(Replicate m) x ~> y
Simplex x y
f
  repMap (X (X Simplex x (S y)
f)) =
    let g :: (Replicate m % S x) ~> (Replicate m % S y)
g = forall {j} {k} (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO j Nat) (a :: Nat) (b :: Nat).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(Replicate m) (Simplex x (S y) -> Simplex (S x) (S y)
forall (n :: Nat) (y :: Nat).
Simplex n (S y) -> Simplex (S n) (S y)
X Simplex x (S y)
f)
        b :: (Replicate m % x) ~> (Replicate m % x)
b = forall {j} {k} (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO j Nat) (a :: Nat) (b :: Nat).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(Replicate m) (Simplex x (S y) -> x ~> x
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src Simplex x (S y)
f)
    in (m ** (Replicate m % x)) ~> (m ** (Replicate m % y))
(Replicate m % S x) ~> (Replicate m % S y)
g ((m ** (Replicate m % x)) ~> (m ** (Replicate m % y)))
-> ((m ** (m ** (Replicate m % x))) ~> (m ** (Replicate m % x)))
-> (m ** (m ** (Replicate m % x))) ~> (m ** (Replicate m % y))
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (m :: j). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @m ((m ** m) ~> m)
-> ((Replicate m % x) ~> (Replicate m % x))
-> ((m ** m) ** (Replicate m % x)) ~> (m ** (Replicate m % x))
forall (a :: j) (b :: j) (c :: j) (d :: j).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` (Replicate m % x) ~> (Replicate m % x)
b) (((m ** m) ** (Replicate m % x)) ~> (m ** (Replicate m % x)))
-> ((m ** (m ** (Replicate m % x)))
    ~> ((m ** m) ** (Replicate m % x)))
-> (m ** (m ** (Replicate m % x))) ~> (m ** (Replicate m % x))
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj m
-> Obj m
-> ((Replicate m % x) ~> (Replicate m % x))
-> (m ** (m ** (Replicate m % x)))
   ~> ((m ** m) ** (Replicate m % x))
forall (a :: j) (b :: j) (c :: j).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv (forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m) (forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m) (Replicate m % x) ~> (Replicate m % x)
b