Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Collage

Contents

Numbering the collage

Description

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 BOOL.

Synopsis

data COLLAGE (p :: k +-> j)
- = L j
- | R k
data Collage (a :: COLLAGE p) (b :: COLLAGE p) where
- InL :: forall {j} {k} (a1 :: j) (b1 :: j) (p :: k +-> j). (a1 ~> b1) -> Collage ('L a1 :: COLLAGE p) ('L b1 :: COLLAGE p)
- InR :: forall {k} {j} (a1 :: k) (b1 :: k) (p :: k +-> j). (a1 ~> b1) -> Collage ('R a1 :: COLLAGE p) ('R b1 :: COLLAGE p)
- L2R :: forall {k} {j} (p :: k +-> j) (a1 :: j) (b1 :: k). p a1 b1 -> Collage ('L a1 :: COLLAGE p) ('R b1 :: COLLAGE p)
class IsLR (a :: COLLAGE p) where
- lrId :: Obj a
class HasArrowCollage (p :: k +-> j) (a :: COLLAGE p) (b :: COLLAGE p) where
- arrCoprod :: a ~> b
data family InjL :: forall (p :: k +-> j) -> j +-> COLLAGE p
data family InjR :: forall (p :: k +-> j) -> k +-> COLLAGE p
collageUniv :: forall {j} {k} (p :: k +-> j). Profunctor p => Iso' p (Direp (InjL p) (InjR p))
data family CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k
data family ProjTo2 :: forall (p :: k +-> j) -> COLLAGE p +-> BOOL
type family CollageObjects (p :: k +-> j) (xs :: [j]) :: [COLLAGE p] where ...
withCollageL :: forall {j} {k} (p :: k +-> j) (x :: j) r. (Finite j, Finite k, KnownIndex x) => (KnownIndex ('L x :: COLLAGE p) => r) -> r
withCollageR :: forall {j} {k} (p :: k +-> j) (y :: k) r. (Finite j, Finite k, KnownIndex y) => (KnownIndex ('R y :: COLLAGE p) => r) -> r

Documentation

data COLLAGE (p :: k +-> j) Source Github #

Constructors

L j
R k

Instances

Instances details

Profunctor p => FunctorForRep (InjL p :: j +-> COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

fmap :: forall (a :: j) (b :: j). (a ~> b) -> (InjL p @ a) ~> (InjL p @ b) Source Github #

Profunctor p => FunctorForRep (InjR p :: j1 +-> COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

fmap :: forall (a :: j1) (b :: j1). (a ~> b) -> (InjR p @ a) ~> (InjR p @ b) Source Github #

(Enumerable j, Enumerable k, Profunctor p) => Enumerable (COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

withIndex :: forall (a :: COLLAGE p) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: COLLAGE p) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (COLLAGE p) (At (COLLAGE p) i) Source Github #

(Finite j, Finite k) => Finite (COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

Associated Types

type Objects (COLLAGE p)
Instance details Defined in Proarrow.Category.Instance.Collage type Objects (COLLAGE p) = CollageObjects p (Objects j)

Methods

finite :: IndexedList (Objects (COLLAGE p)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (COLLAGE p)) i ~ At (COLLAGE p) i => r) -> r Source Github #

(Finite j, Finite k) => Indexed (COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

(HasInitialObject j, CategoryOf k, CodiscreteProfunctor p) => HasInitialObject (COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Collage type InitialObject = 'L (InitialObject :: j) :: COLLAGE p

Methods

initiate :: forall (a :: COLLAGE p). Ob a => (InitialObject :: COLLAGE p) ~> a Source Github #

Profunctor p => CategoryOf (COLLAGE p) Source Github #

The collage of a profunctor.

Instance details

Defined in Proarrow.Category.Instance.Collage

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Collage type (~>) = Collage :: COLLAGE p -> COLLAGE p -> Type

(HasTerminalObject k, CategoryOf j, CodiscreteProfunctor p) => HasTerminalObject (COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Collage type TerminalObject = 'R (TerminalObject :: k) :: COLLAGE p

Methods

terminate :: forall (a :: COLLAGE p). Ob a => a ~> (TerminalObject :: COLLAGE p) Source Github #

Profunctor p => FunctorForRep (ProjTo2 p :: COLLAGE p +-> BOOL) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

fmap :: forall (a :: COLLAGE p) (b :: COLLAGE p). (a ~> b) -> (ProjTo2 p @ a) ~> (ProjTo2 p @ b) Source Github #

DiscreteProfunctor p => FunctorForRep (CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

fmap :: forall (a :: COLLAGE p) (b :: COLLAGE p). (a ~> b) -> ((CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ a) ~> ((CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ b) Source Github #

Profunctor p => Promonad (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

id :: forall (a :: COLLAGE p). Ob a => Collage a a Source Github #

(.) :: forall (b :: COLLAGE p) (c :: COLLAGE p) (a :: COLLAGE p). Collage b c -> Collage a b -> Collage a c Source Github #

(Finitary (Hom j), Finitary (Hom k), Finitary p) => Finitary (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github #

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 details

Defined in Proarrow.Category.Instance.Collage

Methods

size :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => Natural Source Github #

toIndex :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => Collage a b -> Natural Source Github #

fromIndex :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => Natural -> Collage a b Source Github #

elements :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => [Collage a b] Source Github #

(Decidable j, Decidable k, DecidableProfunctor p) => DecidableProfunctor (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github #

Decided piecewise: within either side by that side's order, across by p, and never backwards.

Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

decide :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => Decision (Collage :: COLLAGE p -> COLLAGE p -> Type) a b (Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) a b) Source Github #

toHolds :: forall (a :: COLLAGE p) (b :: COLLAGE p) r. Collage a b -> ((Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Thin j, Thin k, ThinProfunctor p) => ThinProfunctor (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

arr :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b, HasArrow (Collage :: COLLAGE p -> COLLAGE p -> Type) a b) => Collage a b Source Github #

withArr :: forall (a :: COLLAGE p) (b :: COLLAGE p) r. Collage a b -> ((HasArrow (Collage :: COLLAGE p -> COLLAGE p -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

Profunctor p => Profunctor (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

dimap :: forall (c :: COLLAGE p) (a :: COLLAGE p) (b :: COLLAGE p) (d :: COLLAGE p). (c ~> a) -> (b ~> d) -> Collage a b -> Collage c d Source Github #

lmap :: forall (c :: COLLAGE p) (a :: COLLAGE p) (b :: COLLAGE p). (c ~> a) -> Collage a b -> Collage c b Source Github #

rmap :: forall (b :: COLLAGE p) (d :: COLLAGE p) (a :: COLLAGE p). (b ~> d) -> Collage a b -> Collage a d Source Github #

(\\) :: forall (a :: COLLAGE p) (b :: COLLAGE p) r. ((Ob a, Ob b) => r) -> Collage a b -> r Source Github #

type (InjL p :: j +-> COLLAGE p) @ (a :: j) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type (InjL p :: j +-> COLLAGE p) @ (a :: j) = 'L a :: COLLAGE p

type (InjR p :: j1 +-> COLLAGE p) @ (a :: j1) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type (InjR p :: j1 +-> COLLAGE p) @ (a :: j1) = 'R a :: COLLAGE p

type Objects (COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type Objects (COLLAGE p) = CollageObjects p (Objects j)

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type InitialObject = 'L (InitialObject :: j) :: COLLAGE p

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type (~>) = Collage :: COLLAGE p -> COLLAGE p -> Type

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type TerminalObject = 'R (TerminalObject :: k) :: COLLAGE p

type At (COLLAGE p) i Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type At (COLLAGE p) i = Lookup (Objects (COLLAGE p)) i

type Ob (a :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type Ob (a :: COLLAGE p) = IsLR a

type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('L a :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('L a :: COLLAGE p) = 'FLS

type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('R a :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('R a :: COLLAGE p) = 'TRU

type (CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ ('L a :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type (CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ ('L a :: COLLAGE p) = 'L a :: COPRODUCT j k

type (CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ ('R a :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type (CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ ('R a :: COLLAGE p) = 'R a :: COPRODUCT j k

type HasArrow (Collage :: COLLAGE p -> COLLAGE p -> Type) (a :: COLLAGE p) (b :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type HasArrow (Collage :: COLLAGE p -> COLLAGE p -> Type) (a :: COLLAGE p) (b :: COLLAGE p) = HasArrowCollage p a b

type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('L a :: COLLAGE p) ('L b :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('L a :: COLLAGE p) ('L b :: COLLAGE p) = Holds (Hom j) a b

type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('L a :: COLLAGE p) ('R b :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('L a :: COLLAGE p) ('R b :: COLLAGE p) = Holds p a b

type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('R a :: COLLAGE p) ('L b :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('R a :: COLLAGE p) ('L b :: COLLAGE p) = 'FLS

type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('R a :: COLLAGE p) ('R b :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('R a :: COLLAGE p) ('R b :: COLLAGE p) = Holds (Hom k) a b

type Index ('L a :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type Index ('L a :: COLLAGE p) = Index a

type Index ('R b :: COLLAGE p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Collage

type Index ('R b :: COLLAGE p) = Plus (Length (Objects j)) (Index b)

data Collage (a :: COLLAGE p) (b :: COLLAGE p) where Source Github #

Constructors

InL :: forall {j} {k} (a1 :: j) (b1 :: j) (p :: k +-> j). (a1 ~> b1) -> Collage ('L a1 :: COLLAGE p) ('L b1 :: COLLAGE p)
InR :: forall {k} {j} (a1 :: k) (b1 :: k) (p :: k +-> j). (a1 ~> b1) -> Collage ('R a1 :: COLLAGE p) ('R b1 :: COLLAGE p)
L2R :: forall {k} {j} (p :: k +-> j) (a1 :: j) (b1 :: k). p a1 b1 -> Collage ('L a1 :: COLLAGE p) ('R b1 :: COLLAGE p)

Instances

Instances details

Profunctor p => Promonad (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods id :: forall (a :: COLLAGE p). Ob a => Collage a a Source Github # (.) :: forall (b :: COLLAGE p) (c :: COLLAGE p) (a :: COLLAGE p). Collage b c -> Collage a b -> Collage a c Source Github #
(Finitary (Hom j), Finitary (Hom k), Finitary p) => Finitary (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github #	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 details Defined in Proarrow.Category.Instance.Collage Methods size :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => Natural Source Github # toIndex :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => Collage a b -> Natural Source Github # fromIndex :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => Natural -> Collage a b Source Github # elements :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => [Collage a b] Source Github #
(Decidable j, Decidable k, DecidableProfunctor p) => DecidableProfunctor (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github #	Decided piecewise: within either side by that side's order, across by `p`, and never backwards.
Instance details Defined in Proarrow.Category.Instance.Collage Methods decide :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => Decision (Collage :: COLLAGE p -> COLLAGE p -> Type) a b (Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) a b) Source Github # toHolds :: forall (a :: COLLAGE p) (b :: COLLAGE p) r. Collage a b -> ((Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #
(Thin j, Thin k, ThinProfunctor p) => ThinProfunctor (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods arr :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b, HasArrow (Collage :: COLLAGE p -> COLLAGE p -> Type) a b) => Collage a b Source Github # withArr :: forall (a :: COLLAGE p) (b :: COLLAGE p) r. Collage a b -> ((HasArrow (Collage :: COLLAGE p -> COLLAGE p -> Type) a b, Ob a, Ob b) => r) -> r Source Github #
Profunctor p => Profunctor (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods dimap :: forall (c :: COLLAGE p) (a :: COLLAGE p) (b :: COLLAGE p) (d :: COLLAGE p). (c ~> a) -> (b ~> d) -> Collage a b -> Collage c d Source Github # lmap :: forall (c :: COLLAGE p) (a :: COLLAGE p) (b :: COLLAGE p). (c ~> a) -> Collage a b -> Collage c b Source Github # rmap :: forall (b :: COLLAGE p) (d :: COLLAGE p) (a :: COLLAGE p). (b ~> d) -> Collage a b -> Collage a d Source Github # (\\) :: forall (a :: COLLAGE p) (b :: COLLAGE p) r. ((Ob a, Ob b) => r) -> Collage a b -> r Source Github #
type HasArrow (Collage :: COLLAGE p -> COLLAGE p -> Type) (a :: COLLAGE p) (b :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage type HasArrow (Collage :: COLLAGE p -> COLLAGE p -> Type) (a :: COLLAGE p) (b :: COLLAGE p) = HasArrowCollage p a b
type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('L a :: COLLAGE p) ('L b :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('L a :: COLLAGE p) ('L b :: COLLAGE p) = Holds (Hom j) a b
type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('L a :: COLLAGE p) ('R b :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('L a :: COLLAGE p) ('R b :: COLLAGE p) = Holds p a b
type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('R a :: COLLAGE p) ('L b :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('R a :: COLLAGE p) ('L b :: COLLAGE p) = 'FLS
type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('R a :: COLLAGE p) ('R b :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage type Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) ('R a :: COLLAGE p) ('R b :: COLLAGE p) = Holds (Hom k) a b

class IsLR (a :: COLLAGE p) where Source Github #

Methods

lrId :: Obj a Source Github #

Instances

Instances details

(Ob a, Promonad ((~>) :: CAT k)) => IsLR ('L a :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods lrId :: Obj ('L a :: COLLAGE p) Source Github #
(Ob a, Promonad ((~>) :: CAT j)) => IsLR ('R a :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods lrId :: Obj ('R a :: COLLAGE p) Source Github #

class HasArrowCollage (p :: k +-> j) (a :: COLLAGE p) (b :: COLLAGE p) where Source Github #

Methods

arrCoprod :: a ~> b Source Github #

Instances

Instances details

(Thin j, HasArrow ((~>) :: CAT j) a b, Ob a, Ob b) => HasArrowCollage (p :: k +-> j) ('L a :: COLLAGE p) ('L b :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods arrCoprod :: ('L a :: COLLAGE p) ~> ('L b :: COLLAGE p) Source Github #
(ThinProfunctor p, HasArrow p a b, Ob a, Ob b) => HasArrowCollage (p :: k +-> j) ('L a :: COLLAGE p) ('R b :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods arrCoprod :: ('L a :: COLLAGE p) ~> ('R b :: COLLAGE p) Source Github #
(Thin k, HasArrow ((~>) :: CAT k) a b, Ob a, Ob b) => HasArrowCollage (p :: k +-> j) ('R a :: COLLAGE p) ('R b :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods arrCoprod :: ('R a :: COLLAGE p) ~> ('R b :: COLLAGE p) Source Github #

data family InjL :: forall (p :: k +-> j) -> j +-> COLLAGE p Source Github #

Instances

Instances details

Profunctor p => FunctorForRep (InjL p :: j +-> COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods fmap :: forall (a :: j) (b :: j). (a ~> b) -> (InjL p @ a) ~> (InjL p @ b) Source Github #
type (InjL p :: j +-> COLLAGE p) @ (a :: j) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage type (InjL p :: j +-> COLLAGE p) @ (a :: j) = 'L a :: COLLAGE p

data family InjR :: forall (p :: k +-> j) -> k +-> COLLAGE p Source Github #

Instances

Instances details

Profunctor p => FunctorForRep (InjR p :: j1 +-> COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods fmap :: forall (a :: j1) (b :: j1). (a ~> b) -> (InjR p @ a) ~> (InjR p @ b) Source Github #
type (InjR p :: j1 +-> COLLAGE p) @ (a :: j1) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage type (InjR p :: j1 +-> COLLAGE p) @ (a :: j1) = 'R a :: COLLAGE p

collageUniv :: forall {j} {k} (p :: k +-> j). Profunctor p => Iso' p (Direp (InjL p) (InjR p)) Source Github #

data family CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k Source Github #

Instances

Instances details

DiscreteProfunctor p => FunctorForRep (CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods fmap :: forall (a :: COLLAGE p) (b :: COLLAGE p). (a ~> b) -> ((CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ a) ~> ((CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ b) Source Github #
type (CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ ('L a :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage type (CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ ('L a :: COLLAGE p) = 'L a :: COPRODUCT j k
type (CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ ('R a :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage type (CollageAsCoprod :: COLLAGE p +-> COPRODUCT j k) @ ('R a :: COLLAGE p) = 'R a :: COPRODUCT j k

data family ProjTo2 :: forall (p :: k +-> j) -> COLLAGE p +-> BOOL Source Github #

Instances

Instances details

Profunctor p => FunctorForRep (ProjTo2 p :: COLLAGE p +-> BOOL) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage Methods fmap :: forall (a :: COLLAGE p) (b :: COLLAGE p). (a ~> b) -> (ProjTo2 p @ a) ~> (ProjTo2 p @ b) Source Github #
type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('L a :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('L a :: COLLAGE p) = 'FLS
type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('R a :: COLLAGE p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Collage type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('R a :: COLLAGE p) = 'TRU

Numbering the collage

type family CollageObjects (p :: k +-> j) (xs :: [j]) :: [COLLAGE p] where ... Source Github #

The collage numbers the left category's objects first and the right category's after them.

Equations

CollageObjects (p :: k +-> j) ('[] :: [j]) = MapWrap ('R :: k -> COLLAGE p) (Objects k)
CollageObjects (p :: k +-> j) (x ': xs :: [j]) = ('L x :: COLLAGE p) ': CollageObjects p xs

withCollageL :: forall {j} {k} (p :: k +-> j) (x :: j) r. (Finite j, Finite k, KnownIndex x) => (KnownIndex ('L x :: COLLAGE p) => r) -> r Source Github #

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.

withCollageR :: forall {j} {k} (p :: k +-> j) (y :: k) r. (Finite j, Finite k, KnownIndex y) => (KnownIndex ('R y :: COLLAGE p) => r) -> r Source Github #