module Proarrow.Category.Instance.Collage where

import Data.Kind (Constraint)

import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , Obj
  , Profunctor (..)
  , Promonad (..)
  , dimapDefault
  , lmap
  , rmap
  , type (+->)
  )
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Preorder.ThinCategory (Codiscrete (..), Thin, ThinProfunctor (..))
import Proarrow.Profunctor.Representable (Representable (..), dimapRep)

type COLLAGE :: forall {j} {k}. k +-> j -> Kind
type data COLLAGE (p :: k +-> j) = L j | R k

type Collage :: CAT (COLLAGE p)
data Collage a b where
  InL :: a ~> b -> Collage (L a :: COLLAGE p) (L b :: COLLAGE p)
  InR :: a ~> b -> Collage (R a :: COLLAGE p) (R b :: COLLAGE p)
  L2R :: p a b -> Collage (L a :: COLLAGE p) (R b :: COLLAGE p)

type IsLR :: forall {p}. COLLAGE p -> Constraint
class IsLR (a :: COLLAGE p) where
  lrId :: Obj a
instance (Ob a, Promonad ((~>) :: CAT k)) => IsLR (L a :: (COLLAGE (p :: j +-> k))) where
  lrId :: Obj (L a)
lrId = (a ~> a) -> Collage (L a) (L a)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
instance (Ob a, Promonad ((~>) :: CAT j)) => IsLR (R a :: (COLLAGE (p :: j +-> k))) where
  lrId :: Obj (R a)
lrId = (a ~> a) -> Collage (R a) (R a)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id

instance (Profunctor p) => Profunctor (Collage :: CAT (COLLAGE p)) where
  dimap :: forall (c :: COLLAGE p) (a :: COLLAGE p) (b :: COLLAGE p)
       (d :: COLLAGE p).
(c ~> a) -> (b ~> d) -> Collage a b -> Collage c d
dimap = (c ~> a) -> (b ~> d) -> Collage a b -> Collage c d
Collage c a -> Collage b d -> Collage a b -> Collage 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 :: COLLAGE p) (b :: COLLAGE p) r.
((Ob a, Ob b) => r) -> Collage a b -> r
\\ InL a ~> b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> 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 ~> b
f
  (Ob a, Ob b) => r
r \\ InR a ~> b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
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
\\ a ~> b
f
  (Ob a, Ob b) => r
r \\ L2R p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

instance (Profunctor p) => Promonad (Collage :: CAT (COLLAGE p)) where
  id :: forall (a :: COLLAGE p). Ob a => Collage a a
id = Obj a
Collage a a
forall {k} {j} {p :: k +-> j} (a :: COLLAGE p). IsLR a => Obj a
lrId
  InL a ~> b
g . :: forall (b :: COLLAGE p) (c :: COLLAGE p) (a :: COLLAGE p).
Collage b c -> Collage a b -> Collage a c
. InL a ~> b
f = (a ~> b) -> Collage (L a) (L b)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL (a ~> b
g (a ~> b) -> (a ~> a) -> a ~> b
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
. a ~> a
a ~> b
f)
  InR a ~> b
g . L2R p a b
p = p a b -> Collage (L a) (R b)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R ((b ~> b) -> p a b -> p a b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap a ~> b
b ~> b
g p a b
p)
  L2R p a b
p . InL a ~> b
f = p a b -> Collage (L a) (R b)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R ((a ~> a) -> p a b -> p a b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> a
a ~> b
f p a b
p)
  InR a ~> b
g . InR a ~> b
f = (a ~> b) -> Collage (R a) (R b)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR (a ~> b
g (a ~> b) -> (a ~> a) -> a ~> b
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
. a ~> a
a ~> b
f)

instance (Profunctor p) => CategoryOf (COLLAGE p) where
  type (~>) = Collage
  type Ob a = IsLR a

instance (HasInitialObject j, CategoryOf k, Codiscrete p) => HasInitialObject (COLLAGE (p :: k +-> j)) where
  type InitialObject = L InitialObject
  initiate' :: forall (a' :: COLLAGE p) (a :: COLLAGE p).
(a' ~> a) -> InitialObject ~> a
initiate' (InL a ~> b
a) = (InitialObject ~> b) -> Collage (L InitialObject) (L b)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL ((a ~> b) -> InitialObject ~> b
forall (a' :: j) (a :: j). (a' ~> a) -> InitialObject ~> a
forall k (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
initiate' a ~> b
a)
  initiate' (L2R p a b
p) = p InitialObject b -> Collage (L InitialObject) (R b)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R p InitialObject b
forall (a :: j) (b :: k). (Ob a, Ob b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Codiscrete p, Ob a, Ob b) =>
p a b
anyArr ((Ob a, Ob b) => Collage (L InitialObject) (R b))
-> p a b -> Collage (L InitialObject) (R b)
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p
  initiate' (InR a ~> b
b) = p InitialObject b -> Collage (L InitialObject) (R b)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R p InitialObject b
forall (a :: j) (b :: k). (Ob a, Ob b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Codiscrete p, Ob a, Ob b) =>
p a b
anyArr ((Ob a, Ob b) => Collage (L InitialObject) (R b))
-> (a ~> b) -> Collage (L InitialObject) (R b)
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
\\ a ~> b
b

instance (HasTerminalObject k, CategoryOf j, Codiscrete p) => HasTerminalObject (COLLAGE (p :: k +-> j)) where
  type TerminalObject = R TerminalObject
  terminate' :: forall (a :: COLLAGE p) (a' :: COLLAGE p).
(a ~> a') -> a ~> TerminalObject
terminate' (InL a ~> b
a) = p a TerminalObject -> Collage (L a) (R TerminalObject)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R p a TerminalObject
forall (a :: j) (b :: k). (Ob a, Ob b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Codiscrete p, Ob a, Ob b) =>
p a b
anyArr ((Ob a, Ob b) => Collage (L a) (R TerminalObject))
-> (a ~> b) -> Collage (L a) (R TerminalObject)
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 ~> b
a
  terminate' (L2R p a b
p) = p a TerminalObject -> Collage (L a) (R TerminalObject)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R p a TerminalObject
forall (a :: j) (b :: k). (Ob a, Ob b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Codiscrete p, Ob a, Ob b) =>
p a b
anyArr ((Ob a, Ob b) => Collage (L a) (R TerminalObject))
-> p a b -> Collage (L a) (R TerminalObject)
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p
  terminate' (InR a ~> b
b) = (a ~> TerminalObject) -> Collage (R a) (R TerminalObject)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR ((a ~> b) -> a ~> TerminalObject
forall (a :: k) (a' :: k). (a ~> a') -> a ~> TerminalObject
forall k (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> a') -> a ~> TerminalObject
terminate' a ~> b
b)

class HasArrowCollage p (a :: COLLAGE p) b where arrCoprod :: a ~> b
instance (Thin j, HasArrow (~>) (a :: j) b, Ob a, Ob b) => HasArrowCollage (p :: k +-> j) (L a) (L b) where
  arrCoprod :: L a ~> L b
arrCoprod = (a ~> b) -> Collage (L a) (L b)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL a ~> b
forall (a :: j) (b :: j). (Ob a, Ob b, HasArrow (~>) a b) => a ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr
instance (ThinProfunctor p, HasArrow p a b, Ob a, Ob b) => HasArrowCollage (p :: k +-> j) (L a) (R b) where
  arrCoprod :: L a ~> R b
arrCoprod = p a b -> Collage (L a) (R b)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R p a b
forall (a :: j) (b :: k). (Ob a, Ob b, HasArrow p a b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr
instance (Thin k, HasArrow (~>) (a :: k) b, Ob a, Ob b) => HasArrowCollage (p :: k +-> j) (R a) (R b) where
  arrCoprod :: R a ~> R b
arrCoprod = (a ~> b) -> Collage (R a) (R b)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR a ~> b
forall (a :: k) (b :: k). (Ob a, Ob b, HasArrow (~>) a b) => a ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr

instance (Thin j, Thin k, ThinProfunctor p) => ThinProfunctor (Collage :: CAT (COLLAGE (p :: k +-> j))) where
  type HasArrow (Collage :: CAT (COLLAGE p)) a b = HasArrowCollage p a b
  arr :: forall (a :: COLLAGE p) (b :: COLLAGE p).
(Ob a, Ob b, HasArrow Collage a b) =>
Collage a b
arr = a ~> b
Collage a b
forall {k} {j} (p :: k +-> j) (a :: COLLAGE p) (b :: COLLAGE p).
HasArrowCollage p a b =>
a ~> b
arrCoprod
  withArr :: forall (a :: COLLAGE p) (b :: COLLAGE p) r.
Collage a b -> (HasArrow Collage a b => r) -> r
withArr (InL a ~> b
f) HasArrow Collage a b => r
r = (a ~> b) -> (HasArrow (~>) a b => r) -> r
forall (a :: j) (b :: j) r.
(a ~> b) -> (HasArrow (~>) a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr a ~> b
f r
HasArrow (~>) a b => r
HasArrow Collage a b => r
r ((Ob a, Ob b) => r) -> (a ~> 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 ~> b
f
  withArr (L2R p a b
p) HasArrow Collage a b => r
r = p a b -> (HasArrow p a b => r) -> r
forall (a :: j) (b :: k) r. p a b -> (HasArrow p a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr p a b
p r
HasArrow p a b => r
HasArrow Collage a b => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p
  withArr (InR a ~> b
f) HasArrow Collage a b => r
r = (a ~> b) -> (HasArrow (~>) a b => r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> (HasArrow (~>) a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr a ~> b
f r
HasArrow (~>) a b => r
HasArrow Collage a b => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
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
\\ a ~> b
f

type InjL :: forall (p :: k +-> j) -> j +-> COLLAGE p
data InjL p a b where
  InjL :: (Ob b) => {forall {j} {k} (b :: j) (p :: k +-> j) (a :: COLLAGE p).
InjL p a b -> a ~> (InjL p % b)
unInL :: a ~> InjL p % b} -> InjL p a b
instance (Profunctor p) => Profunctor (InjL p) where
  dimap :: forall (c :: COLLAGE p) (a :: COLLAGE p) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> InjL p a b -> InjL p c d
dimap = (c ~> a) -> (b ~> d) -> InjL p a b -> InjL p 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 :: COLLAGE p) (b :: k) r.
((Ob a, Ob b) => r) -> InjL p a b -> r
\\ InjL a ~> (InjL p % b)
p = r
(Ob a, Ob b) => r
(Ob a, Ob (L b)) => r
r ((Ob a, Ob (L b)) => r) -> Collage a (L 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
forall (a :: COLLAGE p) (b :: COLLAGE p) r.
((Ob a, Ob b) => r) -> Collage a b -> r
\\ a ~> (InjL p % b)
Collage a (L b)
p
instance (Profunctor p) => Representable (InjL p) where
  type InjL p % a = L a
  index :: forall (a :: COLLAGE p) (b :: j). InjL p a b -> a ~> (InjL p % b)
index (InjL a ~> (InjL p % b)
f) = a ~> (InjL p % b)
f
  tabulate :: forall (b :: j) (a :: COLLAGE p).
Ob b =>
(a ~> (InjL p % b)) -> InjL p a b
tabulate a ~> (InjL p % b)
f = (a ~> (InjL p % b)) -> InjL p a b
forall {j} {k} (b :: j) (p :: k +-> j) (a :: COLLAGE p).
Ob b =>
(a ~> (InjL p % b)) -> InjL p a b
InjL a ~> (InjL p % b)
f ((Ob a, Ob (L b)) => InjL p a b) -> Collage a (L b) -> InjL p a b
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 :: COLLAGE p) (b :: COLLAGE p) r.
((Ob a, Ob b) => r) -> Collage a b -> r
\\ a ~> (InjL p % b)
Collage a (L b)
f
  repMap :: forall (a :: j) (b :: j). (a ~> b) -> (InjL p % a) ~> (InjL p % b)
repMap = (a ~> b) -> (InjL p % a) ~> (InjL p % b)
(a ~> b) -> Collage (L a) (L b)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL

type InjR :: forall (p :: k +-> j) -> k +-> COLLAGE p
data InjR p a b where
  InjR :: (Ob b) => {forall {j} {j} (b :: j) (p :: j +-> j) (a :: COLLAGE p).
InjR p a b -> a ~> (InjR p % b)
unInjR :: a ~> InjR p % b} -> InjR p a b
instance (Profunctor p) => Profunctor (InjR p) where
  dimap :: forall (c :: COLLAGE p) (a :: COLLAGE p) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> InjR p a b -> InjR p c d
dimap = (c ~> a) -> (b ~> d) -> InjR p a b -> InjR p 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 :: COLLAGE p) (b :: k) r.
((Ob a, Ob b) => r) -> InjR p a b -> r
\\ InjR a ~> (InjR p % b)
p = r
(Ob a, Ob b) => r
(Ob a, Ob (R b)) => r
r ((Ob a, Ob (R b)) => r) -> Collage a (R 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
forall (a :: COLLAGE p) (b :: COLLAGE p) r.
((Ob a, Ob b) => r) -> Collage a b -> r
\\ a ~> (InjR p % b)
Collage a (R b)
p
instance (Profunctor p) => Representable (InjR p) where
  type InjR p % a = R a
  index :: forall (a :: COLLAGE p) (b :: j). InjR p a b -> a ~> (InjR p % b)
index (InjR a ~> (InjR p % b)
f) = a ~> (InjR p % b)
f
  tabulate :: forall (b :: j) (a :: COLLAGE p).
Ob b =>
(a ~> (InjR p % b)) -> InjR p a b
tabulate a ~> (InjR p % b)
f = (a ~> (InjR p % b)) -> InjR p a b
forall {j} {j} (b :: j) (p :: j +-> j) (a :: COLLAGE p).
Ob b =>
(a ~> (InjR p % b)) -> InjR p a b
InjR a ~> (InjR p % b)
f ((Ob a, Ob (R b)) => InjR p a b) -> Collage a (R b) -> InjR p a b
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 :: COLLAGE p) (b :: COLLAGE p) r.
((Ob a, Ob b) => r) -> Collage a b -> r
\\ a ~> (InjR p % b)
Collage a (R b)
f
  repMap :: forall (a :: j) (b :: j). (a ~> b) -> (InjR p % a) ~> (InjR p % b)
repMap = (a ~> b) -> (InjR p % a) ~> (InjR p % b)
(a ~> b) -> Collage (R a) (R b)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR