Safe Haskell	None
Language	GHC2024

Proarrow.Limit.Terminal

Contents

Orphan instances

Description

Terminal objects: HasTerminalObject with the unique arrow terminate, instances for the base kinds, and global elements El a = TerminalObject ~> a.

Synopsis

class (CategoryOf k, Ob (TerminalObject :: k)) => HasTerminalObject k where
- type TerminalObject :: k
- terminate :: forall (a :: k). Ob a => a ~> (TerminalObject :: k)
terminate' :: forall {k} (a :: k) (a' :: k). HasTerminalObject k => (a ~> a') -> a ~> (TerminalObject :: k)
type El (a :: k) = (TerminalObject :: k) ~> a
const :: forall {k} (a :: k) (b :: k). (HasTerminalObject k, Ob a) => El b -> a ~> b
class ((Unit :: k) ~ (TerminalObject :: k), HasTerminalObject k, Monoidal k) => Semicartesian k
data family TermF :: k

Documentation

class (CategoryOf k, Ob (TerminalObject :: k)) => HasTerminalObject k where Source Github #

Associated Types

type TerminalObject :: k Source Github #

Methods

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

Instances

Instances details

HasTerminalObject Nat Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Simplex type TerminalObject = 'S 'Z

Methods

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

HasTerminalObject BOOL Source Github #

Instance details

Defined in Proarrow.Limit.Terminal

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Limit.Terminal type TerminalObject = 'TRU

Methods

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

HasTerminalObject CONSTRAINT Source Github #

Instance details

Defined in Proarrow.Category.Instance.Constraint

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Constraint type TerminalObject = 'CNSTRNT ()

Methods

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

HasTerminalObject COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Cost type TerminalObject = 'C 0

Methods

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

HasTerminalObject FINHASK Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.FinHask type TerminalObject = 'FH ()

Methods

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

HasTerminalObject FINREL Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.FinRel type TerminalObject = 'FR Nat0

Methods

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

HasTerminalObject FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.FinSet type TerminalObject = 'FS Nat1

Methods

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

HasTerminalObject LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Linear type TerminalObject = 'L Top

Methods

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

HasTerminalObject POINTED Source Github #

Instance details

Defined in Proarrow.Category.Instance.PointedHask

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.PointedHask type TerminalObject = 'P Void

Methods

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

HasTerminalObject () Source Github #

Instance details

Defined in Proarrow.Limit.Terminal

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Limit.Terminal type TerminalObject = '()

Methods

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

HasTerminalObject Type Source Github #

Instance details

Defined in Proarrow.Limit.Terminal

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Limit.Terminal type TerminalObject = ()

Methods

terminate :: Ob a => a ~> (TerminalObject :: Type) Source Github #

HasTerminalObject k => HasTerminalObject (FAM k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fam

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Fam type TerminalObject = DEP () (TerminalProfunctor :: k -> () -> Type)

Methods

terminate :: forall (a :: FAM k). Ob a => a ~> (TerminalObject :: FAM k) Source Github #

Num a => HasTerminalObject (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Mat type TerminalObject = 'M 'Z :: MatK a

Methods

terminate :: forall (a0 :: MatK a). Ob a0 => a0 ~> (TerminalObject :: MatK a) Source Github #

HasInitialObject k => HasTerminalObject (OPPOSITE k) Source Github #

Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Colimit.Initial type TerminalObject = 'OP (InitialObject :: k)

Methods

terminate :: forall (a :: OPPOSITE k). Ob a => a ~> (TerminalObject :: OPPOSITE k) Source Github #

HasTerminalObject (ORDINAL ('S n)) => HasTerminalObject (ORDINAL ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Ordinal type TerminalObject = 'OS (TerminalObject :: ORDINAL ('S n))

Methods

terminate :: forall (a :: ORDINAL ('S ('S n))). Ob a => a ~> (TerminalObject :: ORDINAL ('S ('S n))) Source Github #

HasTerminalObject (ORDINAL ('S 'Z)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Ordinal type TerminalObject = 'OZ :: ORDINAL ('S 'Z)

Methods

terminate :: forall (a :: ORDINAL ('S 'Z)). Ob a => a ~> (TerminalObject :: ORDINAL ('S 'Z)) Source Github #

HasTerminalObject k => HasTerminalObject (COPROD k) Source Github #

Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Colimit.BinaryCoproduct type TerminalObject = 'COPR (TerminalObject :: k)

Methods

terminate :: forall (a :: COPROD k). Ob a => a ~> (TerminalObject :: COPROD k) Source Github #

HasTerminalObject k => HasTerminalObject (PROD k) Source Github #

Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Limit.BinaryProduct type TerminalObject = 'PR (TerminalObject :: k)

Methods

terminate :: forall (a :: PROD k). Ob a => a ~> (TerminalObject :: PROD k) Source Github #

(HasTerminalObject k, Comonad p) => HasTerminalObject (KLEISLI p) Source Github #

The terminal object lifts to the co-Kleisli category of a Comonad: there p a b is p %% a ~> b, so p a (-) is representable and preserves limits. A bare Promonad is not enough. At the constant promonad HaskValue c every element of c is an arrow into the terminal object, so uniqueness fails.

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Kleisli type TerminalObject = 'KL (TerminalObject :: k) :: KLEISLI p

Methods

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

(HasTerminalObject k, ob (TerminalObject :: k)) => HasTerminalObject (SUBCAT ob) Source Github #

A full subcategory has the ambient finite products as soon as it contains them, as the quantified constraint says. The projections and pairing are the ambient ones under Sub.

There is no exponential at an arbitrary kind: neither withObExp nor curry discharges through PROD k's round trip UN PR (PR a ~~> PR b). For subcategories of profunctors see Closed (PROD (SUBCAT ob)) in Proarrow.Profunctor.Instance.Exponential.

Instance details

Defined in Proarrow.Category.Instance.Sub

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Sub type TerminalObject = 'SUB (TerminalObject :: k) :: SUBCAT ob

Methods

terminate :: forall (a :: SUBCAT ob). Ob a => a ~> (TerminalObject :: SUBCAT ob) Source Github #

(CategoryOf j, CategoryOf k) => HasTerminalObject (j +-> k) Source Github #

Instance details

Defined in Proarrow.Limit.Terminal

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Limit.Terminal type TerminalObject = TerminalProfunctor :: k -> j -> Type

Methods

terminate :: forall (a :: j +-> k). Ob a => a ~> (TerminalObject :: j +-> k) Source Github #

(HasTerminalObject j, HasTerminalObject k) => HasTerminalObject (j, k) Source Github #

Instance details

Defined in Proarrow.Limit.Terminal

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Limit.Terminal type TerminalObject = '(TerminalObject :: j, TerminalObject :: k)

Methods

terminate :: forall (a :: (j, k)). Ob a => a ~> (TerminalObject :: (j, k)) Source Github #

CategoryOf k1 => HasTerminalObject (k1 -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Nat

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Nat type TerminalObject = Const () :: k1 -> Type

Methods

terminate :: forall (a :: k1 -> Type). Ob a => a ~> (TerminalObject :: k1 -> Type) Source Github #

(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 #

Elem HasTerminalObject cs => HasTerminalObject (FREE cs p) Source Github #

Instance details

Defined in Proarrow.Limit.Terminal

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Limit.Terminal type TerminalObject = TermF :: FREE cs p

Methods

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

terminate' :: forall {k} (a :: k) (a' :: k). HasTerminalObject k => (a ~> a') -> a ~> (TerminalObject :: k) Source Github #

type El (a :: k) = (TerminalObject :: k) ~> a Source Github #

The type of elements of a.

const :: forall {k} (a :: k) (b :: k). (HasTerminalObject k, Ob a) => El b -> a ~> b Source Github #

The constant arrow at an element: terminate, then the element.

class ((Unit :: k) ~ (TerminalObject :: k), HasTerminalObject k, Monoidal k) => Semicartesian k Source Github #

Instances

Instances details

((Unit :: k) ~ (TerminalObject :: k), HasTerminalObject k, Monoidal k) => Semicartesian k Source Github #
Instance details Defined in Proarrow.Limit.Terminal

data family TermF :: k Source Github #

Instances

Instances details

Elem HasTerminalObject cs => IsFreeOb (TermF :: FREE cs p) Source Github #
Instance details Defined in Proarrow.Limit.Terminal Methods lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (TermF :: FREE cs p)) => r) -> r Source Github #
type Lower (f :: k +-> k') (TermF :: FREE cs p) Source Github #
Instance details Defined in Proarrow.Limit.Terminal type Lower (f :: k +-> k') (TermF :: FREE cs p) = TerminalObject :: k'

Orphan instances

(HasTerminalObject k, CategoryOf j) => Representable (TerminalProfunctor :: k -> j -> Type) Source Github #

Instance details

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 #