{-# 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 (..), SNatI, type Plus)
import Data.Vec.Lazy (Vec (..))
import Prelude (Eq, Show (..), (++), type (~))

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

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 + S b ~ S (a + b), Strictly a) => Rules a b
instance (a + S b ~ S (a + b), Strictly a) => Rules a b

class (forall b. Rules a b, 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
  one :: Simplex Unit Unit
one = Simplex 'Z 'Z
Simplex Unit Unit
ZZ
  Simplex x1 x2
ZZ ** :: forall (x1 :: Nat) (x2 :: Nat) (y1 :: Nat) (y2 :: Nat).
Simplex x1 x2 -> Simplex y1 y2 -> Simplex (x1 ** y1) (x2 ** y2)
** Simplex y1 y2
g = Simplex y1 y2
Simplex (x1 ** y1) (x2 ** y2)
g
  Y Simplex x1 y
f ** 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)
** Simplex y1 y2
g)
  X Simplex x ('S y)
f ** 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)
** 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
one
  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)
** (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)
** 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)
** (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