{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The __collage__ (or cograph) of a profunctor @p@: a category on the disjoint union of @p@'s
-- two base categories ('L'- and 'R'-tagged objects, via the kind @'COLLAGE' p@), whose
-- cross-arrows @'L' a '~>' 'R' b@ are the elements @p a b@ (the 'L2R' constructor).
-- The injections 'InjL'\/'InjR' present a profunctor as a single category sitting over the
-- walking arrow 'Proarrow.Category.Instance.Bool.BOOL'.
module Proarrow.Category.Instance.Collage where

import Data.Kind (Constraint)
import Data.List (genericIndex)
import Data.Type.Nat (SNat (..), SNatI, snat, type Plus)
import Prelude (Maybe (..), map, type (~))

import Proarrow.Category.Enriched.Finitary (Finitary (..))
import Proarrow.Category.Enriched.Thin
  ( AtOb (..)
  , CodiscreteProfunctor
  , Decidable
  , DecidableProfunctor (..)
  , Decision (..)
  , DiscreteProfunctor (..)
  , Enumerable (..)
  , Finite (..)
  , FmapWrap
  , Indexed (..)
  , IndexedList (..)
  , KnownIndex
  , Length
  , Lookup
  , MapWrap
  , Thin
  , ThinProfunctor (..)
  , anyArr
  , mapDecision
  , withAtLookup
  , withWrapAtLookup
  )
import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
import Proarrow.Category.Instance.Coproduct qualified as C
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Colimit.Initial (HasInitialObject (..), initiate')
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Hom
  , Kind
  , Obj
  , Profunctor (..)
  , Promonad (..)
  , dimapDefault
  , lmap
  , obj
  , rmap
  , type (+->)
  )
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..), terminate')
import Proarrow.Optic (iso)
import Proarrow.Optic.Iso (Iso')
import Proarrow.Profunctor.Instance.Direp (Direp (..))

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 :: CAT 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 :: CAT 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 :: CAT 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 :: j +-> k) (a :: k) (b :: j) 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 :: j +-> k) (a :: k) (b :: j) 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 :: j +-> k) (a :: k) (b :: j) 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 :: CAT 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 (b :: k) (d :: k) (a :: j). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
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 (c :: j) (a :: j) (b :: k). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a
a ~> b
f)

-- | The collage of a profunctor.
instance (Profunctor p) => CategoryOf (COLLAGE p) where
  type (~>) = Collage
  type Ob a = IsLR a

instance (HasInitialObject j, CategoryOf k, CodiscreteProfunctor p) => HasInitialObject (COLLAGE (p :: k +-> j)) where
  type InitialObject = L InitialObject
  initiate :: forall (a :: COLLAGE p). Ob a => InitialObject ~> a
initiate @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COLLAGE p). (CategoryOf (COLLAGE p), Ob a) => Obj a
obj @a of
    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 ((b ~> b) -> InitialObject ~> b
forall {k} (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
initiate' a ~> b
b ~> b
a)
    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).
(CodiscreteProfunctor p, Ob a, Ob b) =>
p a b
anyArr ((Ob b, Ob b) => Collage (L InitialObject) (R b))
-> (b ~> b) -> Collage (L InitialObject) (R b)
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
\\ a ~> b
b ~> b
b

instance (HasTerminalObject k, CategoryOf j, CodiscreteProfunctor p) => HasTerminalObject (COLLAGE (p :: k +-> j)) where
  type TerminalObject = R TerminalObject
  terminate :: forall (a :: COLLAGE p). Ob a => a ~> TerminalObject
terminate @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COLLAGE p). (CategoryOf (COLLAGE p), Ob a) => Obj a
obj @a of
    InL a ~> b
a -> p b TerminalObject -> Collage (L b) (R TerminalObject)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R p b TerminalObject
forall (a :: j) (b :: k). (Ob a, Ob b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(CodiscreteProfunctor p, Ob a, Ob b) =>
p a b
anyArr ((Ob b, Ob b) => Collage (L b) (R TerminalObject))
-> (b ~> b) -> Collage (L b) (R TerminalObject)
forall (a :: j) (b :: j) 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
\\ a ~> b
b ~> b
a
    InR a ~> b
b -> (b ~> TerminalObject) -> Collage (R b) (R TerminalObject)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR ((b ~> b) -> b ~> TerminalObject
forall {k} (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> a') -> a ~> TerminalObject
terminate' a ~> b
b ~> 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, Ob a, Ob b) => r) -> r
withArr (InL a ~> b
f) (HasArrow Collage a b, Ob a, Ob b) => r
r = (a ~> b) -> ((HasArrow (Hom j) a b, Ob a, Ob b) => r) -> r
forall (a :: j) (b :: j) r.
(a ~> b) -> ((HasArrow (Hom j) a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr a ~> b
f r
(HasArrow (Hom j) a b, Ob a, Ob b) => r
(HasArrow Collage a b, 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 :: j +-> k) (a :: k) (b :: j) 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, Ob a, Ob b) => r
r = p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall (a :: j) (b :: k) r.
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr p a b
p r
(HasArrow p a b, Ob a, Ob b) => r
(HasArrow Collage a b, 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 :: j +-> k) (a :: k) (b :: j) 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, Ob a, Ob b) => r
r = (a ~> b) -> ((HasArrow (Hom k) a b, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> ((HasArrow (Hom k) a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr a ~> b
f r
(HasArrow (Hom k) a b, Ob a, Ob b) => r
(HasArrow Collage a b, 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

-- | Decided piecewise: within either side by that side's order, across by @p@, and never backwards.
instance
  (Decidable j, Decidable k, DecidableProfunctor p)
  => DecidableProfunctor (Collage :: CAT (COLLAGE (p :: k +-> j)))
  where
  type Holds (Collage :: CAT (COLLAGE (p :: k +-> j))) (L a) (L b) = Holds (Hom j) a b
  type Holds (Collage :: CAT (COLLAGE (p :: k +-> j))) (L a) (R b) = Holds p a b
  type Holds (Collage :: CAT (COLLAGE (p :: k +-> j))) (R a) (L b) = FLS
  type Holds (Collage :: CAT (COLLAGE (p :: k +-> j))) (R a) (R b) = Holds (Hom k) a b
  decide :: forall (a :: COLLAGE p) (b :: COLLAGE p).
(Ob a, Ob b) =>
Decision Collage a b (Holds Collage a b)
decide @x @y = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COLLAGE p). (CategoryOf (COLLAGE p), Ob a) => Obj a
obj @x, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COLLAGE p). (CategoryOf (COLLAGE p), Ob a) => Obj a
obj @y) of
    (InL @a a ~> b
f, InL @b a ~> b
g) -> ((a ~> a) -> Collage (L b) (L b))
-> Decision (Hom j) a a (Holds (Hom j) b b)
-> Decision Collage (L b) (L b) (Holds (Hom j) b b)
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision (a ~> a) -> Collage (L b) (L b)
(b ~> b) -> Collage (L b) (L b)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> j) (a :: j) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @(Hom j) @a @b) ((Ob b, Ob b) => Decision Collage (L b) (L b) (Holds (Hom j) b b))
-> (b ~> b) -> Decision Collage (L b) (L b) (Holds (Hom j) b b)
forall (a :: j) (b :: j) 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
\\ a ~> b
b ~> b
f ((Ob b, Ob b) => Decision Collage (L b) (L b) (Holds (Hom j) b b))
-> (b ~> b) -> Decision Collage (L b) (L b) (Holds (Hom j) b b)
forall (a :: j) (b :: j) 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
\\ a ~> b
b ~> b
g
    (InL @a a ~> b
f, InR @b a ~> b
g) -> (p a a -> Collage (L a) (R a))
-> Decision p a a (Holds p b b)
-> Decision Collage (L a) (R a) (Holds p b b)
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision p a a -> Collage (L a) (R a)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: k +-> j) (a :: j) (b :: k).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @b) ((Ob b, Ob b) => Decision Collage (L b) (R b) (Holds p b b))
-> (b ~> b) -> Decision Collage (L b) (R b) (Holds p b b)
forall (a :: j) (b :: j) 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
\\ a ~> b
b ~> b
f ((Ob b, Ob b) => Decision Collage (L b) (R b) (Holds p b b))
-> (b ~> b) -> Decision Collage (L b) (R b) (Holds p b b)
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
\\ a ~> b
b ~> b
g
    (InR a ~> b
_, InL a ~> b
_) -> Decision Collage a b 'FLS
Decision Collage a b (Holds Collage a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
    (InR @a a ~> b
f, InR @b a ~> b
g) -> ((a ~> a) -> Collage (R b) (R b))
-> Decision (Hom k) a a (Holds (Hom k) b b)
-> Decision Collage (R b) (R b) (Holds (Hom k) b b)
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision (a ~> a) -> Collage (R b) (R b)
(b ~> b) -> Collage (R b) (R b)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: k +-> k) (a :: k) (b :: k).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @(Hom k) @a @b) ((Ob b, Ob b) => Decision Collage (R b) (R b) (Holds (Hom k) b b))
-> (b ~> b) -> Decision Collage (R b) (R b) (Holds (Hom k) b b)
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
\\ a ~> b
b ~> b
f ((Ob b, Ob b) => Decision Collage (R b) (R b) (Holds (Hom k) b b))
-> (b ~> b) -> Decision Collage (R b) (R b) (Holds (Hom k) b b)
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
\\ a ~> b
b ~> b
g
  toHolds :: forall (a :: COLLAGE p) (b :: COLLAGE p) r.
Collage a b -> ((Holds Collage a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds (InL a ~> b
f) (Holds Collage a b ~ 'TRU, Ob a, Ob b) => r
r = (a ~> b) -> ((Holds (Hom j) a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall (a :: j) (b :: j) r.
(a ~> b) -> ((Holds (Hom j) a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds a ~> b
f r
(Holds (Hom j) a b ~ 'TRU, Ob a, Ob b) => r
(Holds Collage a b ~ 'TRU, Ob a, Ob b) => r
r
  toHolds (L2R p a b
p) (Holds Collage a b ~ 'TRU, Ob a, Ob b) => r
r = p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall (a :: j) (b :: k) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds p a b
p r
(Holds p a b ~ 'TRU, Ob a, Ob b) => r
(Holds Collage a b ~ 'TRU, Ob a, Ob b) => r
r
  toHolds (InR a ~> b
f) (Holds Collage a b ~ 'TRU, Ob a, Ob b) => r
r = (a ~> b) -> ((Holds (Hom k) a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> ((Holds (Hom k) a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds a ~> b
f r
(Holds (Hom k) a b ~ 'TRU, Ob a, Ob b) => r
(Holds Collage a b ~ 'TRU, Ob a, Ob b) => r
r

data family InjL :: forall (p :: k +-> j) -> j +-> COLLAGE p
instance (Profunctor p) => FunctorForRep (InjL p) where
  type InjL p @ a = L a
  fmap :: forall (a :: j) (b :: j). (a ~> b) -> (InjL p @ a) ~> (InjL p @ b)
fmap = (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

data family InjR :: forall (p :: k +-> j) -> k +-> COLLAGE p
instance (Profunctor p) => FunctorForRep (InjR p) where
  type InjR p @ a = R a
  fmap :: forall (a :: j) (b :: j). (a ~> b) -> (InjR p @ a) ~> (InjR p @ b)
fmap = (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

collageUniv :: forall {j} {k} (p :: k +-> j). (Profunctor p) => Iso' p (Direp (InjL p) (InjR p))
collageUniv :: forall {j} {k} (p :: k +-> j).
Profunctor p =>
Iso' p (Direp (InjL p) (InjR p))
collageUniv = (p ~> Direp (InjL p) (InjR p))
-> (Direp (InjL p) (InjR p) ~> p)
-> Optic
     (Prostrong IsoFl)
     p
     p
     (Direp (InjL p) (InjR p))
     (Direp (InjL p) (InjR p))
forall {j} {k} (c :: (j +-> k) -> Constraint) (s :: k) (t :: j)
       (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Optic c s t a b
iso ((p :~> Direp (InjL p) (InjR p)) -> Prof p (Direp (InjL p) (InjR p))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \p a b
p -> ((InjL p @ a) ~> (InjR p @ b)) -> Direp (InjL p) (InjR p) a b
forall {j} {i} {k} (a :: j) (b :: i) (f :: j +-> k) (g :: i +-> k).
(Ob a, Ob b) =>
((f @ a) ~> (g @ b)) -> Direp f g a b
Direp (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
p) ((Ob a, Ob b) => Direp (InjL p) (InjR p) a b)
-> p a b -> Direp (InjL p) (InjR p) a b
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p) ((Direp (InjL p) (InjR p) :~> p) -> Prof (Direp (InjL p) (InjR p)) p
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \case Direp (L2R p a b
q) -> p a b
p a b
q)

data family CollageAsCoprod :: COLLAGE (p :: k +-> j) +-> C.COPRODUCT j k
instance (DiscreteProfunctor p) => FunctorForRep (CollageAsCoprod :: COLLAGE (p :: k +-> j) +-> C.COPRODUCT j k) where
  type CollageAsCoprod @ L a = C.L a
  type CollageAsCoprod @ R a = C.R a
  fmap :: forall (a :: COLLAGE p) (b :: COLLAGE p).
(a ~> b) -> (CollageAsCoprod @ a) ~> (CollageAsCoprod @ b)
fmap (InL a ~> b
f) = (a ~> b) -> (:++:) (~>) (~>) (L a) (L b)
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (q :: j2 +-> k2).
p a1 b1 -> (:++:) p q (L a1) (L b1)
C.InjL a ~> b
f
  fmap (InR a ~> b
f) = (a ~> b) -> (:++:) (~>) (~>) (R a) (R b)
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a1 :: k2) (b1 :: j2)
       (p :: j1 +-> k1).
q a1 b1 -> (:++:) p q (R a1) (R b1)
C.InjR a ~> b
f
  fmap (L2R p a b
p) = p a b -> (:++:) (~>) (~>) (L a) (R b)
forall (a :: j) (b :: k) r. p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DiscreteProfunctor p =>
p a b -> r
exfalso p a b
p

data family ProjTo2 :: forall (p :: k +-> j) -> COLLAGE p +-> BOOL
instance (Profunctor p) => FunctorForRep (ProjTo2 p) where
  type ProjTo2 p @ L a = FLS
  type ProjTo2 p @ R a = TRU
  fmap :: forall (a :: COLLAGE p) (b :: COLLAGE p).
(a ~> b) -> (ProjTo2 p @ a) ~> (ProjTo2 p @ b)
fmap = \case
    InL a ~> b
_ -> (ProjTo2 p @ a) ~> (ProjTo2 p @ b)
Booleans 'FLS 'FLS
Fls
    InR a ~> b
_ -> (ProjTo2 p @ a) ~> (ProjTo2 p @ b)
Booleans 'TRU 'TRU
Tru
    L2R p a b
_ -> (ProjTo2 p @ a) ~> (ProjTo2 p @ b)
Booleans 'FLS 'TRU
F2T

-- * Numbering the collage

-- | The collage numbers the left category's objects first and the right category's after them.
type CollageObjects :: forall {j} {k}. forall (p :: k +-> j) -> [j] -> [COLLAGE p]
type family CollageObjects p xs where
  CollageObjects (p :: k +-> j) '[] = MapWrap R (Objects k)
  CollageObjects p (x ': xs) = L x ': CollageObjects p xs

instance (Finite j, Finite k) => Indexed (COLLAGE (p :: k +-> j)) where
  type Index (L a) = Index a
  type Index (R b :: COLLAGE (p :: k +-> j)) = Plus (Length (Objects j)) (Index b)

-- | An object of the left category is an object of the collage, keeping its index; one of the right
-- category is too, shifted past all the left ones. Both walk the left object list, and both hand the
-- fact to a continuation, since at each step the statement about the tail is the statement about the
-- whole list already reduced.
withCollageL
  :: forall {j} {k} (p :: k +-> j) (x :: j) r
   . (Finite j, Finite k, KnownIndex x)
  => ((KnownIndex (L x :: COLLAGE p)) => r) -> r
withCollageL :: forall {j} {k} (p :: k +-> j) (x :: j) r.
(Finite j, Finite k, KnownIndex x) =>
(KnownIndex (L x) => r) -> r
withCollageL KnownIndex (L x) => r
r = forall k (i :: Nat) r.
Finite k =>
SNat i -> ((Lookup (Objects k) i ~ At k i) => r) -> r
withAtLookup @j (forall (n :: Nat). SNatI n => SNat n
snat @(Index x)) (IndexedList (Objects j)
-> SNat (Index x)
-> ((Lookup (CollageObjects p (Objects j)) (Index x)
     ~ 'Just (L x)) =>
    r)
-> r
forall (xs :: [j]) (i :: Nat).
(Lookup xs i ~ 'Just x) =>
IndexedList xs
-> SNat i
-> ((Lookup (CollageObjects p xs) i ~ 'Just (L x)) => r)
-> r
go (forall k. Finite k => IndexedList (Objects k)
finite @j) (forall (n :: Nat). SNatI n => SNat n
snat @(Index x)) r
(Lookup (CollageObjects p (Objects j)) (Index x) ~ 'Just (L x)) =>
r
KnownIndex (L x) => r
r)
  where
    go
      :: forall xs i
       . (Lookup xs i ~ 'Just x)
      => IndexedList xs -> SNat i -> ((Lookup (CollageObjects p xs) i ~ 'Just (L x)) => r) -> r
    go :: forall (xs :: [j]) (i :: Nat).
(Lookup xs i ~ 'Just x) =>
IndexedList xs
-> SNat i
-> ((Lookup (CollageObjects p xs) i ~ 'Just (L x)) => r)
-> r
go (FCons IndexedList as1
_) SNat i
SZ (Lookup (CollageObjects p xs) i ~ 'Just (L x)) => r
k = r
(Lookup (CollageObjects p xs) i ~ 'Just (L x)) => r
k
    go (FCons IndexedList as1
xs) (SS @i') (Lookup (CollageObjects p xs) i ~ 'Just (L x)) => r
k = IndexedList as1
-> SNat n1
-> ((Lookup (CollageObjects p as1) n1 ~ 'Just (L x)) => r)
-> r
forall (xs :: [j]) (i :: Nat).
(Lookup xs i ~ 'Just x) =>
IndexedList xs
-> SNat i
-> ((Lookup (CollageObjects p xs) i ~ 'Just (L x)) => r)
-> r
go IndexedList as1
xs (forall (n :: Nat). SNatI n => SNat n
snat @i') r
(Lookup (CollageObjects p xs) i ~ 'Just (L x)) => r
(Lookup (CollageObjects p as1) n1 ~ 'Just (L x)) => r
k

withCollageR
  :: forall {j} {k} (p :: k +-> j) (y :: k) r
   . (Finite j, Finite k, KnownIndex y)
  => ((KnownIndex (R y :: COLLAGE p)) => r) -> r
withCollageR :: forall {j} {k} (p :: k +-> j) (y :: k) r.
(Finite j, Finite k, KnownIndex y) =>
(KnownIndex (R y) => r) -> r
withCollageR KnownIndex (R y) => r
r = IndexedList (Objects j)
-> ((SNatI (Plus (Length (Objects j)) (Index y)),
     Lookup
       (CollageObjects p (Objects j))
       (Plus (Length (Objects j)) (Index y))
     ~ FmapWrap R (At k (Index y))) =>
    r)
-> r
forall (xs :: [j]).
IndexedList xs
-> ((SNatI (Plus (Length xs) (Index y)),
     Lookup (CollageObjects p xs) (Plus (Length xs) (Index y))
     ~ FmapWrap R (At k (Index y))) =>
    r)
-> r
go (forall k. Finite k => IndexedList (Objects k)
finite @j) r
(SNatI (Plus (Length (Objects j)) (Index y)),
 Lookup
   (CollageObjects p (Objects j))
   (Plus (Length (Objects j)) (Index y))
 ~ FmapWrap R (At k (Index y))) =>
r
KnownIndex (R y) => r
r
  where
    go
      :: forall xs
       . IndexedList xs
      -> ( ( SNatI (Plus (Length xs) (Index y))
           , Lookup (CollageObjects p xs) (Plus (Length xs) (Index y)) ~ FmapWrap R (At k (Index y))
           )
           => r
         )
      -> r
    go :: forall (xs :: [j]).
IndexedList xs
-> ((SNatI (Plus (Length xs) (Index y)),
     Lookup (CollageObjects p xs) (Plus (Length xs) (Index y))
     ~ FmapWrap R (At k (Index y))) =>
    r)
-> r
go IndexedList xs
FNil (SNatI (Plus (Length xs) (Index y)),
 Lookup (CollageObjects p xs) (Plus (Length xs) (Index y))
 ~ FmapWrap R (At k (Index y))) =>
r
k = forall {j} {k} (w :: j -> k) (i :: Nat) r.
Finite j =>
SNat i
-> ((Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r)
-> r
forall (w :: k -> COLLAGE p) (i :: Nat) r.
Finite k =>
SNat i
-> ((Lookup (MapWrap w (Objects k)) i ~ FmapWrap w (At k i)) => r)
-> r
withWrapAtLookup @(R :: k -> COLLAGE p) (forall (n :: Nat). SNatI n => SNat n
snat @(Index y)) r
(Lookup (MapWrap R (Objects k)) (Index y)
 ~ FmapWrap R (At k (Index y))) =>
r
(SNatI (Plus (Length xs) (Index y)),
 Lookup (CollageObjects p xs) (Plus (Length xs) (Index y))
 ~ FmapWrap R (At k (Index y))) =>
r
k
    go (FCons IndexedList as1
xs) (SNatI (Plus (Length xs) (Index y)),
 Lookup (CollageObjects p xs) (Plus (Length xs) (Index y))
 ~ FmapWrap R (At k (Index y))) =>
r
k = IndexedList as1
-> ((SNatI (Plus (Length as1) (Index y)),
     Lookup (CollageObjects p as1) (Plus (Length as1) (Index y))
     ~ FmapWrap R (At k (Index y))) =>
    r)
-> r
forall (xs :: [j]).
IndexedList xs
-> ((SNatI (Plus (Length xs) (Index y)),
     Lookup (CollageObjects p xs) (Plus (Length xs) (Index y))
     ~ FmapWrap R (At k (Index y))) =>
    r)
-> r
go IndexedList as1
xs r
(SNatI (Plus (Length xs) (Index y)),
 Lookup (CollageObjects p xs) (Plus (Length xs) (Index y))
 ~ FmapWrap R (At k (Index y))) =>
r
(SNatI (Plus (Length as1) (Index y)),
 Lookup (CollageObjects p as1) (Plus (Length as1) (Index y))
 ~ FmapWrap R (At k (Index y))) =>
r
k

instance (Finite j, Finite k) => Finite (COLLAGE (p :: k +-> j)) where
  type Objects (COLLAGE (p :: k +-> j)) = CollageObjects p (Objects j)
  finite :: IndexedList (Objects (COLLAGE p))
finite = IndexedList (Objects j)
-> IndexedList (CollageObjects p (Objects j))
forall (xs :: [j]).
IndexedList xs -> IndexedList (CollageObjects p xs)
goL (forall k. Finite k => IndexedList (Objects k)
finite @j)
    where
      goL :: forall xs. IndexedList xs -> IndexedList (CollageObjects p xs)
      goL :: forall (xs :: [j]).
IndexedList xs -> IndexedList (CollageObjects p xs)
goL IndexedList xs
FNil = IndexedList (Objects k) -> IndexedList (MapWrap R (Objects k))
forall (ys :: [k]). IndexedList ys -> IndexedList (MapWrap R ys)
goR (forall k. Finite k => IndexedList (Objects k)
finite @k)
      goL (FCons @x IndexedList as1
xs) = forall {j} {k} (p :: k +-> j) (x :: j) r.
(Finite j, Finite k, KnownIndex x) =>
(KnownIndex (L x) => r) -> r
forall (p :: k +-> j) (x :: j) r.
(Finite j, Finite k, KnownIndex x) =>
(KnownIndex (L x) => r) -> r
withCollageL @p @x (forall {k} (a :: k) (as1 :: [k]).
KnownIndex a =>
IndexedList as1 -> IndexedList (a : as1)
forall (a :: COLLAGE p) (as1 :: [COLLAGE p]).
KnownIndex a =>
IndexedList as1 -> IndexedList (a : as1)
FCons @(L x) (IndexedList as1 -> IndexedList (CollageObjects p as1)
forall (xs :: [j]).
IndexedList xs -> IndexedList (CollageObjects p xs)
goL IndexedList as1
xs))
      goR :: forall ys. IndexedList ys -> IndexedList (MapWrap (R :: k -> COLLAGE p) ys)
      goR :: forall (ys :: [k]). IndexedList ys -> IndexedList (MapWrap R ys)
goR IndexedList ys
FNil = IndexedList '[]
IndexedList (MapWrap R ys)
forall {k}. IndexedList '[]
FNil
      goR (FCons @y IndexedList as1
ys) = forall {j} {k} (p :: k +-> j) (y :: k) r.
(Finite j, Finite k, KnownIndex y) =>
(KnownIndex (R y) => r) -> r
forall (p :: k +-> j) (y :: k) r.
(Finite j, Finite k, KnownIndex y) =>
(KnownIndex (R y) => r) -> r
withCollageR @p @y (forall {k} (a :: k) (as1 :: [k]).
KnownIndex a =>
IndexedList as1 -> IndexedList (a : as1)
forall (a :: COLLAGE p) (as1 :: [COLLAGE p]).
KnownIndex a =>
IndexedList as1 -> IndexedList (a : as1)
FCons @(R y) (IndexedList as1 -> IndexedList (MapWrap R as1)
forall (ys :: [k]). IndexedList ys -> IndexedList (MapWrap R ys)
goR IndexedList as1
ys))

-- | The collage of a finitary profunctor between finite categories is a finite category: a
-- hom-set is a base hom-set, an element set of @p@ for a cross-arrow, or empty going back.
--
-- This is the cheapest source of a finite category that is /not a poset/: elements of @p@
-- between one pair of objects are parallel arrows.
instance
  (Finitary (Hom j), Finitary (Hom k), Finitary p)
  => Finitary (Collage :: CAT (COLLAGE (p :: k +-> j)))
  where
  size :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => Natural
size @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COLLAGE p). (CategoryOf (COLLAGE p), Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COLLAGE p). (CategoryOf (COLLAGE p), Ob a) => Obj a
obj @b) of
    (InL @x a ~> b
f, InL @y a ~> b
g) -> forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural
forall (p :: j +-> j) (a :: j) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural
size @(Hom j) @x @y ((Ob b, Ob b) => Natural) -> (b ~> b) -> Natural
forall (a :: j) (b :: j) 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
\\ a ~> b
b ~> b
f ((Ob b, Ob b) => Natural) -> (b ~> b) -> Natural
forall (a :: j) (b :: j) 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
\\ a ~> b
b ~> b
g
    (InL @x a ~> b
f, InR @y a ~> b
g) -> forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural
forall (p :: k +-> j) (a :: j) (b :: k).
(Finitary p, Ob a, Ob b) =>
Natural
size @p @x @y ((Ob b, Ob b) => Natural) -> (b ~> b) -> Natural
forall (a :: j) (b :: j) 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
\\ a ~> b
b ~> b
f ((Ob b, Ob b) => Natural) -> (b ~> b) -> Natural
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
\\ a ~> b
b ~> b
g
    (InR a ~> b
_, InL a ~> b
_) -> Natural
0
    (InR @x a ~> b
f, InR @y a ~> b
g) -> forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural
forall (p :: k +-> k) (a :: k) (b :: k).
(Finitary p, Ob a, Ob b) =>
Natural
size @(Hom k) @x @y ((Ob b, Ob b) => Natural) -> (b ~> b) -> Natural
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
\\ a ~> b
b ~> b
f ((Ob b, Ob b) => Natural) -> (b ~> b) -> Natural
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
\\ a ~> b
b ~> b
g
  toIndex :: forall (a :: COLLAGE p) (b :: COLLAGE p).
(Ob a, Ob b) =>
Collage a b -> Natural
toIndex = \case
    InL a ~> b
f -> (a ~> b) -> Natural
forall (a :: j) (b :: j). (Ob a, Ob b) => (a ~> b) -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex a ~> b
f ((Ob a, Ob b) => Natural) -> (a ~> b) -> Natural
forall (a :: j) (b :: j) 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
\\ a ~> b
f
    InR a ~> b
f -> (a ~> b) -> Natural
forall (a :: k) (b :: k). (Ob a, Ob b) => (a ~> b) -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex a ~> b
f ((Ob a, Ob b) => Natural) -> (a ~> b) -> Natural
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
\\ a ~> b
f
    L2R p a b
x -> p a b -> Natural
forall (a :: j) (b :: k). (Ob a, Ob b) => p a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex p a b
x ((Ob a, Ob b) => Natural) -> p a b -> Natural
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
x
  fromIndex :: forall (a :: COLLAGE p) (b :: COLLAGE p).
(Ob a, Ob b) =>
Natural -> Collage a b
fromIndex @a @b = [Collage a b] -> Natural -> Collage a b
forall i a. Integral i => [a] -> i -> a
genericIndex (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: COLLAGE p +-> COLLAGE p) (a :: COLLAGE p)
       (b :: COLLAGE p).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @(Collage :: CAT (COLLAGE p)) @a @b)
  elements :: forall (a :: COLLAGE p) (b :: COLLAGE p).
(Ob a, Ob b) =>
[Collage a b]
elements @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COLLAGE p). (CategoryOf (COLLAGE p), Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COLLAGE p). (CategoryOf (COLLAGE p), Ob a) => Obj a
obj @b) of
    (InL @x a ~> b
f, InL @y a ~> b
g) -> ((b ~> b) -> Collage a b) -> [b ~> b] -> [Collage a b]
forall a b. (a -> b) -> [a] -> [b]
map (b ~> b) -> Collage a b
(b ~> b) -> Collage (L b) (L b)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: j +-> j) (a :: j) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @(Hom j) @x @y) ((Ob b, Ob b) => [Collage a b]) -> (b ~> b) -> [Collage a b]
forall (a :: j) (b :: j) 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
\\ a ~> b
b ~> b
f ((Ob b, Ob b) => [Collage a b]) -> (b ~> b) -> [Collage a b]
forall (a :: j) (b :: j) 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
\\ a ~> b
b ~> b
g
    (InL @x a ~> b
f, InR @y a ~> b
g) -> (p a a -> Collage a b) -> [p a a] -> [Collage a b]
forall a b. (a -> b) -> [a] -> [b]
map p a a -> Collage a b
p a a -> Collage (L a) (R a)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: k +-> j) (a :: j) (b :: k).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @p @x @y) ((Ob b, Ob b) => [Collage a b]) -> (b ~> b) -> [Collage a b]
forall (a :: j) (b :: j) 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
\\ a ~> b
b ~> b
f ((Ob b, Ob b) => [Collage a b]) -> (b ~> b) -> [Collage a b]
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
\\ a ~> b
b ~> b
g
    (InR a ~> b
_, InL a ~> b
_) -> []
    (InR @x a ~> b
f, InR @y a ~> b
g) -> ((b ~> b) -> Collage a b) -> [b ~> b] -> [Collage a b]
forall a b. (a -> b) -> [a] -> [b]
map (b ~> b) -> Collage a b
(b ~> b) -> Collage (R b) (R b)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: k +-> k) (a :: k) (b :: k).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @(Hom k) @x @y) ((Ob b, Ob b) => [Collage a b]) -> (b ~> b) -> [Collage a b]
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
\\ a ~> b
b ~> b
f ((Ob b, Ob b) => [Collage a b]) -> (b ~> b) -> [Collage a b]
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
\\ a ~> b
b ~> b
g

instance (Enumerable j, Enumerable k, Profunctor p) => Enumerable (COLLAGE (p :: k +-> j)) where
  withIndex :: forall (a :: COLLAGE p) r. Ob a => (KnownIndex a => r) -> r
withIndex @a KnownIndex a => r
r = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COLLAGE p). (CategoryOf (COLLAGE p), Ob a) => Obj a
obj @a of
    InL @x a ~> b
f -> forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
withIndex @j @x (forall {j} {k} (p :: k +-> j) (x :: j) r.
(Finite j, Finite k, KnownIndex x) =>
(KnownIndex (L x) => r) -> r
forall (p :: k +-> j) (x :: j) r.
(Finite j, Finite k, KnownIndex x) =>
(KnownIndex (L x) => r) -> r
withCollageL @p @x r
KnownIndex a => r
KnownIndex (L a) => r
r) ((Ob b, Ob b) => r) -> (b ~> b) -> r
forall (a :: j) (b :: j) 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
\\ a ~> b
b ~> b
f
    InR @y a ~> b
f -> forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
withIndex @k @y (forall {j} {k} (p :: k +-> j) (y :: k) r.
(Finite j, Finite k, KnownIndex y) =>
(KnownIndex (R y) => r) -> r
forall (p :: k +-> j) (y :: k) r.
(Finite j, Finite k, KnownIndex y) =>
(KnownIndex (R y) => r) -> r
withCollageR @p @y r
KnownIndex a => r
KnownIndex (R a) => r
r) ((Ob b, Ob b) => r) -> (b ~> b) -> r
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
\\ a ~> b
b ~> b
f
  atOb :: forall (i :: Nat). SNat i -> AtOb (COLLAGE p) (At (COLLAGE p) i)
atOb = IndexedList (Objects j)
-> SNat i
-> AtOb (COLLAGE p) (Lookup (CollageObjects p (Objects j)) i)
forall (xs :: [j]) (i :: Nat).
IndexedList xs
-> SNat i -> AtOb (COLLAGE p) (Lookup (CollageObjects p xs) i)
go (forall k. Finite k => IndexedList (Objects k)
finite @j)
    where
      go :: forall xs i. IndexedList xs -> SNat i -> AtOb (COLLAGE p) (Lookup (CollageObjects p xs) i)
      go :: forall (xs :: [j]) (i :: Nat).
IndexedList xs
-> SNat i -> AtOb (COLLAGE p) (Lookup (CollageObjects p xs) i)
go IndexedList xs
FNil SNat i
i = forall {j} {k} (w :: j -> k) (i :: Nat) r.
Finite j =>
SNat i
-> ((Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r)
-> r
forall (w :: k -> COLLAGE p) (i :: Nat) r.
Finite k =>
SNat i
-> ((Lookup (MapWrap w (Objects k)) i ~ FmapWrap w (At k i)) => r)
-> r
withWrapAtLookup @(R :: k -> COLLAGE p) SNat i
i case forall k (i :: Nat). Enumerable k => SNat i -> AtOb k (At k i)
atOb @k SNat i
i of
        AtJust @_ @y -> forall {j} {k} (p :: k +-> j) (y :: k) r.
(Finite j, Finite k, KnownIndex y) =>
(KnownIndex (R y) => r) -> r
forall (p :: k +-> j) (y :: k) r.
(Finite j, Finite k, KnownIndex y) =>
(KnownIndex (R y) => r) -> r
withCollageR @p @y AtOb (COLLAGE p) ('Just (R a))
AtOb (COLLAGE p) (Lookup (MapWrap R (Objects k)) i)
KnownIndex (R a) =>
AtOb (COLLAGE p) (Lookup (MapWrap R (Objects k)) i)
forall k (a :: k). (Ob a, KnownIndex a) => AtOb k ('Just a)
AtJust
        AtOb k (At k i)
AtNothing -> AtOb (COLLAGE p) 'Nothing
AtOb (COLLAGE p) (Lookup (MapWrap R (Objects k)) i)
forall k. AtOb k 'Nothing
AtNothing
      go (FCons @x IndexedList as1
_) SNat i
SZ = forall k (a :: k) r.
(Enumerable k, KnownIndex a) =>
(Ob a => r) -> r
withOb @j @x (forall {j} {k} (p :: k +-> j) (x :: j) r.
(Finite j, Finite k, KnownIndex x) =>
(KnownIndex (L x) => r) -> r
forall (p :: k +-> j) (x :: j) r.
(Finite j, Finite k, KnownIndex x) =>
(KnownIndex (L x) => r) -> r
withCollageL @p @x AtOb (COLLAGE p) ('Just (L a))
KnownIndex (L a) => AtOb (COLLAGE p) ('Just (L a))
forall k (a :: k). (Ob a, KnownIndex a) => AtOb k ('Just a)
AtJust)
      go (FCons IndexedList as1
xs) (SS @i') = IndexedList as1
-> SNat n1 -> AtOb (COLLAGE p) (Lookup (CollageObjects p as1) n1)
forall (xs :: [j]) (i :: Nat).
IndexedList xs
-> SNat i -> AtOb (COLLAGE p) (Lookup (CollageObjects p xs) i)
go IndexedList as1
xs (forall (n :: Nat). SNatI n => SNat n
snat @i')