Safe Haskell	None
Language	GHC2024

Proarrow.Profunctor.Instance.Terminal

Description

The terminal profunctor, with exactly one value between any two objects: the terminal object of the category of profunctors j +-> k.

Synopsis

data TerminalProfunctor (a :: k) (b :: j) where
- TerminalProfunctor' :: forall k (a :: k) j (b :: j). Obj a -> Obj b -> TerminalProfunctor a b
- pattern TerminalProfunctor :: (CategoryOf j, CategoryOf k) => (Ob a, Ob b) => TerminalProfunctor a b

Documentation

data TerminalProfunctor (a :: k) (b :: j) where Source Github #

The profunctor with exactly one value between any two objects: the terminal object of the category of profunctors j +-> k.

Constructors

TerminalProfunctor' :: forall k (a :: k) j (b :: j). Obj a -> Obj b -> TerminalProfunctor a b

Bundled Patterns

pattern TerminalProfunctor :: (CategoryOf j, CategoryOf k) => (Ob a, Ob b) => TerminalProfunctor a b

Instances

Instances details

(Site t k, CategoryOf j) => Sheaf t (TerminalProfunctor :: k -> j -> Type) Source Github #	The limits of profunctors are sheaves whenever their factors are: the terminal profunctor for every coverage, and a product of sheaves glued componentwise.
Instance details Defined in Proarrow.Category.Sheaf Methods glue :: forall (a :: k) c (b :: j). (Ob a, Ob b) => Cover t k a c -> (forall (x :: k). Leg t k a c x -> TerminalProfunctor x b) -> TerminalProfunctor a b Source Github #
(CategoryOf k, CategoryOf j) => AffineFoldFl (Id :: k -> k -> Type) (TerminalProfunctor :: j -> j -> Type) Source Github #
Instance details Defined in Proarrow.Optic.AffineFold Methods previewP :: forall (s :: k) (a :: k). Bicartesian k => Id s a -> s ~> (a \|\| (TerminalObject :: k)) Source Github #
(CategoryOf k, CategoryOf j) => FoldFl (Id :: k -> k -> Type) (TerminalProfunctor :: j -> j -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Fold Methods foldMapP :: forall (m :: k) (s :: k) (a :: k). Monoid m => Id s a -> (a ~> m) -> s ~> m Source Github #
(CategoryOf k, CategoryOf j) => GetterFl (Id :: k -> k -> Type) (TerminalProfunctor :: j -> j -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Getter Methods getP :: forall (s :: k) (a :: k). Id s a -> s ~> a Source Github #
(CategoryOf j, CategoryOf k) => Finitary (TerminalProfunctor :: k -> j -> Type) Source Github #	The terminal profunctor has one element everywhere.
Instance details Defined in Proarrow.Category.Enriched.Finitary Methods size :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural Source Github # toIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => TerminalProfunctor a b -> Natural Source Github # fromIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> TerminalProfunctor a b Source Github # elements :: forall (a :: k) (b :: j). (Ob a, Ob b) => [TerminalProfunctor a b] Source Github #
(CategoryOf j, CategoryOf k) => DecidableProfunctor (TerminalProfunctor :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Terminal Methods decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (TerminalProfunctor :: k -> j -> Type) a b (Holds (TerminalProfunctor :: k -> j -> Type) a b) Source Github # toHolds :: forall (a :: k) (b :: j) r. TerminalProfunctor a b -> ((Holds (TerminalProfunctor :: k -> j -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #
(CategoryOf j, CategoryOf k) => ThinProfunctor (TerminalProfunctor :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Terminal Methods arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (TerminalProfunctor :: k -> j -> Type) a b) => TerminalProfunctor a b Source Github # withArr :: forall (a :: k) (b :: j) r. TerminalProfunctor a b -> ((HasArrow (TerminalProfunctor :: k -> j -> Type) a b, Ob a, Ob b) => r) -> r Source Github #
(Monoidal j, Monoidal k) => MonoidalProfunctor (TerminalProfunctor :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Terminal Methods one :: TerminalProfunctor (Unit :: k) (Unit :: j) Source Github # () :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j). TerminalProfunctor x1 x2 -> TerminalProfunctor y1 y2 -> TerminalProfunctor (x1 y1) (x2 ** y2) Source Github #
(CategoryOf j, CategoryOf k) => Profunctor (TerminalProfunctor :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Terminal Methods dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> TerminalProfunctor a b -> TerminalProfunctor c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: j). (c ~> a) -> TerminalProfunctor a b -> TerminalProfunctor c b Source Github # rmap :: forall (b :: j) (d :: j) (a :: k). (b ~> d) -> TerminalProfunctor a b -> TerminalProfunctor a d Source Github # (\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> TerminalProfunctor a b -> r Source Github #
(HasInitialObject j, CategoryOf k) => Corepresentable (TerminalProfunctor :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Colimit.Initial Methods coindex :: forall (a :: k) (b :: j). TerminalProfunctor a b -> ((TerminalProfunctor :: k -> j -> Type) %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: j). Ob a => (((TerminalProfunctor :: k -> j -> Type) %% a) ~> b) -> TerminalProfunctor a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> ((TerminalProfunctor :: k -> j -> Type) %% a) ~> ((TerminalProfunctor :: k -> j -> Type) %% b) Source Github # corepUniv :: forall (a :: k). Ob a => TerminalProfunctor a ((TerminalProfunctor :: k -> j -> Type) %% a) Source Github #
(HasTerminalObject k, CategoryOf j) => Representable (TerminalProfunctor :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Limit.Terminal Methods index :: forall (a :: k) (b :: j). TerminalProfunctor a b -> a ~> ((TerminalProfunctor :: k -> j -> Type) % b) Source Github # tabulate :: forall (b :: j) (a :: k). Ob b => (a ~> ((TerminalProfunctor :: k -> j -> Type) % b)) -> TerminalProfunctor a b Source Github # repMap :: forall (a :: j) (b :: j). (a ~> b) -> ((TerminalProfunctor :: k -> j -> Type) % a) ~> ((TerminalProfunctor :: k -> j -> Type) % b) Source Github # repUniv :: forall (a :: j). Ob a => TerminalProfunctor ((TerminalProfunctor :: k -> j -> Type) % a) a Source Github #
Dagger k => DaggerProfunctor (TerminalProfunctor :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Terminal Methods dagger :: forall (a :: k) (b :: k). TerminalProfunctor a b -> TerminalProfunctor b a Source Github #
CategoryOf k => Promonad (TerminalProfunctor :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Terminal Methods id :: forall (a :: k). Ob a => TerminalProfunctor a a Source Github # (.) :: forall (b :: k) (c :: k) (a :: k). TerminalProfunctor b c -> TerminalProfunctor a b -> TerminalProfunctor a c Source Github #
(HasCoproducts j, HasCoproducts k) => MonoidalProfunctor (Coprod (TerminalProfunctor :: k -> j -> Type) :: COPROD k -> COPROD j -> Type) Source Github #
Instance details Defined in Proarrow.Colimit.BinaryCoproduct Methods one :: Coprod (TerminalProfunctor :: k -> j -> Type) (Unit :: COPROD k) (Unit :: COPROD j) Source Github # () :: forall (x1 :: COPROD k) (x2 :: COPROD j) (y1 :: COPROD k) (y2 :: COPROD j). Coprod (TerminalProfunctor :: k -> j -> Type) x1 x2 -> Coprod (TerminalProfunctor :: k -> j -> Type) y1 y2 -> Coprod (TerminalProfunctor :: k -> j -> Type) (x1 y1) (x2 ** y2) Source Github #
type (TerminalProfunctor :: k -> j -> Type) %% (x :: k) Source Github #
Instance details Defined in Proarrow.Colimit.Initial type (TerminalProfunctor :: k -> j -> Type) %% (x :: k) = InitialObject :: j
type (TerminalProfunctor :: k -> j -> Type) % (x :: j) Source Github #
Instance details Defined in Proarrow.Limit.Terminal type (TerminalProfunctor :: k -> j -> Type) % (x :: j) = TerminalObject :: k
type HasArrow (TerminalProfunctor :: k -> j -> Type) (a :: k) (b :: j) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Terminal type HasArrow (TerminalProfunctor :: k -> j -> Type) (a :: k) (b :: j) = Holds (TerminalProfunctor :: k -> j -> Type) a b ~ 'TRU
type Holds (TerminalProfunctor :: k -> j -> Type) (a :: k) (b :: j) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Terminal type Holds (TerminalProfunctor :: k -> j -> Type) (a :: k) (b :: j) = 'TRU