Safe Haskell	None
Language	GHC2024

Proarrow.Colimit.Initial

Contents

Orphan instances

Description

Initial objects: HasInitialObject with the unique arrow initiate, instances for the base kinds, and HasZeroObject for categories where the initial and terminal objects coincide.

Documentation

class (CategoryOf k, Ob (InitialObject :: k)) => HasInitialObject k where Source Github #

Associated Types

type InitialObject :: k Source Github #

Methods

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

Instances

Instances details

HasInitialObject Nat Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Associated Types

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

Methods

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

HasInitialObject BOOL Source Github #

Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

type InitialObject
Instance details Defined in Proarrow.Colimit.Initial type InitialObject = 'FLS

Methods

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

HasInitialObject COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Cost type InitialObject = 'INF

Methods

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

HasInitialObject FINHASK Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.FinHask type InitialObject = 'FH Void

Methods

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

HasInitialObject FINREL Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

Associated Types

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

Methods

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

HasInitialObject FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.FinSet type InitialObject = 'FS Nat0

Methods

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

HasInitialObject LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Linear type InitialObject = 'L Void

Methods

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

HasInitialObject POINTED Source Github #

Instance details

Defined in Proarrow.Category.Instance.PointedHask

Associated Types

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

Methods

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

HasInitialObject () Source Github #

Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

type InitialObject
Instance details Defined in Proarrow.Colimit.Initial type InitialObject = '()

Methods

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

HasInitialObject Type Source Github #

Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

type InitialObject
Instance details Defined in Proarrow.Colimit.Initial type InitialObject = Void

Methods

initiate :: Ob a => (InitialObject :: Type) ~> a Source Github #

CategoryOf k => HasInitialObject (FAM k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fam

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Fam type InitialObject = DEP VOID (Rep (Initiate :: VOID +-> k))

Methods

initiate :: forall (a :: FAM k). Ob a => (InitialObject :: FAM k) ~> a Source Github #

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

Instance details

Defined in Proarrow.Category.Instance.Mat

Associated Types

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

Methods

initiate :: forall (a0 :: MatK a). Ob a0 => (InitialObject :: MatK a) ~> a0 Source Github #

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

Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

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

Methods

initiate :: forall (a :: OPPOSITE k). Ob a => (InitialObject :: OPPOSITE k) ~> a Source Github #

HasInitialObject (ORDINAL ('S n)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

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

Methods

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

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

Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Associated Types

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

Methods

initiate :: forall (a :: COPROD k). Ob a => (InitialObject :: COPROD k) ~> a Source Github #

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

Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

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

Methods

initiate :: forall (a :: PROD k). Ob a => (InitialObject :: PROD k) ~> a Source Github #

(CategoryOf j, CategoryOf k) => HasInitialObject (FINITARY j k) Source Github #

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Enriched.Finitary.Topos type InitialObject = FIN (InitialProfunctor :: k -> j -> Type)

Methods

initiate :: forall (a :: FINITARY j k). Ob a => (InitialObject :: FINITARY j k) ~> a Source Github #

(HasInitialObject k, Monad p) => HasInitialObject (KLEISLI p) Source Github #

Dually, the initial object lifts to the Kleisli category of a Monad: there p a b is a ~> p % b, so the presheaf p (-) z is representable and takes colimits in k to limits.

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Associated Types

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

Methods

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

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

Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

type InitialObject
Instance details Defined in Proarrow.Colimit.Initial type InitialObject = InitialProfunctor :: k -> j -> Type

Methods

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

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

Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

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

Methods

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

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

Instance details

Defined in Proarrow.Category.Instance.Nat

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Nat type InitialObject = Const Void :: k1 -> Type

Methods

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

(HasFiniteCovers t k, FiniteCat j, FiniteCat k) => HasInitialObject (SHEAVES t j k) Source Github #

Colimits are the presheaf colimits, sheafified: take the FINITARY colimit, follow its cocone with unitSheafify, and get the universal property from extendSheafify. This works because sheafification is a left adjoint.

The initial sheaf need not be the initial presheaf. Joins covers the bottom of a lattice by the empty family, so every sheaf has one section there.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Sheaf

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Enriched.Finitary.Sheaf type InitialObject = 'SUB (Sheafify t (InitialProfunctor :: k -> j -> Type)) :: SUBCAT ((Finitary :: (j +-> k) -> Constraint) :&&: (Sheaf t :: (j +-> k) -> Constraint))

Methods

initiate :: forall (a :: SHEAVES t j k). Ob a => (InitialObject :: SHEAVES t j k) ~> a Source Github #

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

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

Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

type InitialObject
Instance details Defined in Proarrow.Colimit.Initial type InitialObject = InitF :: FREE cs p

Methods

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

initiate' :: forall {k} (a' :: k) (a :: k). HasInitialObject k => (a' ~> a) -> (InitialObject :: k) ~> a Source Github #

class (HasInitialObject k, HasTerminalObject k, (InitialObject :: k) ~ (TerminalObject :: k)) => HasZeroObject k where Source Github #

Methods

zero :: forall (a :: k) (b :: k). (Ob a, Ob b) => a ~> b Source Github #

Instances

Instances details

(HasInitialObject k, HasTerminalObject k, (InitialObject :: k) ~ (TerminalObject :: k)) => HasZeroObject k Source Github #
Instance details Defined in Proarrow.Colimit.Initial Methods zero :: forall (a :: k) (b :: k). (Ob a, Ob b) => a ~> b Source Github #

data family InitF :: k Source Github #

Instances

Instances details

Elem HasInitialObject cs => IsFreeOb (InitF :: FREE cs p) Source Github #
Instance details Defined in Proarrow.Colimit.Initial Methods lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (InitF :: FREE cs p)) => r) -> r Source Github #
type Lower (f :: k +-> k') (InitF :: FREE cs p) Source Github #
Instance details Defined in Proarrow.Colimit.Initial type Lower (f :: k +-> k') (InitF :: FREE cs p) = InitialObject :: k'

Orphan instances

(HasInitialObject j, CategoryOf k) => Corepresentable (TerminalProfunctor :: k -> j -> Type) Source Github #

Instance details

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 #

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

Instance details

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 #