data-category-0.11: Category theory
LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Category.Coproduct

Description

 
Synopsis

Documentation

data I1 a Source #

Instances

Instances details
type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) = I1 (BinaryCoproduct c1 a b)
type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) = I2 b
type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) = I2 a
type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) = I1 (BinaryProduct c1 a b)
type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) = I1 a
type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) = I1 b
type (CodiagCoprod k) :% (I1 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (CodiagCoprod k) :% (I1 a) = a
type (f1 :+++: f2) :% (I1 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (f1 :+++: f2) :% (I1 a) = I1 (f1 :% a)
type (NatAsFunctor f g) :% (a, I1 ()) Source # 
Instance details

Defined in Data.Category.Coproduct

type (NatAsFunctor f g) :% (a, I1 ()) = f :% a
type (Cotuple1 c1 c2 a1) :% (I1 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (Cotuple1 c1 c2 a1) :% (I1 a) = a
type (Cotuple2 c1 c2 a2) :% (I1 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (Cotuple2 c1 c2 a2) :% (I1 a) = a2

data I2 a Source #

Instances

Instances details
type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) = I2 b
type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) = I2 a
type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) = I2 (BinaryCoproduct c2 a b)
type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) = I1 a
type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) = I1 b
type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) = I2 (BinaryProduct c2 a b)
type (CodiagCoprod k) :% (I2 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (CodiagCoprod k) :% (I2 a) = a
type (f1 :+++: f2) :% (I2 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)
type (NatAsFunctor f g) :% (a, I2 ()) Source # 
Instance details

Defined in Data.Category.Coproduct

type (NatAsFunctor f g) :% (a, I2 ()) = g :% a
type (Cotuple1 c1 c2 a1) :% (I2 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (Cotuple1 c1 c2 a1) :% (I2 a) = a1
type (Cotuple2 c1 c2 a2) :% (I2 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (Cotuple2 c1 c2 a2) :% (I2 a) = a

data (:++:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where Source #

Constructors

I1 :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1) 
I2 :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2) 

Instances

Instances details
(Category c1, Category c2) => Category (c1 :++: c2 :: Type -> Type -> Type) Source #

The coproduct category of categories c1 and c2.

Instance details

Defined in Data.Category.Coproduct

Methods

src :: forall (a :: k) (b :: k). (c1 :++: c2) a b -> Obj (c1 :++: c2) a Source #

tgt :: forall (a :: k) (b :: k). (c1 :++: c2) a b -> Obj (c1 :++: c2) b Source #

(.) :: forall (b :: k) (c :: k) (a :: k). (c1 :++: c2) b c -> (c1 :++: c2) a b -> (c1 :++: c2) a c Source #

(HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (i :++: j) k Source #

If k has binary coproducts, we can take the colimit of 2 joined diagrams.

Instance details

Defined in Data.Category.Limit

Associated Types

type ColimitFam (i :++: j) k f Source #

Methods

colimit :: Obj (Nat (i :++: j) k) f -> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f) Source #

colimitFactorizer :: Cocone (i :++: j) k f n -> k (ColimitFam (i :++: j) k f) n Source #

(HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (i :++: j) k Source #

If k has binary products, we can take the limit of 2 joined diagrams.

Instance details

Defined in Data.Category.Limit

Associated Types

type LimitFam (i :++: j) k f Source #

Methods

limit :: Obj (Nat (i :++: j) k) f -> Cone (i :++: j) k f (LimitFam (i :++: j) k f) Source #

limitFactorizer :: Cone (i :++: j) k f n -> k n (LimitFam (i :++: j) k f) Source #

type ColimitFam (i :++: j) k f Source # 
Instance details

Defined in Data.Category.Limit

type ColimitFam (i :++: j) k f = BinaryCoproduct k (ColimitFam i k (f :.: Inj1 i j)) (ColimitFam j k (f :.: Inj2 i j))
type LimitFam (i :++: j) k f Source # 
Instance details

Defined in Data.Category.Limit

type LimitFam (i :++: j) k f = BinaryProduct k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j))

data Inj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) Source #

Constructors

Inj1 

Instances

Instances details
(Category c1, Category c2) => Functor (Inj1 c1 c2) Source #

Inj1 is a functor which injects into the left category.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (Inj1 c1 c2) :: Type -> Type -> Type Source #

type Cod (Inj1 c1 c2) :: Type -> Type -> Type Source #

type (Inj1 c1 c2) :% a Source #

Methods

(%) :: Inj1 c1 c2 -> Dom (Inj1 c1 c2) a b -> Cod (Inj1 c1 c2) (Inj1 c1 c2 :% a) (Inj1 c1 c2 :% b) Source #

type Cod (Inj1 c1 c2) Source # 
Instance details

Defined in Data.Category.Coproduct

type Cod (Inj1 c1 c2) = c1 :++: c2
type Dom (Inj1 c1 c2) Source # 
Instance details

Defined in Data.Category.Coproduct

type Dom (Inj1 c1 c2) = c1
type (Inj1 c1 c2) :% a Source # 
Instance details

Defined in Data.Category.Coproduct

type (Inj1 c1 c2) :% a = I1 a

data Inj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) Source #

Constructors

Inj2 

Instances

Instances details
(Category c1, Category c2) => Functor (Inj2 c1 c2) Source #

Inj2 is a functor which injects into the right category.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (Inj2 c1 c2) :: Type -> Type -> Type Source #

type Cod (Inj2 c1 c2) :: Type -> Type -> Type Source #

type (Inj2 c1 c2) :% a Source #

Methods

(%) :: Inj2 c1 c2 -> Dom (Inj2 c1 c2) a b -> Cod (Inj2 c1 c2) (Inj2 c1 c2 :% a) (Inj2 c1 c2 :% b) Source #

type Cod (Inj2 c1 c2) Source # 
Instance details

Defined in Data.Category.Coproduct

type Cod (Inj2 c1 c2) = c1 :++: c2
type Dom (Inj2 c1 c2) Source # 
Instance details

Defined in Data.Category.Coproduct

type Dom (Inj2 c1 c2) = c2
type (Inj2 c1 c2) :% a Source # 
Instance details

Defined in Data.Category.Coproduct

type (Inj2 c1 c2) :% a = I2 a

data f1 :+++: f2 Source #

Constructors

f1 :+++: f2 

Instances

Instances details
(Functor f1, Functor f2) => Functor (f1 :+++: f2) Source #

f1 :+++: f2 is the coproduct of the functors f1 and f2.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (f1 :+++: f2) :: Type -> Type -> Type Source #

type Cod (f1 :+++: f2) :: Type -> Type -> Type Source #

type (f1 :+++: f2) :% a Source #

Methods

(%) :: (f1 :+++: f2) -> Dom (f1 :+++: f2) a b -> Cod (f1 :+++: f2) ((f1 :+++: f2) :% a) ((f1 :+++: f2) :% b) Source #

type Cod (f1 :+++: f2) Source # 
Instance details

Defined in Data.Category.Coproduct

type Cod (f1 :+++: f2) = Cod f1 :++: Cod f2
type Dom (f1 :+++: f2) Source # 
Instance details

Defined in Data.Category.Coproduct

type Dom (f1 :+++: f2) = Dom f1 :++: Dom f2
type (f1 :+++: f2) :% (I1 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (f1 :+++: f2) :% (I1 a) = I1 (f1 :% a)
type (f1 :+++: f2) :% (I2 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)

data CodiagCoprod (k :: Type -> Type -> Type) Source #

Constructors

CodiagCoprod 

Instances

Instances details
Category k => Functor (CodiagCoprod k) Source #

CodiagCoprod is the codiagonal functor for coproducts.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (CodiagCoprod k) :: Type -> Type -> Type Source #

type Cod (CodiagCoprod k) :: Type -> Type -> Type Source #

type (CodiagCoprod k) :% a Source #

type Cod (CodiagCoprod k) Source # 
Instance details

Defined in Data.Category.Coproduct

type Cod (CodiagCoprod k) = k
type Dom (CodiagCoprod k) Source # 
Instance details

Defined in Data.Category.Coproduct

type Dom (CodiagCoprod k) = k :++: k
type (CodiagCoprod k) :% (I1 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (CodiagCoprod k) :% (I1 a) = a
type (CodiagCoprod k) :% (I2 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (CodiagCoprod k) :% (I2 a) = a

newtype Cotuple1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a Source #

Constructors

Cotuple1 (Obj c1 a) 

Instances

Instances details
(Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) Source #

Cotuple1 projects out to the left category, replacing a value from the right category with a fixed object.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (Cotuple1 c1 c2 a1) :: Type -> Type -> Type Source #

type Cod (Cotuple1 c1 c2 a1) :: Type -> Type -> Type Source #

type (Cotuple1 c1 c2 a1) :% a Source #

Methods

(%) :: Cotuple1 c1 c2 a1 -> Dom (Cotuple1 c1 c2 a1) a b -> Cod (Cotuple1 c1 c2 a1) (Cotuple1 c1 c2 a1 :% a) (Cotuple1 c1 c2 a1 :% b) Source #

type Cod (Cotuple1 c1 c2 a1) Source # 
Instance details

Defined in Data.Category.Coproduct

type Cod (Cotuple1 c1 c2 a1) = c1
type Dom (Cotuple1 c1 c2 a1) Source # 
Instance details

Defined in Data.Category.Coproduct

type Dom (Cotuple1 c1 c2 a1) = c1 :++: c2
type (Cotuple1 c1 c2 a1) :% (I1 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (Cotuple1 c1 c2 a1) :% (I1 a) = a
type (Cotuple1 c1 c2 a1) :% (I2 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (Cotuple1 c1 c2 a1) :% (I2 a) = a1

newtype Cotuple2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a Source #

Constructors

Cotuple2 (Obj c2 a) 

Instances

Instances details
(Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) Source #

Cotuple2 projects out to the right category, replacing a value from the left category with a fixed object.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (Cotuple2 c1 c2 a2) :: Type -> Type -> Type Source #

type Cod (Cotuple2 c1 c2 a2) :: Type -> Type -> Type Source #

type (Cotuple2 c1 c2 a2) :% a Source #

Methods

(%) :: Cotuple2 c1 c2 a2 -> Dom (Cotuple2 c1 c2 a2) a b -> Cod (Cotuple2 c1 c2 a2) (Cotuple2 c1 c2 a2 :% a) (Cotuple2 c1 c2 a2 :% b) Source #

type Cod (Cotuple2 c1 c2 a2) Source # 
Instance details

Defined in Data.Category.Coproduct

type Cod (Cotuple2 c1 c2 a2) = c2
type Dom (Cotuple2 c1 c2 a2) Source # 
Instance details

Defined in Data.Category.Coproduct

type Dom (Cotuple2 c1 c2 a2) = c1 :++: c2
type (Cotuple2 c1 c2 a2) :% (I1 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (Cotuple2 c1 c2 a2) :% (I1 a) = a2
type (Cotuple2 c1 c2 a2) :% (I2 a) Source # 
Instance details

Defined in Data.Category.Coproduct

type (Cotuple2 c1 c2 a2) :% (I2 a) = a

data Cograph c d f :: Type -> Type -> Type where Source #

Constructors

I1A :: c a1 b1 -> Cograph c d f (I1 a1) (I1 b1) 
I2A :: d a2 b2 -> Cograph c d f (I2 a2) (I2 b2) 
I12 :: Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph c d f (I1 a) (I2 b) 

Instances

Instances details
ProfunctorOf c d f => Category (Cograph c d f :: Type -> Type -> Type) Source #

The cograph of the profunctor f.

Instance details

Defined in Data.Category.Coproduct

Methods

src :: forall (a :: k) (b :: k). Cograph c d f a b -> Obj (Cograph c d f) a Source #

tgt :: forall (a :: k) (b :: k). Cograph c d f a b -> Obj (Cograph c d f) b Source #

(.) :: forall (b :: k) (c0 :: k) (a :: k). Cograph c d f b c0 -> Cograph c d f a b -> Cograph c d f a c0 Source #

newtype (c1 :>>: c2) a b Source #

The directed coproduct category of categories c1 and c2.

Constructors

DC (Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b) 

Instances

Instances details
(Category c1, Category c2) => Category (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) Source # 
Instance details

Defined in Data.Category.Coproduct

Methods

src :: forall (a :: k) (b :: k). (c1 :>>: c2) a b -> Obj (c1 :>>: c2) a Source #

tgt :: forall (a :: k) (b :: k). (c1 :>>: c2) a b -> Obj (c1 :>>: c2) b Source #

(.) :: forall (b :: k) (c :: k) (a :: k). (c1 :>>: c2) b c -> (c1 :>>: c2) a b -> (c1 :>>: c2) a c Source #

(HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) Source # 
Instance details

Defined in Data.Category.Limit

Associated Types

type BinaryCoproduct (c1 :>>: c2) x y :: Kind k Source #

Methods

inj1 :: forall (x :: k) (y :: k). Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) x (BinaryCoproduct (c1 :>>: c2) x y) Source #

inj2 :: forall (x :: k) (y :: k). Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) y (BinaryCoproduct (c1 :>>: c2) x y) Source #

(|||) :: forall (x :: k) (a :: k) (y :: k). (c1 :>>: c2) x a -> (c1 :>>: c2) y a -> (c1 :>>: c2) (BinaryCoproduct (c1 :>>: c2) x y) a Source #

(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). (c1 :>>: c2) a1 b1 -> (c1 :>>: c2) a2 b2 -> (c1 :>>: c2) (BinaryCoproduct (c1 :>>: c2) a1 a2) (BinaryCoproduct (c1 :>>: c2) b1 b2) Source #

(HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) Source # 
Instance details

Defined in Data.Category.Limit

Associated Types

type BinaryProduct (c1 :>>: c2) x y :: Kind k Source #

Methods

proj1 :: forall (x :: k) (y :: k). Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) x y) x Source #

proj2 :: forall (x :: k) (y :: k). Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) x y) y Source #

(&&&) :: forall (a :: k) (x :: k) (y :: k). (c1 :>>: c2) a x -> (c1 :>>: c2) a y -> (c1 :>>: c2) a (BinaryProduct (c1 :>>: c2) x y) Source #

(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). (c1 :>>: c2) a1 b1 -> (c1 :>>: c2) a2 b2 -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) a1 a2) (BinaryProduct (c1 :>>: c2) b1 b2) Source #

(HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) Source #

The initial object of the direct coproduct of categories is the initial object of the initial category.

Instance details

Defined in Data.Category.Limit

Associated Types

type InitialObject (c1 :>>: c2) :: Kind k Source #

Methods

initialObject :: Obj (c1 :>>: c2) (InitialObject (c1 :>>: c2)) Source #

initialize :: forall (a :: k). Obj (c1 :>>: c2) a -> (c1 :>>: c2) (InitialObject (c1 :>>: c2)) a Source #

(Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) Source #

The terminal object of the direct coproduct of categories is the terminal object of the terminal category.

Instance details

Defined in Data.Category.Limit

Associated Types

type TerminalObject (c1 :>>: c2) :: Kind k Source #

Methods

terminalObject :: Obj (c1 :>>: c2) (TerminalObject (c1 :>>: c2)) Source #

terminate :: forall (a :: k). Obj (c1 :>>: c2) a -> (c1 :>>: c2) a (TerminalObject (c1 :>>: c2)) Source #

(HasTerminalObject (i :>>: j), Category i, Category j, Category k) => HasColimits (i :>>: j) k Source #

The colimit of any diagram with a terminal object, has the limit at the terminal object.

Instance details

Defined in Data.Category.Limit

Associated Types

type ColimitFam (i :>>: j) k f Source #

Methods

colimit :: Obj (Nat (i :>>: j) k) f -> Cocone (i :>>: j) k f (ColimitFam (i :>>: j) k f) Source #

colimitFactorizer :: Cocone (i :>>: j) k f n -> k (ColimitFam (i :>>: j) k f) n Source #

(HasInitialObject (i :>>: j), Category i, Category j, Category k) => HasLimits (i :>>: j) k Source #

The limit of any diagram with an initial object, has the limit at the initial object.

Instance details

Defined in Data.Category.Limit

Associated Types

type LimitFam (i :>>: j) k f Source #

Methods

limit :: Obj (Nat (i :>>: j) k) f -> Cone (i :>>: j) k f (LimitFam (i :>>: j) k f) Source #

limitFactorizer :: Cone (i :>>: j) k f n -> k n (LimitFam (i :>>: j) k f) Source #

type InitialObject (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) Source # 
Instance details

Defined in Data.Category.Limit

type InitialObject (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) = I1 (InitialObject c1)
type TerminalObject (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) = I1 (BinaryCoproduct c1 a b)
type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) = I2 b
type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) = I2 a
type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) = I2 (BinaryCoproduct c2 a b)
type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) = I1 (BinaryProduct c1 a b)
type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I1 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) = I1 a
type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I1 b :: Kind (c1 :>>: c2)) = I1 b
type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) (I2 a :: Kind (c1 :>>: c2)) (I2 b :: Kind (c1 :>>: c2)) = I2 (BinaryProduct c2 a b)
type ColimitFam (i :>>: j) k f Source # 
Instance details

Defined in Data.Category.Limit

type ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)
type LimitFam (i :>>: j) k f Source # 
Instance details

Defined in Data.Category.Limit

type LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)

newtype NatAsFunctor f g Source #

Constructors

NatAsFunctor (Nat (Dom f) (Cod f) f g) 

Instances

Instances details
(Functor f, Functor g, Dom f ~ Dom g, Cod f ~ Cod g) => Functor (NatAsFunctor f g) Source #

A natural transformation Nat c d is isomorphic to a functor from c :**: 2 to d.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (NatAsFunctor f g) :: Type -> Type -> Type Source #

type Cod (NatAsFunctor f g) :: Type -> Type -> Type Source #

type (NatAsFunctor f g) :% a Source #

Methods

(%) :: NatAsFunctor f g -> Dom (NatAsFunctor f g) a b -> Cod (NatAsFunctor f g) (NatAsFunctor f g :% a) (NatAsFunctor f g :% b) Source #

type Cod (NatAsFunctor f g) Source # 
Instance details

Defined in Data.Category.Coproduct

type Cod (NatAsFunctor f g) = Cod f
type Dom (NatAsFunctor f g) Source # 
Instance details

Defined in Data.Category.Coproduct

type (NatAsFunctor f g) :% (a, I1 ()) Source # 
Instance details

Defined in Data.Category.Coproduct

type (NatAsFunctor f g) :% (a, I1 ()) = f :% a
type (NatAsFunctor f g) :% (a, I2 ()) Source # 
Instance details

Defined in Data.Category.Coproduct

type (NatAsFunctor f g) :% (a, I2 ()) = g :% a