{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Instance.Simplex (module Proarrow.Category.Instance.Simplex, Nat (..)) where

import Data.Fin (Fin (..))
import Data.Kind (Type)
import Data.Type.Nat (Nat (..), type Plus, SNatI)
import Data.Vec.Lazy (Vec (..))
import Prelude (Eq, Show (..), (++), type (~))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, obj, src, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Monoid (Monoid (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Data.Typeable (Typeable)

type n + m = Plus n m

data SNat :: Nat -> Type where
  SZ :: SNat Z
  SS :: (IsNat n) => SNat (S n)
instance Show (SNat n) where
  show :: SNat n -> String
show SNat n
SZ = String
"Z"
  show (SS @n') = String
"S" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SNat n -> String
forall a. Show a => a -> String
show (forall (a :: Nat). IsNat a => SNat a
singNat @n')

class (a + Z ~ a, a + S b ~ S (a + b), (a + b) + c ~ a + (b + c)) => Rules a b c
instance (a + Z ~ a, a + S b ~ S (a + b), (a + b) + c ~ a + (b + c)) => Rules a b c

class (forall b c. Rules a b c, SNatI a, Typeable a) => 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 ('S a)
forall (a :: Nat). IsNat a => SNat ('S a)
SS

type Simplex :: CAT Nat
data Simplex a b where
  ZZ :: Simplex Z Z
  Y :: Simplex x y -> Simplex x (S y)
  X :: Simplex x (S y) -> Simplex (S x) (S y)
deriving instance Eq (Simplex a b)
deriving instance Show (Simplex a b)

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 (y :: Nat) (y :: Nat).
Simplex y ('S y) -> Simplex ('S y) ('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 :: 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) (y :: Nat). Simplex x y -> Simplex x ('S y)
Y

-- | The (augmented) simplex category is the category of finite ordinals and order preserving maps.
instance CategoryOf Nat where
  type (~>) = Simplex
  type Ob a = IsNat a

instance Promonad Simplex where
  id :: forall (a :: Nat). Ob a => Simplex a a
id @a = case forall (a :: Nat). IsNat a => SNat a
singNat @a of
    SNat a
SZ -> Simplex a a
Simplex 'Z 'Z
ZZ
    SNat a
SS -> Simplex n n -> Simplex ('S n) ('S n)
forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex ('S a) ('S b)
suc Simplex n n
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Nat). Ob a => Simplex a a
id
  Simplex b c
ZZ . :: 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
  Y Simplex b y
f . Simplex a b
g = Simplex a y -> Simplex a ('S y)
forall (x :: Nat) (y :: Nat). Simplex x y -> Simplex x ('S y)
Y (Simplex b y
f Simplex b y -> Simplex a b -> Simplex a y
forall {k} (p :: 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 :: 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 (y :: Nat) (y :: Nat).
Simplex y ('S y) -> Simplex ('S y) ('S y)
X (Simplex x ('S y) -> Simplex ('S x) ('S y)
forall (y :: Nat) (y :: Nat).
Simplex y ('S y) -> Simplex ('S y) ('S y)
X Simplex x ('S y)
f Simplex ('S x) ('S y) -> Simplex x ('S x) -> Simplex x ('S y)
forall {k} (p :: 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 :: 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
ZZ = 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 :: j +-> k) (a :: k) (b :: j) 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 :: j +-> k) (a :: k) (b :: j) 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). Ob a => InitialObject ~> a
initiate @a = case forall (a :: Nat). IsNat a => SNat a
singNat @a of
    SNat a
SZ -> InitialObject ~> a
Simplex 'Z 'Z
ZZ
    SS @a' -> Simplex 'Z n -> Simplex 'Z ('S n)
forall (x :: Nat) (y :: Nat). Simplex x y -> Simplex x ('S y)
Y (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a')

instance HasTerminalObject Nat where
  type TerminalObject = S Z
  terminate :: forall (a :: Nat). Ob a => a ~> TerminalObject
terminate @a = case forall (a :: Nat). IsNat a => SNat a
singNat @a of
    SNat a
SZ -> Simplex 'Z 'Z -> Simplex 'Z ('S 'Z)
forall (x :: Nat) (y :: Nat). Simplex x y -> Simplex x ('S y)
Y Simplex 'Z 'Z
ZZ
    SS @n -> Simplex n ('S 'Z) -> Simplex ('S n) ('S 'Z)
forall (y :: Nat) (y :: Nat).
Simplex y ('S y) -> Simplex ('S y) ('S y)
X (forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @_ @n)

data family Forget :: Nat +-> Type
instance FunctorForRep Forget where
  type Forget @ n = Fin n
  fmap :: forall (a :: Nat) (b :: Nat).
(a ~> b) -> (Forget @ a) ~> (Forget @ b)
fmap a ~> b
Simplex a b
ZZ = (Forget @ a) ~> (Forget @ b)
Fin 'Z -> Fin 'Z
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  fmap (Y Simplex a y
f) = Fin y -> Fin ('S y)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: Nat +-> Type) (a :: Nat) (b :: Nat).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @Forget a ~> y
Simplex a y
f
  fmap (X Simplex x ('S y)
f) = \case
    Fin ('S x)
FZ -> Fin ('S y)
forall (n1 :: Nat). Fin ('S n1)
FZ
    FS Fin n1
n -> forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: Nat +-> Type) (a :: Nat) (b :: Nat).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @Forget x ~> 'S y
Simplex x ('S y)
f Fin n1
n

data family Pick :: Type -> OPPOSITE Nat +-> Type
instance FunctorForRep (Pick a) where
  type (Pick a) @ OP n = Vec n a
  fmap :: forall (a :: OPPOSITE Nat) (b :: OPPOSITE Nat).
(a ~> b) -> (Pick a @ a) ~> (Pick a @ b)
fmap (Op Simplex b1 a1
ZZ) Vec 'Z a
Pick a @ a
VNil = Vec 'Z a
Pick a @ b
forall a. Vec 'Z a
VNil
  fmap (Op (Y Simplex b1 y
f)) (a
_ ::: Vec n1 a
xs) = forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: OPPOSITE Nat +-> Type) (a :: OPPOSITE Nat)
       (b :: OPPOSITE Nat).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @(Pick a) (Simplex b1 y -> Op Simplex ('OP y) ('OP b1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op Simplex b1 y
f) Vec n1 a
xs
  fmap (Op (X Simplex x ('S y)
f)) (a
x ::: Vec n1 a
xs) = a
x a -> Vec x a -> Vec ('S x) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: (forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: OPPOSITE Nat +-> Type) (a :: OPPOSITE Nat)
       (b :: OPPOSITE Nat).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @(Pick a) (Simplex x ('S y) -> Op Simplex ('OP ('S y)) ('OP x)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op Simplex x ('S y)
f) (a
x a -> Vec n1 a -> Vec ('S n1) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec n1 a
xs))

instance MonoidalProfunctor Simplex where
  par0 :: Simplex Unit Unit
par0 = Simplex 'Z 'Z
Simplex Unit Unit
ZZ
  Simplex x1 x2
ZZ par :: forall (x1 :: Nat) (x2 :: Nat) (y1 :: Nat) (y2 :: Nat).
Simplex x1 x2 -> Simplex y1 y2 -> Simplex (x1 ** y1) (x2 ** y2)
`par` Simplex y1 y2
g = Simplex y1 y2
Simplex (x1 ** y1) (x2 ** y2)
g
  Y Simplex x1 y
f `par` Simplex y1 y2
g = Simplex (Plus x1 y1) (Plus y y2)
-> Simplex (Plus x1 y1) ('S (Plus y y2))
forall (x :: Nat) (y :: Nat). Simplex x y -> Simplex x ('S y)
Y (Simplex x1 y
f Simplex x1 y -> Simplex y1 y2 -> Simplex (x1 ** y1) (y ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: Nat) (x2 :: Nat) (y1 :: Nat) (y2 :: Nat).
Simplex x1 x2 -> Simplex y1 y2 -> Simplex (x1 ** y1) (x2 ** y2)
`par` Simplex y1 y2
g)
  X Simplex x ('S y)
f `par` Simplex y1 y2
g = Simplex (Plus x y1) ('S (Plus y y2))
-> Simplex ('S (Plus x y1)) ('S (Plus y y2))
forall (y :: Nat) (y :: Nat).
Simplex y ('S y) -> Simplex ('S y) ('S y)
X (Simplex x ('S y)
f Simplex x ('S y) -> Simplex y1 y2 -> Simplex (x ** y1) ('S y ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: Nat) (x2 :: Nat) (y1 :: Nat) (y2 :: Nat).
Simplex x1 x2 -> Simplex y1 y2 -> Simplex (x1 ** y1) (x2 ** y2)
`par` Simplex y1 y2
g)

-- | Addition as monoidal tensor.
instance Monoidal Nat where
  type Unit = Z
  type a ** b = a + b
  withOb2 :: forall (a :: Nat) (b :: Nat) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @a @b Ob (a ** b) => r
r = case forall (a :: Nat). IsNat a => SNat a
singNat @a of
    SNat a
SZ -> r
Ob (a ** b) => r
r
    SS @a' -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a' @b r
Ob (a ** b) => r
Ob (n ** b) => r
r
  leftUnitor :: forall (a :: Nat). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
Simplex a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Nat). Ob a => Simplex a a
id
  leftUnitorInv :: forall (a :: Nat). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
Simplex a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Nat). Ob a => Simplex a a
id
  rightUnitor :: forall (a :: Nat). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
Simplex a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Nat). Ob a => Simplex a a
id
  rightUnitorInv :: forall (a :: Nat). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
Simplex a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Nat). Ob a => Simplex a a
id
  associator :: forall (a :: Nat) (b :: Nat) (c :: Nat).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @a @b @c = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(a ** b) @c (forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: Nat +-> Nat) (a :: Nat). (Promonad p, Ob a) => p a a
id @Simplex))
  associatorInv :: forall (a :: Nat) (b :: Nat) (c :: Nat).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @a @b @c = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @b @c (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @(b ** c) (forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: Nat +-> Nat) (a :: Nat). (Promonad p, Ob a) => p a a
id @Simplex))

-- Not symmetric monoidal

instance Monoid Z where
  mempty :: Unit ~> 'Z
mempty = Unit ~> 'Z
Simplex 'Z 'Z
ZZ
  mappend :: ('Z ** 'Z) ~> 'Z
mappend = ('Z ** 'Z) ~> 'Z
Simplex 'Z 'Z
ZZ

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

data family Replicate :: k -> Nat +-> k
instance (Monoid m) => FunctorForRep (Replicate m) where
  type Replicate m @ Z = Unit
  type Replicate m @ S b = m ** (Replicate m @ b)
  fmap :: forall (a :: Nat) (b :: Nat).
(a ~> b) -> (Replicate m @ a) ~> (Replicate m @ b)
fmap a ~> b
Simplex a b
ZZ = (Replicate m @ a) ~> (Replicate m @ b)
Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  fmap (Y Simplex a y
f) = let g :: (Replicate m @ a) ~> (Replicate m @ y)
g = forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: Nat +-> k) (a :: Nat) (b :: Nat).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @(Replicate m) a ~> y
Simplex a y
f in (forall (m :: k). 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 (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`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 :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Replicate m @ a) ~> (Unit ** (Replicate m @ a))
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv ((Ob (Replicate m @ a), Ob (Replicate m @ y)) =>
 (Replicate m @ a) ~> (m ** (Replicate m @ y)))
-> ((Replicate m @ a) ~> (Replicate m @ y))
-> (Replicate m @ a) ~> (m ** (Replicate m @ y))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Replicate m @ a) ~> (Replicate m @ y)
g
  fmap (X (Y Simplex x y
f)) = forall (a :: k). (CategoryOf k, 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 (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: Nat +-> k) (a :: Nat) (b :: Nat).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @(Replicate m) x ~> y
Simplex x y
f
  fmap (X (X @x Simplex x ('S y)
f)) =
    let g :: (Replicate m @ 'S x) ~> (Replicate m @ 'S y)
g = forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: Nat +-> k) (a :: Nat) (b :: Nat).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @(Replicate m) (Simplex x ('S y) -> Simplex ('S x) ('S y)
forall (y :: Nat) (y :: Nat).
Simplex y ('S y) -> Simplex ('S y) ('S y)
X Simplex x ('S y)
f)
        b :: (Replicate m @ x) ~> (Replicate m @ x)
b = forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: Nat +-> k) (a :: Nat) (b :: Nat).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @(Replicate m) (Simplex x ('S y) -> x ~> x
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src Simplex x ('S y)
f)
    in (Replicate m @ 'S x) ~> (Replicate m @ 'S y)
(m ** (Replicate m @ x)) ~> (m ** (Replicate m @ 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 :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (m :: k). 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 (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`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 :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @m @m @(Replicate m @ x) ((Ob (Replicate m @ x), Ob (Replicate m @ x)) =>
 (m ** (m ** (Replicate m @ x))) ~> (m ** (Replicate m @ y)))
-> ((Replicate m @ x) ~> (Replicate m @ x))
-> (m ** (m ** (Replicate m @ x))) ~> (m ** (Replicate m @ y))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Replicate m @ x) ~> (Replicate m @ x)
b