{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Instance.Simplex where

import Data.Kind (Constraint, Type)

import Prelude (type (~))

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

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

class (a + Z ~ a) => IsNat (a :: Nat) where
  singNat :: SNat a
  withIsNat2 :: IsNat b => (IsNat (a + b) => r) -> r
instance IsNat Z where
  singNat :: SNat Z
singNat = SNat Z
SZ
  withIsNat2 :: forall (b :: Nat) r. IsNat b => (IsNat (Z + b) => r) -> r
withIsNat2 IsNat (Z + b) => r
r = r
IsNat (Z + b) => r
r
instance (IsNat a) => IsNat (S a) where
  singNat :: SNat (S a)
singNat = SNat a -> SNat (S a)
forall (j :: Nat). SNat j -> SNat (S j)
SS SNat a
forall (a :: Nat). IsNat a => SNat a
singNat
  withIsNat2 :: forall (b :: Nat) r. IsNat b => (IsNat (S a + b) => r) -> r
withIsNat2 @b IsNat (S a + b) => r
r = forall (a :: Nat) (b :: Nat) r.
(IsNat a, IsNat b) =>
(IsNat (a + b) => r) -> r
withIsNat2 @a @b r
IsNat (a + b) => r
IsNat (S a + b) => r
r

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
  ZZ :: 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 (j :: Nat) (y :: Nat).
Simplex j (S y) -> Simplex (S j) (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) (j :: Nat). Simplex x j -> Simplex x (S j)
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 -> Obj a
forall (a :: Nat). SNat a -> Obj a
singObj (forall (a :: Nat). IsNat a => SNat a
singNat @a)
  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) (j :: Nat). Simplex x j -> Simplex x (S j)
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 (j :: Nat) (y :: Nat).
Simplex j (S y) -> Simplex (S j) (S y)
X (Simplex x (S y) -> Simplex (S x) (S y)
forall (j :: Nat) (y :: Nat).
Simplex j (S y) -> Simplex (S j) (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
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 :: 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) (a :: Nat). (a' ~> a) -> InitialObject ~> a
initiate' a' ~> a
Simplex a' a
ZZ = InitialObject ~> a
Simplex Z Z
ZZ
  initiate' (Y Simplex a' y
n) = Simplex Z y -> Simplex Z (S y)
forall (x :: Nat) (j :: Nat). Simplex x j -> Simplex x (S j)
Y ((a' ~> y) -> InitialObject ~> y
forall k (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
forall (a' :: Nat) (a :: Nat). (a' ~> a) -> InitialObject ~> a
initiate' a' ~> y
Simplex a' y
n)
  initiate' (X Simplex x (S y)
n) = (x ~> S y) -> InitialObject ~> S y
forall k (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
forall (a' :: Nat) (a :: Nat). (a' ~> a) -> InitialObject ~> a
initiate' x ~> S y
Simplex x (S y)
n

instance HasTerminalObject Nat where
  type TerminalObject = S Z
  terminate' :: forall (a :: Nat) (a' :: Nat). (a ~> a') -> a ~> TerminalObject
terminate' a ~> a'
Simplex a a'
ZZ = Simplex Z Z -> Simplex Z (S Z)
forall (x :: Nat) (j :: Nat). Simplex x j -> Simplex x (S j)
Y Simplex Z Z
ZZ
  terminate' (Y Simplex a y
n) = (a ~> y) -> a ~> TerminalObject
forall k (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> a') -> a ~> TerminalObject
forall (a :: Nat) (a' :: Nat). (a ~> a') -> a ~> TerminalObject
terminate' a ~> y
Simplex a y
n
  terminate' (X Simplex x (S y)
n) = Simplex x (S Z) -> Simplex (S x) (S Z)
forall (j :: Nat) (y :: Nat).
Simplex j (S y) -> Simplex (S j) (S y)
X ((x ~> S y) -> x ~> TerminalObject
forall k (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> a') -> a ~> TerminalObject
forall (a :: Nat) (a' :: Nat). (a ~> a') -> a ~> TerminalObject
terminate' x ~> S y
Simplex x (S y)
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
unForget :: 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 :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
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
unForget
  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
ZZ = (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 (j :: Nat). Fin j -> Fin (S j)
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 :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: Nat +-> Type) (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 (j :: Nat). Fin (S j)
Fz
    Fs Fin n
n -> forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: Nat +-> Type) (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 MonoidalProfunctor Simplex where
  par0 :: Simplex Unit Unit
par0 = Simplex Unit Unit
Simplex Z Z
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 (x1 + y1) (y + y2) -> Simplex (x1 + y1) (S (y + y2))
forall (x :: Nat) (j :: Nat). Simplex x j -> Simplex x (S j)
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 (x + y1) (S (y + y2)) -> Simplex (S (x + y1)) (S (y + y2))
forall (j :: Nat) (y :: Nat).
Simplex j (S y) -> Simplex (S j) (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)

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 = forall (a :: Nat) (b :: Nat) r.
(IsNat a, IsNat b) =>
(IsNat (a + b) => r) -> r
withIsNat2 @a @b
  leftUnitor :: forall (a :: Nat). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
Simplex a a
forall {k} (p :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 = SNat a -> SNat b -> Obj 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' (forall (a :: Nat). IsNat a => SNat a
singNat @a) (forall (a :: Nat). IsNat a => SNat a
singNat @b) (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: Nat). (CategoryOf Nat, Ob a) => Obj a
obj @c)
  associatorInv :: forall (a :: Nat) (b :: Nat) (c :: Nat).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @a @b @c = SNat a -> SNat b -> Obj 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' (forall (a :: Nat). IsNat a => SNat a
singNat @a) (forall (a :: Nat). IsNat a => SNat a
singNat @b) (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: Nat). (CategoryOf Nat, Ob a) => Obj a
obj @c)

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) (j :: Nat). Simplex x j -> Simplex x (S j)
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 (j :: Nat) (y :: Nat).
Simplex j (S y) -> Simplex (S j) (S y)
X (Simplex Z (S Z) -> Simplex (S Z) (S Z)
forall (j :: Nat) (y :: Nat).
Simplex j (S y) -> Simplex (S j) (S y)
X (Simplex Z Z -> Simplex Z (S Z)
forall (x :: Nat) (j :: Nat). Simplex x j -> Simplex x (S j)
Y Simplex Z Z
ZZ))

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 :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
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 :: k) (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 :: k).
Ob b =>
(a ~> (Replicate m % b)) -> Replicate m a b
tabulate = (a ~> (Replicate m % b)) -> Replicate m a b
forall {k} (b :: Nat) (a :: k) (m :: k).
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
ZZ = Unit ~> Unit
(Replicate m % a) ~> (Replicate m % b)
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  repMap (Y Simplex a y
f) = let g :: (Replicate m % a) ~> (Replicate m % y)
g = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: Nat +-> k) (a :: Nat) (b :: Nat).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(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 :: PRO 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 :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Replicate m % a) ~> (Replicate m % y)
g
  repMap (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} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: Nat +-> k) (a :: Nat) (b :: Nat).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(Replicate m) x ~> y
Simplex x y
f
  repMap (X (X @x Simplex x (S y)
f)) =
    let g :: (Replicate m % S x) ~> (Replicate m % S y)
g = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: Nat +-> k) (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 (j :: Nat) (y :: Nat).
Simplex j (S y) -> Simplex (S j) (S y)
X Simplex x (S y)
f)
        b :: (Replicate m % x) ~> (Replicate m % x)
b = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: Nat +-> k) (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 :: k) (c :: k) (a :: k). (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 :: 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 :: PRO 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 :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Replicate m % x) ~> (Replicate m % x)
b

class IsSimplex s where
  bisimplex :: BiSimplex s s
instance IsSimplex ZZ where
  bisimplex :: BiSimplex 'ZZ 'ZZ
bisimplex = BiSimplex 'ZZ 'ZZ
ZZZ
instance (IsSimplex s) => IsSimplex (Y s) where
  bisimplex :: BiSimplex ('Y s) ('Y s)
bisimplex = BiSimplex s s -> BiSimplex ('Y s) ('Y s)
forall {j :: Nat} {j :: Nat} (y :: Simplex j j) (f :: Simplex j j).
BiSimplex y f -> BiSimplex ('Y y) ('Y f)
YYY BiSimplex s s
forall {j :: Nat} {k :: Nat} (s :: Simplex j k).
IsSimplex s =>
BiSimplex s s
bisimplex
instance (IsSimplex s) => IsSimplex (X s) where
  bisimplex :: BiSimplex ('X s) ('X s)
bisimplex = BiSimplex s s -> BiSimplex ('X s) ('X s)
forall {j :: Nat} {y :: Nat} (f :: Simplex j (S y))
       (g :: Simplex j (S y)).
BiSimplex f g -> BiSimplex ('X f) ('X g)
XXX BiSimplex s s
forall {j :: Nat} {k :: Nat} (s :: Simplex j k).
IsSimplex s =>
BiSimplex s s
bisimplex

type LT :: forall j k -> Simplex j k -> Simplex j k -> Constraint
type family LT j k (f :: Simplex j k) (g :: Simplex j k) :: Constraint where
  LT Z Z ZZ ZZ = ()
  LT j (S k) (Y f) (Y g) = LT j k f g
  LT (S j) (S k) (X f) (X g) = LT j (S k) f g

type (f :: Simplex j k) <= g = LT j k f g

type BiSimplex :: CAT (Simplex j k)
data BiSimplex f g where
  ZZZ :: BiSimplex ZZ ZZ
  YYY :: BiSimplex f g -> BiSimplex (Y f) (Y g)
  XXX :: BiSimplex f g -> BiSimplex (X f) (X g)

instance Profunctor BiSimplex where
  dimap :: forall (c :: Simplex j k) (a :: Simplex j k) (b :: Simplex j k)
       (d :: Simplex j k).
(c ~> a) -> (b ~> d) -> BiSimplex a b -> BiSimplex c d
dimap = (c ~> a) -> (b ~> d) -> BiSimplex a b -> BiSimplex c d
BiSimplex c a -> BiSimplex b d -> BiSimplex a b -> BiSimplex 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 :: Simplex j k) (b :: Simplex j k) r.
((Ob a, Ob b) => r) -> BiSimplex a b -> r
\\ BiSimplex a b
ZZZ = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ YYY BiSimplex f g
f = r
(Ob a, Ob b) => r
(Ob f, Ob g) => r
r ((Ob f, Ob g) => r) -> BiSimplex f g -> 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 :: Simplex j k) (b :: Simplex j k) r.
((Ob a, Ob b) => r) -> BiSimplex a b -> r
\\ BiSimplex f g
f
  (Ob a, Ob b) => r
r \\ XXX BiSimplex f g
f = r
(Ob a, Ob b) => r
(Ob f, Ob g) => r
r ((Ob f, Ob g) => r) -> BiSimplex f g -> 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 :: Simplex j (S y)) (b :: Simplex j (S y)) r.
((Ob a, Ob b) => r) -> BiSimplex a b -> r
\\ BiSimplex f g
f
instance Promonad BiSimplex where
  id :: forall a. (Ob a) => BiSimplex a a
  id :: forall (j :: Nat) (k :: Nat) (a :: Simplex j k).
Ob a =>
BiSimplex a a
id = forall (s :: Simplex j k). IsSimplex s => BiSimplex s s
forall {j :: Nat} {k :: Nat} (s :: Simplex j k).
IsSimplex s =>
BiSimplex s s
bisimplex @a
  BiSimplex b c
ZZZ . :: forall (b :: Simplex j k) (c :: Simplex j k) (a :: Simplex j k).
BiSimplex b c -> BiSimplex a b -> BiSimplex a c
. BiSimplex a b
f = BiSimplex a b
BiSimplex a c
f
  YYY BiSimplex f g
f . YYY BiSimplex f g
g = BiSimplex f g -> BiSimplex ('Y f) ('Y g)
forall {j :: Nat} {j :: Nat} (y :: Simplex j j) (f :: Simplex j j).
BiSimplex y f -> BiSimplex ('Y y) ('Y f)
YYY (BiSimplex f g
f BiSimplex f g -> BiSimplex f f -> BiSimplex f g
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 :: Simplex j k) (c :: Simplex j k) (a :: Simplex j k).
BiSimplex b c -> BiSimplex a b -> BiSimplex a c
. BiSimplex f f
BiSimplex f g
g)
  XXX BiSimplex f g
f . XXX BiSimplex f g
g = BiSimplex f g -> BiSimplex ('X f) ('X g)
forall {j :: Nat} {y :: Nat} (f :: Simplex j (S y))
       (g :: Simplex j (S y)).
BiSimplex f g -> BiSimplex ('X f) ('X g)
XXX (BiSimplex f g
f BiSimplex f g -> BiSimplex f f -> BiSimplex f g
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 :: Simplex j (S y)) (c :: Simplex j (S y))
       (a :: Simplex j (S y)).
BiSimplex b c -> BiSimplex a b -> BiSimplex a c
. BiSimplex f f
BiSimplex f g
g)
instance CategoryOf (Simplex j k) where
  type (~>) = BiSimplex
  type Ob a = IsSimplex a