{-# LANGUAGE
  FlexibleContexts,
  FlexibleInstances,
  GADTs,
  PolyKinds,
  DataKinds,
  MultiParamTypeClasses,
  RankNTypes,
  ScopedTypeVariables,
  TypeOperators,
  TypeFamilies,
  TypeSynonymInstances,
  UndecidableInstances,
  NoImplicitPrelude  #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Limit
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.Limit (

  -- * Preliminairies

  -- ** Diagonal Functor
    Diag(..)
  , DiagF

  -- ** Cones
  , Cone
  , Cocone
  , coneVertex
  , coconeVertex

  -- * Limits
  , LimitFam
  , Limit
  , HasLimits(..)
  , LimitFunctor(..)
  , limitAdj
  , adjLimit
  , adjLimitFactorizer
  , rightAdjointPreservesLimits
  , rightAdjointPreservesLimitsInv

  -- * Colimits
  , ColimitFam
  , Colimit
  , HasColimits(..)
  , ColimitFunctor(..)
  , colimitAdj
  , adjColimit
  , adjColimitFactorizer
  , leftAdjointPreservesColimits
  , leftAdjointPreservesColimitsInv

  -- ** Limits of type Void
  , HasTerminalObject(..)
  , HasInitialObject(..)
  , Zero

  -- ** Limits of type Pair
  , HasBinaryProducts(..)
  , ProductFunctor(..)
  , (:*:)(..)
  , prodAdj
  , HasBinaryCoproducts(..)
  , CoproductFunctor(..)
  , (:+:)(..)
  , coprodAdj

) where

import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Adjunction

import Data.Category.Product
import Data.Category.Coproduct
import Data.Category.Unit
import Data.Category.Void

infixl 3 ***
infixl 3 &&&
infixl 2 +++
infixl 2 |||


data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
  Diag :: Diag j k

-- | The diagonal functor from (index-) category J to k.
instance (Category j, Category k) => Functor (Diag j k) where
  type Dom (Diag j k) = k
  type Cod (Diag j k) = Nat j k
  type Diag j k :% a = Const j k a

  Diag j k
Diag % :: Diag j k
-> Dom (Diag j k) a b
-> Cod (Diag j k) (Diag j k :% a) (Diag j k :% b)
% Dom (Diag j k) a b
f = Const j k a
-> Const j k b
-> (forall z. Obj j z -> Component (Const j k a) (Const j k b) z)
-> Nat j k (Const j k a) (Const j k b)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj k a -> Const j k a
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (k a b -> Obj k a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a b
Dom (Diag j k) a b
f)) (Obj k b -> Const j k b
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (k a b -> Obj k b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a b
Dom (Diag j k) a b
f)) (\Obj j z
_ -> Dom (Diag j k) a b
Component (Const j k a) (Const j k b) z
f)

-- | The diagonal functor with the same domain and codomain as @f@.
type DiagF f = Diag (Dom f) (Cod f)



-- | A cone from N to F is a natural transformation from the constant functor to N to F.
type Cone   j k f n = Nat j k (Const j k n) f

-- | A co-cone from F to N is a natural transformation from F to the constant functor to N.
type Cocone j k f n = Nat j k f (Const j k n)


-- | The vertex (or apex) of a cone.
coneVertex :: Cone j k f n -> Obj k n
coneVertex :: Cone j k f n -> Obj k n
coneVertex (Nat (Const Obj k n
x) f
_ forall z. Obj j z -> Component (Const j k n) f z
_) = Obj k n
x

-- | The vertex (or apex) of a co-cone.
coconeVertex :: Cocone j k f n -> Obj k n
coconeVertex :: Cocone j k f n -> Obj k n
coconeVertex (Nat f
_ (Const Obj k n
x) forall z. Obj j z -> Component f (Const j k n) z
_) = Obj k n
x



-- | Limits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.
type family LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *

type Limit f = LimitFam (Dom f) (Cod f) f

-- | An instance of @HasLimits j k@ says that @k@ has all limits of type @j@.
class (Category j, Category k) => HasLimits j k where
  -- | 'limit' returns the limiting cone for a functor @f@.
  limit           :: Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
  -- | 'limitFactorizer' shows that the limiting cone is universal – i.e. any other cone of @f@ factors through it
  --   by returning the morphism between the vertices of the cones.
  limitFactorizer :: Cone j k f n -> k n (LimitFam j k f)

data LimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = LimitFunctor
-- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor.
--   It can be seen as a generalisation of @(***)@.
instance HasLimits j k => Functor (LimitFunctor j k) where
  type Dom (LimitFunctor j k) = Nat j k
  type Cod (LimitFunctor j k) = k
  type LimitFunctor j k :% f = LimitFam j k f

  LimitFunctor j k
LimitFunctor % :: LimitFunctor j k
-> Dom (LimitFunctor j k) a b
-> Cod
     (LimitFunctor j k) (LimitFunctor j k :% a) (LimitFunctor j k :% b)
% Dom (LimitFunctor j k) a b
n = Cone j k b (LimitFam j k a) -> k (LimitFam j k a) (LimitFam j k b)
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (Dom (LimitFunctor j k) a b
Nat j k a b
n Nat j k a b
-> Nat j k (Const j k (LimitFam j k a)) a
-> Cone j k b (LimitFam j k a)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj (Nat j k) a -> Nat j k (Const j k (LimitFam j k a)) a
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit (Nat j k a b -> Obj (Nat j k) a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (LimitFunctor j k) a b
Nat j k a b
n))

-- | The limit functor is right adjoint to the diagonal functor.
limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
limitAdj :: Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
limitAdj = Diag j k
-> LimitFunctor j k
-> (forall a b.
    Obj k a
    -> Nat j k (Diag j k :% a) b -> k a (LimitFunctor j k :% b))
-> (forall a.
    Obj (Nat j k) a
    -> Component (Diag j k :.: LimitFunctor j k) (Id (Nat j k)) a)
-> Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionCounit Diag j k
forall (j :: * -> * -> *) (k :: * -> * -> *). Diag j k
Diag LimitFunctor j k
forall (j :: * -> * -> *) (k :: * -> * -> *). LimitFunctor j k
LimitFunctor (\Obj k a
_ -> Nat j k (Diag j k :% a) b -> k a (LimitFunctor j k :% b)
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer) forall a.
Obj (Nat j k) a
-> Component (Diag j k :.: LimitFunctor j k) (Id (Nat j k)) a
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit

adjLimit :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Obj (Nat j k) f -> Cone j k f (r :% f)
adjLimit :: Adjunction (Nat j k) k (Diag j k) r
-> Obj (Nat j k) f -> Cone j k f (r :% f)
adjLimit Adjunction (Nat j k) k (Diag j k) r
adj Obj (Nat j k) f
f = Adjunction (Nat j k) k (Diag j k) r
-> Nat (Nat j k) (Nat j k) (Diag j k :.: r) (Id (Nat j k))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit Adjunction (Nat j k) k (Diag j k) r
adj Nat (Nat j k) (Nat j k) (Diag j k :.: r) (Id (Nat j k))
-> Obj (Nat j k) f
-> Nat j k ((Diag j k :.: r) :% f) (Id (Nat j k) :% f)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj (Nat j k) f
f

adjLimitFactorizer :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Cone j k f n -> k n (r :% f)
adjLimitFactorizer :: Adjunction (Nat j k) k (Diag j k) r -> Cone j k f n -> k n (r :% f)
adjLimitFactorizer Adjunction (Nat j k) k (Diag j k) r
adj Cone j k f n
cone = Adjunction (Nat j k) k (Diag j k) r
-> Obj k n -> Nat j k (Diag j k :% n) f -> k n (r :% f)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct Adjunction (Nat j k) k (Diag j k) r
adj (Cone j k f n -> Obj k n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
coneVertex Cone j k f n
cone) Cone j k f n
Nat j k (Diag j k :% n) f
cone


-- Cone (g :.: t) (Limit (g :.: t))
-- Obj j z -> d (Limit (g :.: t)) ((g :.: t) :% z)
-- Obj j z -> d (f :% Limit (g :.: t)) (t :% z)
-- Cone t (f :% Limit (g :.: t))
-- d (f :% Limit (g :.: t)) (Limit t)
-- d (Limit (g :.: t)) (g :% Limit t)
rightAdjointPreservesLimits
  :: (HasLimits j c, HasLimits j d)
  => Adjunction c d f g -> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t)
rightAdjointPreservesLimits :: Adjunction c d f g
-> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t)
rightAdjointPreservesLimits adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) (Nat t
t t
_ forall z. Obj j z -> Component t t z
_) =
  Adjunction c d f g
-> Obj d (LimitFam j d (g :.: t))
-> c (f :% LimitFam j d (g :.: t)) (LimitFam j c t)
-> d (LimitFam j d (g :.: t)) (g :% LimitFam j c t)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct Adjunction c d f g
adj Obj d (LimitFam j d (g :.: t))
x (Cone j c t (f :% LimitFam j d (g :.: t))
-> c (f :% LimitFam j d (g :.: t)) (LimitFam j c t)
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer Cone j c t (f :% LimitFam j d (g :.: t))
cone)
    where
      l :: Cone j d (g :.: t) (LimitFam j d (g :.: t))
l = Obj (Nat j d) (g :.: t)
-> Cone j d (g :.: t) (LimitFam j d (g :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit ((g :.: t)
-> Nat (Dom (g :.: t)) (Cod (g :.: t)) (g :.: t) (g :.: t)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (g
g g -> t -> g :.: t
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: t
t))
      x :: Obj d (LimitFam j d (g :.: t))
x = Cone j d (g :.: t) (LimitFam j d (g :.: t))
-> Obj d (LimitFam j d (g :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
coneVertex Cone j d (g :.: t) (LimitFam j d (g :.: t))
l
      -- cone :: Cone t (f :% Limit (g :.: t))
      cone :: Cone j c t (f :% LimitFam j d (g :.: t))
cone = Const j c (f :% LimitFam j d (g :.: t))
-> t
-> (forall z.
    Obj j z -> Component (Const j c (f :% LimitFam j d (g :.: t))) t z)
-> Cone j c t (f :% LimitFam j d (g :.: t))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj c (f :% LimitFam j d (g :.: t))
-> Const j c (f :% LimitFam j d (g :.: t))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f
-> Dom f (LimitFam j d (g :.: t)) (LimitFam j d (g :.: t))
-> Cod
     f (f :% LimitFam j d (g :.: t)) (f :% LimitFam j d (g :.: t))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj d (LimitFam j d (g :.: t))
Dom f (LimitFam j d (g :.: t)) (LimitFam j d (g :.: t))
x)) t
t (\Obj j z
z -> Adjunction c d f g
-> Obj c (t :% z)
-> d (LimitFam j d (g :.: t)) (g :% (t :% z))
-> c (f :% LimitFam j d (g :.: t)) (t :% z)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct Adjunction c d f g
adj (t
t t -> Dom t z z -> Cod t (t :% z) (t :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj j z
Dom t z z
z) (Cone j d (g :.: t) (LimitFam j d (g :.: t))
l Cone j d (g :.: t) (LimitFam j d (g :.: t))
-> Obj j z
-> d (Const j d (LimitFam j d (g :.: t)) :% z) ((g :.: t) :% z)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj j z
z))

-- Cone t (Limit t)
-- Cone (g :.: t) (g :% Limit t)
-- d (g :% Limit t) (Limit (g :.: t))
rightAdjointPreservesLimitsInv
  :: (HasLimits j c, HasLimits j d)
  => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% LimitFam j c t) (LimitFam j d (g :.: t))
rightAdjointPreservesLimitsInv :: Obj (Nat c d) g
-> Obj (Nat j c) t
-> d (g :% LimitFam j c t) (LimitFam j d (g :.: t))
rightAdjointPreservesLimitsInv Obj (Nat c d) g
g Obj (Nat j c) t
t = Cone j d (g :.: t) (g :% LimitFam j c t)
-> d (g :% LimitFam j c t) (LimitFam j d (g :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (Nat j d (g :.: Const j c (LimitFam j c t)) (g :.: t)
-> Cone j d (g :.: t) (g :% LimitFam j c t)
forall (j :: * -> * -> *) (d :: * -> * -> *) f (c :: * -> * -> *) x
       g.
Nat j d (f :.: Const j c x) g -> Nat j d (Const j d (f :% x)) g
constPrecompIn (Obj (Nat c d) g
g Obj (Nat c d) g
-> Nat j c (Const j c (LimitFam j c t)) t
-> Nat j d (g :.: Const j c (LimitFam j c t)) (g :.: t)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Obj (Nat j c) t -> Nat j c (Const j c (LimitFam j c t)) t
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit Obj (Nat j c) t
t))

-- | Colimits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.
type family ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *

type Colimit f = ColimitFam (Dom f) (Cod f) f

-- | An instance of @HasColimits j k@ says that @k@ has all colimits of type @j@.
class (Category j, Category k) => HasColimits j k where
  -- | 'colimit' returns the limiting co-cone for a functor @f@.
  colimit           :: Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
  -- | 'colimitFactorizer' shows that the limiting co-cone is universal – i.e. any other co-cone of @f@ factors through it
  --   by returning the morphism between the vertices of the cones.
  colimitFactorizer :: Cocone j k f n -> k (ColimitFam j k f) n

data ColimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = ColimitFunctor
-- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor.
--   It can be seen as a generalisation of @(+++)@.
instance HasColimits j k => Functor (ColimitFunctor j k) where
  type Dom (ColimitFunctor j k) = Nat j k
  type Cod (ColimitFunctor j k) = k
  type ColimitFunctor j k :% f = ColimitFam j k f

  ColimitFunctor j k
ColimitFunctor % :: ColimitFunctor j k
-> Dom (ColimitFunctor j k) a b
-> Cod
     (ColimitFunctor j k)
     (ColimitFunctor j k :% a)
     (ColimitFunctor j k :% b)
% Dom (ColimitFunctor j k) a b
n = Cocone j k a (ColimitFam j k b)
-> k (ColimitFam j k a) (ColimitFam j k b)
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (Obj (Nat j k) b -> Cocone j k b (ColimitFam j k b)
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit (Nat j k a b -> Obj (Nat j k) b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (ColimitFunctor j k) a b
Nat j k a b
n) Cocone j k b (ColimitFam j k b)
-> Nat j k a b -> Cocone j k a (ColimitFam j k b)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Dom (ColimitFunctor j k) a b
Nat j k a b
n)

-- | The colimit functor is left adjoint to the diagonal functor.
colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
colimitAdj :: Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
colimitAdj = ColimitFunctor j k
-> Diag j k
-> (forall a.
    Obj (Nat j k) a
    -> Component (Id (Nat j k)) (Diag j k :.: ColimitFunctor j k) a)
-> (forall a b.
    Obj k b
    -> Nat j k a (Diag j k :% b) -> k (ColimitFunctor j k :% a) b)
-> Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionUnit ColimitFunctor j k
forall (j :: * -> * -> *) (k :: * -> * -> *). ColimitFunctor j k
ColimitFunctor Diag j k
forall (j :: * -> * -> *) (k :: * -> * -> *). Diag j k
Diag forall a.
Obj (Nat j k) a
-> Component (Id (Nat j k)) (Diag j k :.: ColimitFunctor j k) a
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit (\Obj k b
_ -> Nat j k a (Diag j k :% b) -> k (ColimitFunctor j k :% a) b
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer)

adjColimit :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Obj (Nat j k) f -> Cocone j k f (l :% f)
adjColimit :: Adjunction k (Nat j k) l (Diag j k)
-> Obj (Nat j k) f -> Cocone j k f (l :% f)
adjColimit Adjunction k (Nat j k) l (Diag j k)
adj Obj (Nat j k) f
f = Adjunction k (Nat j k) l (Diag j k)
-> Nat (Nat j k) (Nat j k) (Id (Nat j k)) (Diag j k :.: l)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction k (Nat j k) l (Diag j k)
adj Nat (Nat j k) (Nat j k) (Id (Nat j k)) (Diag j k :.: l)
-> Obj (Nat j k) f
-> Nat j k (Id (Nat j k) :% f) ((Diag j k :.: l) :% f)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj (Nat j k) f
f

adjColimitFactorizer :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Cocone j k f n -> k (l :% f) n
adjColimitFactorizer :: Adjunction k (Nat j k) l (Diag j k)
-> Cocone j k f n -> k (l :% f) n
adjColimitFactorizer Adjunction k (Nat j k) l (Diag j k)
adj Cocone j k f n
cocone = Adjunction k (Nat j k) l (Diag j k)
-> Obj k n -> Nat j k f (Diag j k :% n) -> k (l :% f) n
forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct Adjunction k (Nat j k) l (Diag j k)
adj (Cocone j k f n -> Obj k n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex Cocone j k f n
cocone) Cocone j k f n
Nat j k f (Diag j k :% n)
cocone


leftAdjointPreservesColimits
  :: (HasColimits j c, HasColimits j d)
  => Adjunction c d f g -> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t))
leftAdjointPreservesColimits :: Adjunction c d f g
-> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t))
leftAdjointPreservesColimits adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) (Nat t
t t
_ forall z. Obj j z -> Component t t z
_) =
  Adjunction c d f g
-> Obj c (ColimitFam j c (f :.: t))
-> d (ColimitFam j d t) (g :% ColimitFam j c (f :.: t))
-> c (f :% ColimitFam j d t) (ColimitFam j c (f :.: t))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct Adjunction c d f g
adj Obj c (ColimitFam j c (f :.: t))
x (Cocone j d t (g :% ColimitFam j c (f :.: t))
-> d (ColimitFam j d t) (g :% ColimitFam j c (f :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer Cocone j d t (g :% ColimitFam j c (f :.: t))
cocone)
    where
      l :: Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
l = Obj (Nat j c) (f :.: t)
-> Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit ((f :.: t)
-> Nat (Dom (f :.: t)) (Cod (f :.: t)) (f :.: t) (f :.: t)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (f
f f -> t -> f :.: t
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: t
t))
      x :: Obj c (ColimitFam j c (f :.: t))
x = Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
-> Obj c (ColimitFam j c (f :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
l
      cocone :: Cocone j d t (g :% ColimitFam j c (f :.: t))
cocone = t
-> Const j d (g :% ColimitFam j c (f :.: t))
-> (forall z.
    Obj j z
    -> Component t (Const j d (g :% ColimitFam j c (f :.: t))) z)
-> Cocone j d t (g :% ColimitFam j c (f :.: t))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat t
t (Obj d (g :% ColimitFam j c (f :.: t))
-> Const j d (g :% ColimitFam j c (f :.: t))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (g
g g
-> Dom g (ColimitFam j c (f :.: t)) (ColimitFam j c (f :.: t))
-> Cod
     g (g :% ColimitFam j c (f :.: t)) (g :% ColimitFam j c (f :.: t))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c (ColimitFam j c (f :.: t))
Dom g (ColimitFam j c (f :.: t)) (ColimitFam j c (f :.: t))
x)) (\Obj j z
z -> Adjunction c d f g
-> Obj d (t :% z)
-> c (f :% (t :% z)) (ColimitFam j c (f :.: t))
-> d (t :% z) (g :% ColimitFam j c (f :.: t))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct Adjunction c d f g
adj (t
t t -> Dom t z z -> Cod t (t :% z) (t :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj j z
Dom t z z
z) (Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
l Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
-> Obj j z
-> c ((f :.: t) :% z) (Const j c (ColimitFam j c (f :.: t)) :% z)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj j z
z))

leftAdjointPreservesColimitsInv
  :: (HasColimits j c, HasColimits j d)
  => Obj (Nat d c) f -> Obj (Nat j d) t -> c (ColimitFam j c (f :.: t)) (f :% ColimitFam j d t)
leftAdjointPreservesColimitsInv :: Obj (Nat d c) f
-> Obj (Nat j d) t
-> c (ColimitFam j c (f :.: t)) (f :% ColimitFam j d t)
leftAdjointPreservesColimitsInv Obj (Nat d c) f
f Obj (Nat j d) t
t = Cocone j c (f :.: t) (f :% ColimitFam j d t)
-> c (ColimitFam j c (f :.: t)) (f :% ColimitFam j d t)
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (Nat j c (f :.: t) (f :.: Const j d (ColimitFam j d t))
-> Cocone j c (f :.: t) (f :% ColimitFam j d t)
forall (j :: * -> * -> *) (d :: * -> * -> *) f g (c :: * -> * -> *)
       x.
Nat j d f (g :.: Const j c x) -> Nat j d f (Const j d (g :% x))
constPrecompOut (Obj (Nat d c) f
f Obj (Nat d c) f
-> Nat j d t (Const j d (ColimitFam j d t))
-> Nat j c (f :.: t) (f :.: Const j d (ColimitFam j d t))
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Obj (Nat j d) t -> Nat j d t (Const j d (ColimitFam j d t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit Obj (Nat j d) t
t))


class Category k => HasTerminalObject k where

  type TerminalObject k :: Kind k

  terminalObject :: Obj k (TerminalObject k)

  terminate :: Obj k a -> k a (TerminalObject k)


type instance LimitFam Void k f = TerminalObject k

-- | A terminal object is the limit of the functor from /0/ to k.
instance (Category k, HasTerminalObject k) => HasLimits Void k where

  limit :: Obj (Nat Void k) f -> Cone Void k f (LimitFam Void k f)
limit (Nat f
f f
_ forall z. Obj Void z -> Component f f z
_) = Const Void k (TerminalObject k)
-> f -> Nat Void k (Const Void k (TerminalObject k)) f
forall f g (d :: * -> * -> *).
(Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d,
 Cod g ~ d) =>
f -> g -> Nat Void d f g
voidNat (Obj k (TerminalObject k) -> Const Void k (TerminalObject k)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj k (TerminalObject k)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject) f
f
  limitFactorizer :: Cone Void k f n -> k n (LimitFam Void k f)
limitFactorizer = Obj k n -> k n (TerminalObject k)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate (Obj k n -> k n (TerminalObject k))
-> (Cone Void k f n -> Obj k n)
-> Cone Void k f n
-> k n (TerminalObject k)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cone Void k f n -> Obj k n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
coneVertex


-- | @()@ is the terminal object in @Hask@.
instance HasTerminalObject (->) where
  type TerminalObject (->) = ()

  terminalObject :: Obj (->) (TerminalObject (->))
terminalObject = \TerminalObject (->)
x -> TerminalObject (->)
x

  terminate :: Obj (->) a -> a -> TerminalObject (->)
terminate Obj (->) a
_ a
_ = ()

-- | @Unit@ is the terminal category.
instance HasTerminalObject Cat where
  type TerminalObject Cat = Unit

  terminalObject :: Obj Cat (TerminalObject Cat)
terminalObject = Id Unit -> Cat (Dom (Id Unit)) (Cod (Id Unit))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Id Unit
forall (k :: * -> * -> *). Id k
Id

  terminate :: Obj Cat a -> Cat a (TerminalObject Cat)
terminate (CatA ftag
_) = Const a Unit ()
-> Cat (Dom (Const a Unit ())) (Cod (Const a Unit ()))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA (Obj Unit () -> Const a Unit ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj Unit ()
Unit)

-- | The constant functor to the terminal object is itself the terminal object in its functor category.
instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) where
  type TerminalObject (Nat c d) = Const c d (TerminalObject d)

  terminalObject :: Obj (Nat c d) (TerminalObject (Nat c d))
terminalObject = Const c d (TerminalObject d)
-> Nat
     (Dom (Const c d (TerminalObject d)))
     (Cod (Const c d (TerminalObject d)))
     (Const c d (TerminalObject d))
     (Const c d (TerminalObject d))
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (Obj d (TerminalObject d) -> Const c d (TerminalObject d)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj d (TerminalObject d)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject)

  terminate :: Obj (Nat c d) a -> Nat c d a (TerminalObject (Nat c d))
terminate (Nat a
f a
_ forall z. Obj c z -> Component a a z
_) = a
-> Const c d (TerminalObject d)
-> (forall z.
    Obj c z -> Component a (Const c d (TerminalObject d)) z)
-> Nat c d a (Const c d (TerminalObject d))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat a
f (Obj d (TerminalObject d) -> Const c d (TerminalObject d)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj d (TerminalObject d)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject) (Obj d (a :% z) -> d (a :% z) (TerminalObject d)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate (Obj d (a :% z) -> d (a :% z) (TerminalObject d))
-> (c z z -> Obj d (a :% z))
-> c z z
-> d (a :% z) (TerminalObject d)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (a
f a -> Dom a z z -> Cod a (a :% z) (a :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
%))

-- | The category of one object has that object as terminal object.
instance HasTerminalObject Unit where
  type TerminalObject Unit = ()

  terminalObject :: Obj Unit (TerminalObject Unit)
terminalObject = Obj Unit ()
Obj Unit (TerminalObject Unit)
Unit

  terminate :: Obj Unit a -> Unit a (TerminalObject Unit)
terminate Obj Unit a
Unit = Unit a (TerminalObject Unit)
Obj Unit ()
Unit

-- | The terminal object of the product of 2 categories is the product of their terminal objects.
instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2) where
  type TerminalObject (c1 :**: c2) = (TerminalObject c1, TerminalObject c2)

  terminalObject :: Obj (c1 :**: c2) (TerminalObject (c1 :**: c2))
terminalObject = Obj c1 (TerminalObject c1)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject Obj c1 (TerminalObject c1)
-> c2 (TerminalObject c2) (TerminalObject c2)
-> (:**:)
     c1
     c2
     (TerminalObject c1, TerminalObject c2)
     (TerminalObject c1, TerminalObject c2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: c2 (TerminalObject c2) (TerminalObject c2)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject

  terminate :: Obj (c1 :**: c2) a -> (:**:) c1 c2 a (TerminalObject (c1 :**: c2))
terminate (c1 a1 b1
a1 :**: c2 a2 b2
a2) = Obj c1 a1 -> c1 a1 (TerminalObject c1)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj c1 a1
c1 a1 b1
a1 c1 a1 (TerminalObject c1)
-> c2 a2 (TerminalObject c2)
-> (:**:) c1 c2 (a1, a2) (TerminalObject c1, TerminalObject c2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> c2 a2 (TerminalObject c2)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj c2 a2
c2 a2 b2
a2

-- | The terminal object of the direct coproduct of categories is the terminal object of the terminal category.
instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2) where
  type TerminalObject (c1 :>>: c2) = I2 (TerminalObject c2)

  terminalObject :: Obj (c1 :>>: c2) (TerminalObject (c1 :>>: c2))
terminalObject = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I2 (TerminalObject c2))
  (I2 (TerminalObject c2))
-> (:>>:) c1 c2 (I2 (TerminalObject c2)) (I2 (TerminalObject c2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c2 (TerminalObject c2) (TerminalObject c2)
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I2 (TerminalObject c2))
     (I2 (TerminalObject c2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A c2 (TerminalObject c2) (TerminalObject c2)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject)

  terminate :: Obj (c1 :>>: c2) a -> (:>>:) c1 c2 a (TerminalObject (c1 :>>: c2))
terminate (DC (I1A c a1 b1
a)) = Cograph
  (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 (TerminalObject c2))
-> (:>>:) c1 c2 (I1 a1) (I2 (TerminalObject c2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a1
-> c2 (TerminalObject c2) (TerminalObject c2)
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a1, TerminalObject c2))
-> Cograph
     (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 (TerminalObject c2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a1
c a1 b1
a c2 (TerminalObject c2) (TerminalObject c2)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
  terminate (DC (I2A d a2 b2
a)) = Cograph
  (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 (TerminalObject c2))
-> (:>>:) c1 c2 (I2 a2) (I2 (TerminalObject c2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 (TerminalObject c2)
-> Cograph
     (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 (TerminalObject c2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (Obj d a2 -> d a2 (TerminalObject d)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj d a2
d a2 b2
a))



class Category k => HasInitialObject k where
  type InitialObject k :: Kind k

  initialObject :: Obj k (InitialObject k)

  initialize :: Obj k a -> k (InitialObject k) a


type instance ColimitFam Void k f = InitialObject k

-- | An initial object is the colimit of the functor from /0/ to k.
instance (Category k, HasInitialObject k) => HasColimits Void k where

  colimit :: Obj (Nat Void k) f -> Cocone Void k f (ColimitFam Void k f)
colimit (Nat f
f f
_ forall z. Obj Void z -> Component f f z
_) = f
-> Const Void k (InitialObject k)
-> Nat Void k f (Const Void k (InitialObject k))
forall f g (d :: * -> * -> *).
(Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d,
 Cod g ~ d) =>
f -> g -> Nat Void d f g
voidNat f
f (Obj k (InitialObject k) -> Const Void k (InitialObject k)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj k (InitialObject k)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)
  colimitFactorizer :: Cocone Void k f n -> k (ColimitFam Void k f) n
colimitFactorizer = Obj k n -> k (InitialObject k) n
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize (Obj k n -> k (InitialObject k) n)
-> (Cocone Void k f n -> Obj k n)
-> Cocone Void k f n
-> k (InitialObject k) n
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cocone Void k f n -> Obj k n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex


data Zero

-- | Any empty data type is an initial object in @Hask@.
instance HasInitialObject (->) where
  type InitialObject (->) = Zero

  initialObject :: Obj (->) (InitialObject (->))
initialObject = \InitialObject (->)
x -> InitialObject (->)
x

  initialize :: Obj (->) a -> InitialObject (->) -> a
initialize = Obj (->) a -> InitialObject (->) -> a
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize

-- | The empty category is the initial object in @Cat@.
instance HasInitialObject Cat where
  type InitialObject Cat = Void

  initialObject :: Obj Cat (InitialObject Cat)
initialObject = Id Void -> Cat (Dom (Id Void)) (Cod (Id Void))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Id Void
forall (k :: * -> * -> *). Id k
Id

  initialize :: Obj Cat a -> Cat (InitialObject Cat) a
initialize (CatA ftag
_) = Magic a -> Cat (Dom (Magic a)) (Cod (Magic a))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Magic a
forall (k :: * -> * -> *). Magic k
Magic

-- | The constant functor to the initial object is itself the initial object in its functor category.
instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d) where
  type InitialObject (Nat c d) = Const c d (InitialObject d)

  initialObject :: Obj (Nat c d) (InitialObject (Nat c d))
initialObject = Const c d (InitialObject d)
-> Nat
     (Dom (Const c d (InitialObject d)))
     (Cod (Const c d (InitialObject d)))
     (Const c d (InitialObject d))
     (Const c d (InitialObject d))
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (Obj d (InitialObject d) -> Const c d (InitialObject d)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj d (InitialObject d)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)

  initialize :: Obj (Nat c d) a -> Nat c d (InitialObject (Nat c d)) a
initialize (Nat a
f a
_ forall z. Obj c z -> Component a a z
_) = Const c d (InitialObject d)
-> a
-> (forall z.
    Obj c z -> Component (Const c d (InitialObject d)) a z)
-> Nat c d (Const c d (InitialObject d)) a
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj d (InitialObject d) -> Const c d (InitialObject d)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj d (InitialObject d)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject) a
f (Obj d (a :% z) -> d (InitialObject d) (a :% z)
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize (Obj d (a :% z) -> d (InitialObject d) (a :% z))
-> (c z z -> Obj d (a :% z))
-> c z z
-> d (InitialObject d) (a :% z)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (a
f a -> Dom a z z -> Cod a (a :% z) (a :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
%))

-- | The initial object of the product of 2 categories is the product of their initial objects.
instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2) where
  type InitialObject (c1 :**: c2) = (InitialObject c1, InitialObject c2)

  initialObject :: Obj (c1 :**: c2) (InitialObject (c1 :**: c2))
initialObject = Obj c1 (InitialObject c1)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject Obj c1 (InitialObject c1)
-> c2 (InitialObject c2) (InitialObject c2)
-> (:**:)
     c1
     c2
     (InitialObject c1, InitialObject c2)
     (InitialObject c1, InitialObject c2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: c2 (InitialObject c2) (InitialObject c2)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject

  initialize :: Obj (c1 :**: c2) a -> (:**:) c1 c2 (InitialObject (c1 :**: c2)) a
initialize (c1 a1 b1
a1 :**: c2 a2 b2
a2) = Obj c1 a1 -> c1 (InitialObject c1) a1
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj c1 a1
c1 a1 b1
a1 c1 (InitialObject c1) a1
-> c2 (InitialObject c2) a2
-> (:**:) c1 c2 (InitialObject c1, InitialObject c2) (a1, a2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> c2 (InitialObject c2) a2
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj c2 a2
c2 a2 b2
a2

-- | The category of one object has that object as initial object.
instance HasInitialObject Unit where
  type InitialObject Unit = ()

  initialObject :: Obj Unit (InitialObject Unit)
initialObject = Obj Unit ()
Obj Unit (InitialObject Unit)
Unit

  initialize :: Obj Unit a -> Unit (InitialObject Unit) a
initialize Obj Unit a
Unit = Obj Unit ()
Unit (InitialObject Unit) a
Unit

-- | The initial object of the direct coproduct of categories is the initial object of the initial category.
instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2) where
  type InitialObject (c1 :>>: c2) = I1 (InitialObject c1)

  initialObject :: Obj (c1 :>>: c2) (InitialObject (c1 :>>: c2))
initialObject = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I1 (InitialObject c1))
  (I1 (InitialObject c1))
-> (:>>:) c1 c2 (I1 (InitialObject c1)) (I1 (InitialObject c1))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c1 (InitialObject c1) (InitialObject c1)
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I1 (InitialObject c1))
     (I1 (InitialObject c1))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A c1 (InitialObject c1) (InitialObject c1)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)

  initialize :: Obj (c1 :>>: c2) a -> (:>>:) c1 c2 (InitialObject (c1 :>>: c2)) a
initialize (DC (I1A c a1 b1
a)) = Cograph
  (Const (Op c1 :**: c2) (->) ()) (I1 (InitialObject c1)) (I1 a1)
-> (:>>:) c1 c2 (I1 (InitialObject c1)) (I1 a1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c (InitialObject c1) a1
-> Cograph
     (Const (Op c1 :**: c2) (->) ()) (I1 (InitialObject c1)) (I1 a1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (Obj c a1 -> c (InitialObject c) a1
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj c a1
c a1 b1
a))
  initialize (DC (I2A d a2 b2
a)) = Cograph
  (Const (Op c1 :**: c2) (->) ()) (I1 (InitialObject c1)) (I2 a2)
-> (:>>:) c1 c2 (I1 (InitialObject c1)) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c1 (InitialObject c1) (InitialObject c1)
-> Obj d a2
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (InitialObject c1, a2))
-> Cograph
     (Const (Op c1 :**: c2) (->) ()) (I1 (InitialObject c1)) (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 c1 (InitialObject c1) (InitialObject c1)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject Obj d a2
d a2 b2
a (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())


class Category k => HasBinaryProducts k where
  type BinaryProduct k (x :: Kind k) (y :: Kind k) :: Kind k

  proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) x
  proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) y

  (&&&) :: k a x -> k a y -> k a (BinaryProduct k x y)

  (***) :: k a1 b1 -> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
  k a1 b1
l *** k a2 b2
r = (k a1 b1
l k a1 b1
-> k (BinaryProduct k a1 a2) a1 -> k (BinaryProduct k a1 a2) b1
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k a1 -> Obj k a2 -> k (BinaryProduct k a1 a2) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 (k a1 b1 -> Obj k a1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a1 b1
l) (k a2 b2 -> Obj k a2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a2 b2
r)) k (BinaryProduct k a1 a2) b1
-> k (BinaryProduct k a1 a2) b2
-> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& (k a2 b2
r k a2 b2
-> k (BinaryProduct k a1 a2) a2 -> k (BinaryProduct k a1 a2) b2
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k a1 -> Obj k a2 -> k (BinaryProduct k a1 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 (k a1 b1 -> Obj k a1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a1 b1
l) (k a2 b2 -> Obj k a2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a2 b2
r))


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

-- | If `k` has binary products, we can take the limit of 2 joined diagrams.
instance (HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (i :++: j) k where

  limit :: Obj (Nat (i :++: j) k) f
-> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
limit = Obj (Nat (i :++: j) k) f
-> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
forall f.
Obj (Nat (i :++: j) k) f
-> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
limit'
    where
      limit' :: forall f. Obj (Nat (i :++: j) k) f -> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
      limit' :: Obj (Nat (i :++: j) k) f
-> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
limit' l :: Obj (Nat (i :++: j) k) f
l@Nat{} = Const
  (i :++: j)
  k
  (BinaryProduct
     k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
-> f
-> (forall z.
    Obj (i :++: j) z
    -> Component
         (Const
            (i :++: j)
            k
            (BinaryProduct
               k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j))))
         f
         z)
-> Nat
     (i :++: j)
     k
     (Const
        (i :++: j)
        k
        (BinaryProduct
           k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j))))
     f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj
  k
  (BinaryProduct
     k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
-> Const
     (i :++: j)
     k
     (BinaryProduct
        k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (Obj k (LimitFam i k (f :.: Inj1 i j))
x Obj k (LimitFam i k (f :.: Inj1 i j))
-> k (LimitFam j k (f :.: Inj2 i j))
     (LimitFam j k (f :.: Inj2 i j))
-> Obj
     k
     (BinaryProduct
        k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** k (LimitFam j k (f :.: Inj2 i j)) (LimitFam j k (f :.: Inj2 i j))
y)) (Obj (Nat (i :++: j) k) f -> f
forall (c :: * -> * -> *) (d :: * -> * -> *) f g. Nat c d f g -> f
srcF Obj (Nat (i :++: j) k) f
l) forall z.
Obj (i :++: j) z
-> Component (ConstF f (LimitFam (i :++: j) k f)) f z
forall z.
Obj (i :++: j) z
-> Component
     (Const
        (i :++: j)
        k
        (BinaryProduct
           k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j))))
     f
     z
h
        where
          x :: Obj k (LimitFam i k (f :.: Inj1 i j))
x = Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
-> Obj k (LimitFam i k (f :.: Inj1 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
coneVertex Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
lim1
          y :: k (LimitFam j k (f :.: Inj2 i j)) (LimitFam j k (f :.: Inj2 i j))
y = Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
-> k (LimitFam j k (f :.: Inj2 i j))
     (LimitFam j k (f :.: Inj2 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
coneVertex Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
lim2
          lim1 :: Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
lim1 = Obj (Nat i k) (f :.: Inj1 i j)
-> Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit (Obj (Nat (i :++: j) k) f
l Obj (Nat (i :++: j) k) f
-> Nat i (i :++: j) (Inj1 i j) (Inj1 i j)
-> Obj (Nat i k) (f :.: Inj1 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj1 i j
-> Nat (Dom (Inj1 i j)) (Cod (Inj1 i j)) (Inj1 i j) (Inj1 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj1 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1)
          lim2 :: Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
lim2 = Obj (Nat j k) (f :.: Inj2 i j)
-> Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit (Obj (Nat (i :++: j) k) f
l Obj (Nat (i :++: j) k) f
-> Nat j (i :++: j) (Inj2 i j) (Inj2 i j)
-> Obj (Nat j k) (f :.: Inj2 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj2 i j
-> Nat (Dom (Inj2 i j)) (Cod (Inj2 i j)) (Inj2 i j) (Inj2 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj2 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2)
          h :: Obj (i :++: j) z -> Component (ConstF f (LimitFam (i :++: j) k f)) f z
          h :: Obj (i :++: j) z
-> Component (ConstF f (LimitFam (i :++: j) k f)) f z
h (I1 i a1 b1
n) = Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
lim1 Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
-> i a1 b1
-> k (Const i k (LimitFam i k (f :.: Inj1 i j)) :% a1)
     ((f :.: Inj1 i j) :% b1)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! i a1 b1
n k (LimitFam i k (f :.: Inj1 i j)) (f :% I1 b1)
-> k (BinaryProduct
        k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
     (LimitFam i k (f :.: Inj1 i j))
-> k (BinaryProduct
        k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
     (f :% I1 b1)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k (LimitFam i k (f :.: Inj1 i j))
-> k (LimitFam j k (f :.: Inj2 i j))
     (LimitFam j k (f :.: Inj2 i j))
-> k (BinaryProduct
        k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
     (LimitFam i k (f :.: Inj1 i j))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj k (LimitFam i k (f :.: Inj1 i j))
x k (LimitFam j k (f :.: Inj2 i j)) (LimitFam j k (f :.: Inj2 i j))
y
          h (I2 j a2 b2
n) = Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
lim2 Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
-> j a2 b2
-> k (Const j k (LimitFam j k (f :.: Inj2 i j)) :% a2)
     ((f :.: Inj2 i j) :% b2)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! j a2 b2
n k (LimitFam j k (f :.: Inj2 i j)) (f :% I2 b2)
-> k (BinaryProduct
        k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
     (LimitFam j k (f :.: Inj2 i j))
-> k (BinaryProduct
        k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
     (f :% I2 b2)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k (LimitFam i k (f :.: Inj1 i j))
-> k (LimitFam j k (f :.: Inj2 i j))
     (LimitFam j k (f :.: Inj2 i j))
-> k (BinaryProduct
        k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
     (LimitFam j k (f :.: Inj2 i j))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj k (LimitFam i k (f :.: Inj1 i j))
x k (LimitFam j k (f :.: Inj2 i j)) (LimitFam j k (f :.: Inj2 i j))
y

  limitFactorizer :: Cone (i :++: j) k f n -> k n (LimitFam (i :++: j) k f)
limitFactorizer Cone (i :++: j) k f n
c =
    Cone i k (f :.: Inj1 i j) n -> k n (LimitFam i k (f :.: Inj1 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (Nat i k (Const (i :++: j) k n :.: Inj1 i j) (f :.: Inj1 i j)
-> Cone i k (f :.: Inj1 i j) n
forall (j :: * -> * -> *) (d :: * -> * -> *) (k :: * -> * -> *) x f
       g.
Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g
constPostcompIn (Cone (i :++: j) k f n
c Cone (i :++: j) k f n
-> Nat i (i :++: j) (Inj1 i j) (Inj1 i j)
-> Nat i k (Const (i :++: j) k n :.: Inj1 i j) (f :.: Inj1 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj1 i j
-> Nat (Dom (Inj1 i j)) (Cod (Inj1 i j)) (Inj1 i j) (Inj1 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj1 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1))
    k n (LimitFam i k (f :.: Inj1 i j))
-> k n (LimitFam j k (f :.: Inj2 i j))
-> k n
     (BinaryProduct
        k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&&
    Cone j k (f :.: Inj2 i j) n -> k n (LimitFam j k (f :.: Inj2 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (Nat j k (Const (i :++: j) k n :.: Inj2 i j) (f :.: Inj2 i j)
-> Cone j k (f :.: Inj2 i j) n
forall (j :: * -> * -> *) (d :: * -> * -> *) (k :: * -> * -> *) x f
       g.
Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g
constPostcompIn (Cone (i :++: j) k f n
c Cone (i :++: j) k f n
-> Nat j (i :++: j) (Inj2 i j) (Inj2 i j)
-> Nat j k (Const (i :++: j) k n :.: Inj2 i j) (f :.: Inj2 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj2 i j
-> Nat (Dom (Inj2 i j)) (Cod (Inj2 i j)) (Inj2 i j) (Inj2 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj2 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2))


-- | The tuple is the binary product in @Hask@.
instance HasBinaryProducts (->) where
  type BinaryProduct (->) x y = (x, y)

  proj1 :: Obj (->) x -> Obj (->) y -> BinaryProduct (->) x y -> x
proj1 Obj (->) x
_ Obj (->) y
_ = \(x, _) -> x
x
  proj2 :: Obj (->) x -> Obj (->) y -> BinaryProduct (->) x y -> y
proj2 Obj (->) x
_ Obj (->) y
_ = \(_, y) -> y
y

  a -> x
f &&& :: (a -> x) -> (a -> y) -> a -> BinaryProduct (->) x y
&&& a -> y
g = \a
x -> (a -> x
f a
x, a -> y
g a
x)
  a1 -> b1
f *** :: (a1 -> b1)
-> (a2 -> b2)
-> BinaryProduct (->) a1 a2
-> BinaryProduct (->) b1 b2
*** a2 -> b2
g = \(x, y) -> (a1 -> b1
f a1
x, a2 -> b2
g a2
y)

-- | The product of categories ':**:' is the binary product in 'Cat'.
instance HasBinaryProducts Cat where
  type BinaryProduct Cat c1 c2 = c1 :**: c2

  proj1 :: Obj Cat x -> Obj Cat y -> Cat (BinaryProduct Cat x y) x
proj1 (CatA ftag
_) (CatA ftag
_) = Proj1 x y -> Cat (Dom (Proj1 x y)) (Cod (Proj1 x y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Proj1 x y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Proj1 c1 c2
Proj1
  proj2 :: Obj Cat x -> Obj Cat y -> Cat (BinaryProduct Cat x y) y
proj2 (CatA ftag
_) (CatA ftag
_) = Proj2 x y -> Cat (Dom (Proj2 x y)) (Cod (Proj2 x y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Proj2 x y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Proj2 c1 c2
Proj2

  CatA ftag
f1 &&& :: Cat a x -> Cat a y -> Cat a (BinaryProduct Cat x y)
&&& CatA ftag
f2 = ((ftag :***: ftag) :.: DiagProd a)
-> Cat
     (Dom ((ftag :***: ftag) :.: DiagProd a))
     (Cod ((ftag :***: ftag) :.: DiagProd a))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA ((ftag
f1 ftag -> ftag -> ftag :***: ftag
forall f1 f2. (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2
:***: ftag
f2) (ftag :***: ftag) -> DiagProd a -> (ftag :***: ftag) :.: DiagProd a
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: DiagProd a
forall (k :: * -> * -> *). DiagProd k
DiagProd)
  CatA ftag
f1 *** :: Cat a1 b1
-> Cat a2 b2
-> Cat (BinaryProduct Cat a1 a2) (BinaryProduct Cat b1 b2)
*** CatA ftag
f2 = (ftag :***: ftag)
-> Cat (Dom (ftag :***: ftag)) (Cod (ftag :***: ftag))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA (ftag
f1 ftag -> ftag -> ftag :***: ftag
forall f1 f2. (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2
:***: ftag
f2)

-- | In the category of one object that object is its own product.
instance HasBinaryProducts Unit where
  type BinaryProduct Unit () () = ()

  proj1 :: Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) x
proj1 Obj Unit x
Unit Obj Unit y
Unit = Obj Unit ()
Unit (BinaryProduct Unit x y) x
Unit
  proj2 :: Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) y
proj2 Obj Unit x
Unit Obj Unit y
Unit = Obj Unit ()
Unit (BinaryProduct Unit x y) y
Unit

  Unit a x
Unit &&& :: Unit a x -> Unit a y -> Unit a (BinaryProduct Unit x y)
&&& Unit a y
Unit = Unit a (BinaryProduct Unit x y)
Obj Unit ()
Unit
  Unit a1 b1
Unit *** :: Unit a1 b1
-> Unit a2 b2
-> Unit (BinaryProduct Unit a1 a2) (BinaryProduct Unit b1 b2)
*** Unit a2 b2
Unit = Obj Unit ()
Unit (BinaryProduct Unit a1 a2) (BinaryProduct Unit b1 b2)
Unit

-- | The binary product of the product of 2 categories is the product of their binary products.
instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where
  type BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)

  proj1 :: Obj (c1 :**: c2) x
-> Obj (c1 :**: c2) y
-> (:**:) c1 c2 (BinaryProduct (c1 :**: c2) x y) x
proj1 (c1 a1 b1
x1 :**: c2 a2 b2
x2) (c1 a1 b1
y1 :**: c2 a2 b2
y2) = Obj c1 a1 -> Obj c1 a1 -> c1 (BinaryProduct c1 a1 a1) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj c1 a1
c1 a1 b1
x1 Obj c1 a1
c1 a1 b1
y1 c1 (BinaryProduct c1 b1 b1) a1
-> c2 (BinaryProduct c2 b2 b2) a2
-> (:**:)
     c1 c2 (BinaryProduct c1 b1 b1, BinaryProduct c2 b2 b2) (a1, a2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> Obj c2 a2 -> c2 (BinaryProduct c2 a2 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj c2 a2
c2 a2 b2
x2 Obj c2 a2
c2 a2 b2
y2
  proj2 :: Obj (c1 :**: c2) x
-> Obj (c1 :**: c2) y
-> (:**:) c1 c2 (BinaryProduct (c1 :**: c2) x y) y
proj2 (c1 a1 b1
x1 :**: c2 a2 b2
x2) (c1 a1 b1
y1 :**: c2 a2 b2
y2) = Obj c1 a1 -> Obj c1 a1 -> c1 (BinaryProduct c1 a1 a1) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj c1 a1
c1 a1 b1
x1 Obj c1 a1
c1 a1 b1
y1 c1 (BinaryProduct c1 b1 b1) a1
-> c2 (BinaryProduct c2 b2 b2) a2
-> (:**:)
     c1 c2 (BinaryProduct c1 b1 b1, BinaryProduct c2 b2 b2) (a1, a2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> Obj c2 a2 -> c2 (BinaryProduct c2 a2 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj c2 a2
c2 a2 b2
x2 Obj c2 a2
c2 a2 b2
y2

  (c1 a1 b1
f1 :**: c2 a2 b2
f2) &&& :: (:**:) c1 c2 a x
-> (:**:) c1 c2 a y
-> (:**:) c1 c2 a (BinaryProduct (c1 :**: c2) x y)
&&& (c1 a1 b1
g1 :**: c2 a2 b2
g2) = (c1 a1 b1
f1 c1 a1 b1 -> c1 a1 b1 -> c1 a1 (BinaryProduct c1 b1 b1)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& c1 a1 b1
c1 a1 b1
g1) c1 a1 (BinaryProduct c1 b1 b1)
-> c2 a2 (BinaryProduct c2 b2 b2)
-> (:**:)
     c1 c2 (a1, a2) (BinaryProduct c1 b1 b1, BinaryProduct c2 b2 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (c2 a2 b2
f2 c2 a2 b2 -> c2 a2 b2 -> c2 a2 (BinaryProduct c2 b2 b2)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& c2 a2 b2
c2 a2 b2
g2)
  (c1 a1 b1
f1 :**: c2 a2 b2
f2) *** :: (:**:) c1 c2 a1 b1
-> (:**:) c1 c2 a2 b2
-> (:**:)
     c1
     c2
     (BinaryProduct (c1 :**: c2) a1 a2)
     (BinaryProduct (c1 :**: c2) b1 b2)
*** (c1 a1 b1
g1 :**: c2 a2 b2
g2) = (c1 a1 b1
f1 c1 a1 b1
-> c1 a1 b1 -> c1 (BinaryProduct c1 a1 a1) (BinaryProduct c1 b1 b1)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** c1 a1 b1
g1) c1 (BinaryProduct c1 a1 a1) (BinaryProduct c1 b1 b1)
-> c2 (BinaryProduct c2 a2 a2) (BinaryProduct c2 b2 b2)
-> (:**:)
     c1
     c2
     (BinaryProduct c1 a1 a1, BinaryProduct c2 a2 a2)
     (BinaryProduct c1 b1 b1, BinaryProduct c2 b2 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (c2 a2 b2
f2 c2 a2 b2
-> c2 a2 b2 -> c2 (BinaryProduct c2 a2 a2) (BinaryProduct c2 b2 b2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** c2 a2 b2
g2)

instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :>>: c2) where
  type BinaryProduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryProduct c1 a b)
  type BinaryProduct (c1 :>>: c2) (I1 a) (I2 b) = I1 a
  type BinaryProduct (c1 :>>: c2) (I2 a) (I1 b) = I1 b
  type BinaryProduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b)

  proj1 :: Obj (c1 :>>: c2) x
-> Obj (c1 :>>: c2) y
-> (:>>:) c1 c2 (BinaryProduct (c1 :>>: c2) x y) x
proj1 (DC (I1A c a1 b1
a)) (DC (I1A c a1 b1
b)) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I1 (BinaryProduct c1 b1 b1))
  (I1 a1)
-> (:>>:) c1 c2 (I1 (BinaryProduct c1 b1 b1)) (I1 a1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c (BinaryProduct c1 b1 b1) a1
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I1 (BinaryProduct c1 b1 b1))
     (I1 a1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (Obj c a1 -> Obj c a1 -> c (BinaryProduct c a1 a1) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj c a1
c a1 b1
a Obj c a1
c a1 b1
b))
  proj1 (DC (I1A c a1 b1
a)) (DC (I2A d a2 b2
_)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
-> (:>>:) c1 c2 (I1 a1) (I1 b1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 b1 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A c a1 b1
a)
  proj1 (DC (I2A d a2 b2
a)) (DC (I1A c a1 b1
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
-> (:>>:) c1 c2 (I1 a1) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a1
-> Obj d a2
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a1, a2))
-> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a1
c a1 b1
b Obj d a2
d a2 b2
a (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
  proj1 (DC (I2A d a2 b2
a)) (DC (I2A d a2 b2
b)) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I2 (BinaryProduct c2 b2 b2))
  (I2 a2)
-> (:>>:) c1 c2 (I2 (BinaryProduct c2 b2 b2)) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d (BinaryProduct c2 b2 b2) a2
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I2 (BinaryProduct c2 b2 b2))
     (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (Obj d a2 -> Obj d a2 -> d (BinaryProduct d a2 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj d a2
d a2 b2
a Obj d a2
d a2 b2
b))

  proj2 :: Obj (c1 :>>: c2) x
-> Obj (c1 :>>: c2) y
-> (:>>:) c1 c2 (BinaryProduct (c1 :>>: c2) x y) y
proj2 (DC (I1A c a1 b1
a)) (DC (I1A c a1 b1
b)) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I1 (BinaryProduct c1 b1 b1))
  (I1 a1)
-> (:>>:) c1 c2 (I1 (BinaryProduct c1 b1 b1)) (I1 a1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c (BinaryProduct c1 b1 b1) a1
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I1 (BinaryProduct c1 b1 b1))
     (I1 a1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (Obj c a1 -> Obj c a1 -> c (BinaryProduct c a1 a1) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj c a1
c a1 b1
a Obj c a1
c a1 b1
b))
  proj2 (DC (I1A c a1 b1
a)) (DC (I2A d a2 b2
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
-> (:>>:) c1 c2 (I1 a1) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a1
-> Obj d a2
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a1, a2))
-> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a1
c a1 b1
a Obj d a2
d a2 b2
b (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
  proj2 (DC (I2A d a2 b2
_)) (DC (I1A c a1 b1
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
-> (:>>:) c1 c2 (I1 a1) (I1 b1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 b1 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A c a1 b1
b)
  proj2 (DC (I2A d a2 b2
a)) (DC (I2A d a2 b2
b)) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I2 (BinaryProduct c2 b2 b2))
  (I2 a2)
-> (:>>:) c1 c2 (I2 (BinaryProduct c2 b2 b2)) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d (BinaryProduct c2 b2 b2) a2
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I2 (BinaryProduct c2 b2 b2))
     (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (Obj d a2 -> Obj d a2 -> d (BinaryProduct d a2 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj d a2
d a2 b2
a Obj d a2
d a2 b2
b))

  DC (I1A c a1 b1
a) &&& :: (:>>:) c1 c2 a x
-> (:>>:) c1 c2 a y
-> (:>>:) c1 c2 a (BinaryProduct (c1 :>>: c2) x y)
&&& DC (I1A c a1 b1
b) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I1 a1)
  (I1 (BinaryProduct c1 b1 b1))
-> (:>>:) c1 c2 (I1 a1) (I1 (BinaryProduct c1 b1 b1))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 (BinaryProduct c1 b1 b1)
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I1 a1)
     (I1 (BinaryProduct c1 b1 b1))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (c a1 b1
a c a1 b1 -> c a1 b1 -> c a1 (BinaryProduct c b1 b1)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& c a1 b1
c a1 b1
b))
  DC (I1A c a1 b1
a) &&& DC (I12 Obj c a
_ Obj d b
_ Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
-> (:>>:) c1 c2 (I1 a1) (I1 b1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 b1 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A c a1 b1
a)
  DC (I12 Obj c a
_ Obj d b
_ Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) &&& DC (I1A c a1 b1
b) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
-> (:>>:) c1 c2 (I1 a1) (I1 b1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 b1 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A c a1 b1
b)
  DC (I2A d a2 b2
a) &&& DC (I2A d a2 b2
b) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I2 a2)
  (I2 (BinaryProduct c2 b2 b2))
-> (:>>:) c1 c2 (I2 a2) (I2 (BinaryProduct c2 b2 b2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 (BinaryProduct c2 b2 b2)
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I2 a2)
     (I2 (BinaryProduct c2 b2 b2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (d a2 b2
a d a2 b2 -> d a2 b2 -> d a2 (BinaryProduct d b2 b2)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& d a2 b2
d a2 b2
b))
  DC (I12 Obj c a
a Obj d b
b1 Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) &&& DC (I12 Obj c a
_ Obj d b
b2 Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) = Cograph
  (Const (Op c1 :**: c2) (->) ()) (I1 a) (I2 (BinaryProduct c2 b b))
-> (:>>:) c1 c2 (I1 a) (I2 (BinaryProduct c2 b b))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a
-> Obj d (BinaryProduct c2 b b)
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a, BinaryProduct c2 b b))
-> Cograph
     (Const (Op c1 :**: c2) (->) ()) (I1 a) (I2 (BinaryProduct c2 b b))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a
a (Obj d b
b1 Obj d b -> d b b -> d (BinaryProduct d b b) (BinaryProduct d b b)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** d b b
Obj d b
b2) (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())


data ProductFunctor (k :: * -> * -> *) = ProductFunctor
-- | Binary product as a bifunctor.
instance HasBinaryProducts k => Functor (ProductFunctor k) where
  type Dom (ProductFunctor k) = k :**: k
  type Cod (ProductFunctor k) = k
  type ProductFunctor k :% (a, b) = BinaryProduct k a b

  ProductFunctor k
ProductFunctor % :: ProductFunctor k
-> Dom (ProductFunctor k) a b
-> Cod
     (ProductFunctor k) (ProductFunctor k :% a) (ProductFunctor k :% b)
% (a1 :**: a2) = k a1 b1
a1 k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** k a2 b2
a2

-- | A specialisation of the limit adjunction to products.
prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
prodAdj :: Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
prodAdj = DiagProd k
-> ProductFunctor k
-> (forall a.
    Obj k a -> Component (Id k) (ProductFunctor k :.: DiagProd k) a)
-> (forall a.
    Obj (k :**: k) a
    -> Component (DiagProd k :.: ProductFunctor k) (Id (k :**: k)) a)
-> Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionUnits DiagProd k
forall (k :: * -> * -> *). DiagProd k
DiagProd ProductFunctor k
forall (k :: * -> * -> *). ProductFunctor k
ProductFunctor (\Obj k a
x -> Obj k a
x Obj k a -> Obj k a -> k a (BinaryProduct k a a)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& Obj k a
x) (\(l :**: r) -> Obj k a1 -> Obj k a2 -> k (BinaryProduct k a1 a2) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj k a1
k a1 b1
l Obj k a2
k a2 b2
r k (BinaryProduct k b1 b2) a1
-> k (BinaryProduct k b1 b2) a2
-> (:**:)
     k k (BinaryProduct k b1 b2, BinaryProduct k b1 b2) (a1, a2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj k a1 -> Obj k a2 -> k (BinaryProduct k a1 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj k a1
k a1 b1
l Obj k a2
k a2 b2
r)

data p :*: q where
  (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q
-- | The product of two functors, passing the same object to both functors and taking the product of the results.
instance (Category (Dom p), Category (Cod p)) => Functor (p :*: q) where
  type Dom (p :*: q) = Dom p
  type Cod (p :*: q) = Cod p
  type (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a)

  (p
p :*: q
q) % :: (p :*: q)
-> Dom (p :*: q) a b
-> Cod (p :*: q) ((p :*: q) :% a) ((p :*: q) :% b)
% Dom (p :*: q) a b
f = (p
p p -> Dom p a b -> Cod p (p :% a) (p :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom p a b
Dom (p :*: q) a b
f) Cod p (p :% a) (p :% b)
-> Cod p (q :% a) (q :% b)
-> Cod
     p
     (BinaryProduct (Cod p) (p :% a) (q :% a))
     (BinaryProduct (Cod p) (p :% b) (q :% b))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** (q
q q -> Dom q a b -> Cod q (q :% a) (q :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom q a b
Dom (p :*: q) a b
f)

-- | The functor product ':*:' is the binary product in functor categories.
instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where
  type BinaryProduct (Nat c d) x y = x :*: y

  proj1 :: Obj (Nat c d) x
-> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) x
proj1 (Nat x
f x
_ forall z. Obj c z -> Component x x z
_) (Nat y
g y
_ forall z. Obj c z -> Component y y z
_) = (x :*: y)
-> x
-> (forall z. Obj c z -> Component (x :*: y) x z)
-> Nat c d (x :*: y) x
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (x
f x -> y -> x :*: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryProducts k) =>
p -> q -> p :*: q
:*: y
g) x
f (\Obj c z
z -> Obj d (x :% z)
-> Obj d (y :% z) -> d (BinaryProduct d (x :% z) (y :% z)) (x :% z)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 (x
f x -> Dom x z z -> Cod x (x :% z) (x :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom x z z
z) (y
g y -> Dom y z z -> Cod y (y :% z) (y :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom y z z
z))
  proj2 :: Obj (Nat c d) x
-> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) y
proj2 (Nat x
f x
_ forall z. Obj c z -> Component x x z
_) (Nat y
g y
_ forall z. Obj c z -> Component y y z
_) = (x :*: y)
-> y
-> (forall z. Obj c z -> Component (x :*: y) y z)
-> Nat c d (x :*: y) y
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (x
f x -> y -> x :*: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryProducts k) =>
p -> q -> p :*: q
:*: y
g) y
g (\Obj c z
z -> Obj d (x :% z)
-> Obj d (y :% z) -> d (BinaryProduct d (x :% z) (y :% z)) (y :% z)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 (x
f x -> Dom x z z -> Cod x (x :% z) (x :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom x z z
z) (y
g y -> Dom y z z -> Cod y (y :% z) (y :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom y z z
z))

  Nat a
a x
f forall z. Obj c z -> Component a x z
af &&& :: Nat c d a x
-> Nat c d a y -> Nat c d a (BinaryProduct (Nat c d) x y)
&&& Nat a
_ y
g forall z. Obj c z -> Component a y z
ag = a
-> (x :*: y)
-> (forall z. Obj c z -> Component a (x :*: y) z)
-> Nat c d a (x :*: y)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat a
a (x
f x -> y -> x :*: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryProducts k) =>
p -> q -> p :*: q
:*: y
g) (\Obj c z
z -> Obj c z -> Component a x z
forall z. Obj c z -> Component a x z
af Obj c z
z d (a :% z) (x :% z)
-> d (a :% z) (y :% z)
-> d (a :% z) (BinaryProduct d (x :% z) (y :% z))
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& Obj c z -> Component a y z
forall z. Obj c z -> Component a y z
ag Obj c z
z)
  Nat a1
f1 b1
f2 forall z. Obj c z -> Component a1 b1 z
f *** :: Nat c d a1 b1
-> Nat c d a2 b2
-> Nat
     c d (BinaryProduct (Nat c d) a1 a2) (BinaryProduct (Nat c d) b1 b2)
*** Nat a2
g1 b2
g2 forall z. Obj c z -> Component a2 b2 z
g = (a1 :*: a2)
-> (b1 :*: b2)
-> (forall z. Obj c z -> Component (a1 :*: a2) (b1 :*: b2) z)
-> Nat c d (a1 :*: a2) (b1 :*: b2)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (a1
f1 a1 -> a2 -> a1 :*: a2
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryProducts k) =>
p -> q -> p :*: q
:*: a2
g1) (b1
f2 b1 -> b2 -> b1 :*: b2
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryProducts k) =>
p -> q -> p :*: q
:*: b2
g2) (\Obj c z
z -> Obj c z -> Component a1 b1 z
forall z. Obj c z -> Component a1 b1 z
f Obj c z
z d (a1 :% z) (b1 :% z)
-> d (a2 :% z) (b2 :% z)
-> d (BinaryProduct d (a1 :% z) (a2 :% z))
     (BinaryProduct d (b1 :% z) (b2 :% z))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj c z -> Component a2 b2 z
forall z. Obj c z -> Component a2 b2 z
g Obj c z
z)



class Category k => HasBinaryCoproducts k where
  type BinaryCoproduct k (x :: Kind k) (y :: Kind k) :: Kind k

  inj1 :: Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
  inj2 :: Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)

  (|||) :: k x a -> k y a -> k (BinaryCoproduct k x y) a

  (+++) :: k a1 b1 -> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
  k a1 b1
l +++ k a2 b2
r = (Obj k b1 -> Obj k b2 -> k b1 (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 (k a1 b1 -> Obj k b1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a1 b1
l) (k a2 b2 -> Obj k b2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a2 b2
r) k b1 (BinaryCoproduct k b1 b2)
-> k a1 b1 -> k a1 (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k a1 b1
l) k a1 (BinaryCoproduct k b1 b2)
-> k a2 (BinaryCoproduct k b1 b2)
-> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| (Obj k b1 -> Obj k b2 -> k b2 (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 (k a1 b1 -> Obj k b1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a1 b1
l) (k a2 b2 -> Obj k b2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a2 b2
r) k b2 (BinaryCoproduct k b1 b2)
-> k a2 b2 -> k a2 (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k a2 b2
r)


type instance ColimitFam (i :++: j) k f = BinaryCoproduct k
  (ColimitFam i k (f :.: Inj1 i j))
  (ColimitFam j k (f :.: Inj2 i j))

-- | If `k` has binary coproducts, we can take the colimit of 2 joined diagrams.
instance (HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (i :++: j) k where

  colimit :: Obj (Nat (i :++: j) k) f
-> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
colimit = Obj (Nat (i :++: j) k) f
-> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
forall f.
Obj (Nat (i :++: j) k) f
-> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
colimit'
    where
      colimit' :: forall f. Obj (Nat (i :++: j) k) f -> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
      colimit' :: Obj (Nat (i :++: j) k) f
-> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
colimit' l :: Obj (Nat (i :++: j) k) f
l@Nat{} = f
-> Const
     (i :++: j)
     k
     (BinaryCoproduct
        k
        (ColimitFam i k (f :.: Inj1 i j))
        (ColimitFam j k (f :.: Inj2 i j)))
-> (forall z.
    Obj (i :++: j) z
    -> Component
         f
         (Const
            (i :++: j)
            k
            (BinaryCoproduct
               k
               (ColimitFam i k (f :.: Inj1 i j))
               (ColimitFam j k (f :.: Inj2 i j))))
         z)
-> Nat
     (i :++: j)
     k
     f
     (Const
        (i :++: j)
        k
        (BinaryCoproduct
           k
           (ColimitFam i k (f :.: Inj1 i j))
           (ColimitFam j k (f :.: Inj2 i j))))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj (Nat (i :++: j) k) f -> f
forall (c :: * -> * -> *) (d :: * -> * -> *) f g. Nat c d f g -> f
srcF Obj (Nat (i :++: j) k) f
l) (Obj
  k
  (BinaryCoproduct
     k
     (ColimitFam i k (f :.: Inj1 i j))
     (ColimitFam j k (f :.: Inj2 i j)))
-> Const
     (i :++: j)
     k
     (BinaryCoproduct
        k
        (ColimitFam i k (f :.: Inj1 i j))
        (ColimitFam j k (f :.: Inj2 i j)))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (Obj k (ColimitFam i k (f :.: Inj1 i j))
x Obj k (ColimitFam i k (f :.: Inj1 i j))
-> k (ColimitFam j k (f :.: Inj2 i j))
     (ColimitFam j k (f :.: Inj2 i j))
-> Obj
     k
     (BinaryCoproduct
        k
        (ColimitFam i k (f :.: Inj1 i j))
        (ColimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ k (ColimitFam j k (f :.: Inj2 i j))
  (ColimitFam j k (f :.: Inj2 i j))
y)) forall z.
Obj (i :++: j) z
-> Component f (ConstF f (ColimitFam (i :++: j) k f)) z
forall z.
Obj (i :++: j) z
-> Component
     f
     (Const
        (i :++: j)
        k
        (BinaryCoproduct
           k
           (ColimitFam i k (f :.: Inj1 i j))
           (ColimitFam j k (f :.: Inj2 i j))))
     z
h
        where
          x :: Obj k (ColimitFam i k (f :.: Inj1 i j))
x = Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
-> Obj k (ColimitFam i k (f :.: Inj1 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
col1
          y :: k (ColimitFam j k (f :.: Inj2 i j))
  (ColimitFam j k (f :.: Inj2 i j))
y = Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
-> k (ColimitFam j k (f :.: Inj2 i j))
     (ColimitFam j k (f :.: Inj2 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
col2
          col1 :: Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
col1 = Obj (Nat i k) (f :.: Inj1 i j)
-> Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit (Obj (Nat (i :++: j) k) f
l Obj (Nat (i :++: j) k) f
-> Nat i (i :++: j) (Inj1 i j) (Inj1 i j)
-> Obj (Nat i k) (f :.: Inj1 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj1 i j
-> Nat (Dom (Inj1 i j)) (Cod (Inj1 i j)) (Inj1 i j) (Inj1 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj1 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1)
          col2 :: Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
col2 = Obj (Nat j k) (f :.: Inj2 i j)
-> Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit (Obj (Nat (i :++: j) k) f
l Obj (Nat (i :++: j) k) f
-> Nat j (i :++: j) (Inj2 i j) (Inj2 i j)
-> Obj (Nat j k) (f :.: Inj2 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj2 i j
-> Nat (Dom (Inj2 i j)) (Cod (Inj2 i j)) (Inj2 i j) (Inj2 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj2 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2)
          h :: Obj (i :++: j) z -> Component f (ConstF f (ColimitFam (i :++: j) k f)) z
          h :: Obj (i :++: j) z
-> Component f (ConstF f (ColimitFam (i :++: j) k f)) z
h (I1 i a1 b1
n) = Obj k (ColimitFam i k (f :.: Inj1 i j))
-> k (ColimitFam j k (f :.: Inj2 i j))
     (ColimitFam j k (f :.: Inj2 i j))
-> k (ColimitFam i k (f :.: Inj1 i j))
     (BinaryCoproduct
        k
        (ColimitFam i k (f :.: Inj1 i j))
        (ColimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj k (ColimitFam i k (f :.: Inj1 i j))
x k (ColimitFam j k (f :.: Inj2 i j))
  (ColimitFam j k (f :.: Inj2 i j))
y k (ColimitFam i k (f :.: Inj1 i j))
  (BinaryCoproduct
     k
     (ColimitFam i k (f :.: Inj1 i j))
     (ColimitFam j k (f :.: Inj2 i j)))
-> k (f :% I1 b1) (ColimitFam i k (f :.: Inj1 i j))
-> k (f :% I1 b1)
     (BinaryCoproduct
        k
        (ColimitFam i k (f :.: Inj1 i j))
        (ColimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
col1 Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
-> i a1 b1
-> k ((f :.: Inj1 i j) :% a1)
     (Const i k (ColimitFam i k (f :.: Inj1 i j)) :% b1)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! i a1 b1
n
          h (I2 j a2 b2
n) = Obj k (ColimitFam i k (f :.: Inj1 i j))
-> k (ColimitFam j k (f :.: Inj2 i j))
     (ColimitFam j k (f :.: Inj2 i j))
-> k (ColimitFam j k (f :.: Inj2 i j))
     (BinaryCoproduct
        k
        (ColimitFam i k (f :.: Inj1 i j))
        (ColimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj k (ColimitFam i k (f :.: Inj1 i j))
x k (ColimitFam j k (f :.: Inj2 i j))
  (ColimitFam j k (f :.: Inj2 i j))
y k (ColimitFam j k (f :.: Inj2 i j))
  (BinaryCoproduct
     k
     (ColimitFam i k (f :.: Inj1 i j))
     (ColimitFam j k (f :.: Inj2 i j)))
-> k (f :% I2 b2) (ColimitFam j k (f :.: Inj2 i j))
-> k (f :% I2 b2)
     (BinaryCoproduct
        k
        (ColimitFam i k (f :.: Inj1 i j))
        (ColimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
col2 Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
-> j a2 b2
-> k ((f :.: Inj2 i j) :% a2)
     (Const j k (ColimitFam j k (f :.: Inj2 i j)) :% b2)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! j a2 b2
n

  colimitFactorizer :: Cocone (i :++: j) k f n -> k (ColimitFam (i :++: j) k f) n
colimitFactorizer Cocone (i :++: j) k f n
c =
    Cocone i k (f :.: Inj1 i j) n
-> k (ColimitFam i k (f :.: Inj1 i j)) n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (Nat i k (f :.: Inj1 i j) (Const (i :++: j) k n :.: Inj1 i j)
-> Cocone i k (f :.: Inj1 i j) n
forall (j :: * -> * -> *) (d :: * -> * -> *) f (k :: * -> * -> *) x
       g.
Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x)
constPostcompOut (Cocone (i :++: j) k f n
c Cocone (i :++: j) k f n
-> Nat i (i :++: j) (Inj1 i j) (Inj1 i j)
-> Nat i k (f :.: Inj1 i j) (Const (i :++: j) k n :.: Inj1 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj1 i j
-> Nat (Dom (Inj1 i j)) (Cod (Inj1 i j)) (Inj1 i j) (Inj1 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj1 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1))
    k (ColimitFam i k (f :.: Inj1 i j)) n
-> k (ColimitFam j k (f :.: Inj2 i j)) n
-> k (BinaryCoproduct
        k
        (ColimitFam i k (f :.: Inj1 i j))
        (ColimitFam j k (f :.: Inj2 i j)))
     n
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
|||
    Cocone j k (f :.: Inj2 i j) n
-> k (ColimitFam j k (f :.: Inj2 i j)) n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (Nat j k (f :.: Inj2 i j) (Const (i :++: j) k n :.: Inj2 i j)
-> Cocone j k (f :.: Inj2 i j) n
forall (j :: * -> * -> *) (d :: * -> * -> *) f (k :: * -> * -> *) x
       g.
Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x)
constPostcompOut (Cocone (i :++: j) k f n
c Cocone (i :++: j) k f n
-> Nat j (i :++: j) (Inj2 i j) (Inj2 i j)
-> Nat j k (f :.: Inj2 i j) (Const (i :++: j) k n :.: Inj2 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj2 i j
-> Nat (Dom (Inj2 i j)) (Cod (Inj2 i j)) (Inj2 i j) (Inj2 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj2 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2))


-- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'.
instance HasBinaryCoproducts Cat where
  type BinaryCoproduct Cat c1 c2 = c1 :++: c2

  inj1 :: Obj Cat x -> Obj Cat y -> Cat x (BinaryCoproduct Cat x y)
inj1 (CatA ftag
_) (CatA ftag
_) = Inj1 x y -> Cat (Dom (Inj1 x y)) (Cod (Inj1 x y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Inj1 x y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1
  inj2 :: Obj Cat x -> Obj Cat y -> Cat y (BinaryCoproduct Cat x y)
inj2 (CatA ftag
_) (CatA ftag
_) = Inj2 x y -> Cat (Dom (Inj2 x y)) (Cod (Inj2 x y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Inj2 x y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2

  CatA ftag
f1 ||| :: Cat x a -> Cat y a -> Cat (BinaryCoproduct Cat x y) a
||| CatA ftag
f2 = (CodiagCoprod a :.: (ftag :+++: ftag))
-> Cat
     (Dom (CodiagCoprod a :.: (ftag :+++: ftag)))
     (Cod (CodiagCoprod a :.: (ftag :+++: ftag)))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA (CodiagCoprod a
forall (k :: * -> * -> *). CodiagCoprod k
CodiagCoprod CodiagCoprod a
-> (ftag :+++: ftag) -> CodiagCoprod a :.: (ftag :+++: ftag)
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: (ftag
f1 ftag -> ftag -> ftag :+++: ftag
forall f1 f2. f1 -> f2 -> f1 :+++: f2
:+++: ftag
f2))
  CatA ftag
f1 +++ :: Cat a1 b1
-> Cat a2 b2
-> Cat (BinaryCoproduct Cat a1 a2) (BinaryCoproduct Cat b1 b2)
+++ CatA ftag
f2 = (ftag :+++: ftag)
-> Cat (Dom (ftag :+++: ftag)) (Cod (ftag :+++: ftag))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA (ftag
f1 ftag -> ftag -> ftag :+++: ftag
forall f1 f2. f1 -> f2 -> f1 :+++: f2
:+++: ftag
f2)

-- | In the category of one object that object is its own coproduct.
instance HasBinaryCoproducts Unit where
  type BinaryCoproduct Unit () () = ()

  inj1 :: Obj Unit x -> Obj Unit y -> Unit x (BinaryCoproduct Unit x y)
inj1 Obj Unit x
Unit Obj Unit y
Unit = Unit x (BinaryCoproduct Unit x y)
Obj Unit ()
Unit
  inj2 :: Obj Unit x -> Obj Unit y -> Unit y (BinaryCoproduct Unit x y)
inj2 Obj Unit x
Unit Obj Unit y
Unit = Unit y (BinaryCoproduct Unit x y)
Obj Unit ()
Unit

  Unit x a
Unit ||| :: Unit x a -> Unit y a -> Unit (BinaryCoproduct Unit x y) a
||| Unit y a
Unit = Obj Unit ()
Unit (BinaryCoproduct Unit x y) a
Unit
  Unit a1 b1
Unit +++ :: Unit a1 b1
-> Unit a2 b2
-> Unit (BinaryCoproduct Unit a1 a2) (BinaryCoproduct Unit b1 b2)
+++ Unit a2 b2
Unit = Obj Unit ()
Unit (BinaryCoproduct Unit a1 a2) (BinaryCoproduct Unit b1 b2)
Unit

-- | The binary coproduct of the product of 2 categories is the product of their binary coproducts.
instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where
  type BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)

  inj1 :: Obj (c1 :**: c2) x
-> Obj (c1 :**: c2) y
-> (:**:) c1 c2 x (BinaryCoproduct (c1 :**: c2) x y)
inj1 (c1 a1 b1
x1 :**: c2 a2 b2
x2) (c1 a1 b1
y1 :**: c2 a2 b2
y2) = Obj c1 a1 -> Obj c1 a1 -> c1 a1 (BinaryCoproduct c1 a1 a1)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj c1 a1
c1 a1 b1
x1 Obj c1 a1
c1 a1 b1
y1 c1 a1 (BinaryCoproduct c1 b1 b1)
-> c2 a2 (BinaryCoproduct c2 b2 b2)
-> (:**:)
     c1 c2 (a1, a2) (BinaryCoproduct c1 b1 b1, BinaryCoproduct c2 b2 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> Obj c2 a2 -> c2 a2 (BinaryCoproduct c2 a2 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj c2 a2
c2 a2 b2
x2 Obj c2 a2
c2 a2 b2
y2
  inj2 :: Obj (c1 :**: c2) x
-> Obj (c1 :**: c2) y
-> (:**:) c1 c2 y (BinaryCoproduct (c1 :**: c2) x y)
inj2 (c1 a1 b1
x1 :**: c2 a2 b2
x2) (c1 a1 b1
y1 :**: c2 a2 b2
y2) = Obj c1 a1 -> Obj c1 a1 -> c1 a1 (BinaryCoproduct c1 a1 a1)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj c1 a1
c1 a1 b1
x1 Obj c1 a1
c1 a1 b1
y1 c1 a1 (BinaryCoproduct c1 b1 b1)
-> c2 a2 (BinaryCoproduct c2 b2 b2)
-> (:**:)
     c1 c2 (a1, a2) (BinaryCoproduct c1 b1 b1, BinaryCoproduct c2 b2 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> Obj c2 a2 -> c2 a2 (BinaryCoproduct c2 a2 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj c2 a2
c2 a2 b2
x2 Obj c2 a2
c2 a2 b2
y2

  (c1 a1 b1
f1 :**: c2 a2 b2
f2) ||| :: (:**:) c1 c2 x a
-> (:**:) c1 c2 y a
-> (:**:) c1 c2 (BinaryCoproduct (c1 :**: c2) x y) a
||| (c1 a1 b1
g1 :**: c2 a2 b2
g2) = (c1 a1 b1
f1 c1 a1 b1 -> c1 a1 b1 -> c1 (BinaryCoproduct c1 a1 a1) b1
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| c1 a1 b1
c1 a1 b1
g1) c1 (BinaryCoproduct c1 a1 a1) b1
-> c2 (BinaryCoproduct c2 a2 a2) b2
-> (:**:)
     c1 c2 (BinaryCoproduct c1 a1 a1, BinaryCoproduct c2 a2 a2) (b1, b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (c2 a2 b2
f2 c2 a2 b2 -> c2 a2 b2 -> c2 (BinaryCoproduct c2 a2 a2) b2
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| c2 a2 b2
c2 a2 b2
g2)
  (c1 a1 b1
f1 :**: c2 a2 b2
f2) +++ :: (:**:) c1 c2 a1 b1
-> (:**:) c1 c2 a2 b2
-> (:**:)
     c1
     c2
     (BinaryCoproduct (c1 :**: c2) a1 a2)
     (BinaryCoproduct (c1 :**: c2) b1 b2)
+++ (c1 a1 b1
g1 :**: c2 a2 b2
g2) = (c1 a1 b1
f1 c1 a1 b1
-> c1 a1 b1
-> c1 (BinaryCoproduct c1 a1 a1) (BinaryCoproduct c1 b1 b1)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ c1 a1 b1
g1) c1 (BinaryCoproduct c1 a1 a1) (BinaryCoproduct c1 b1 b1)
-> c2 (BinaryCoproduct c2 a2 a2) (BinaryCoproduct c2 b2 b2)
-> (:**:)
     c1
     c2
     (BinaryCoproduct c1 a1 a1, BinaryCoproduct c2 a2 a2)
     (BinaryCoproduct c1 b1 b1, BinaryCoproduct c2 b2 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (c2 a2 b2
f2 c2 a2 b2
-> c2 a2 b2
-> c2 (BinaryCoproduct c2 a2 a2) (BinaryCoproduct c2 b2 b2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ c2 a2 b2
g2)

instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :>>: c2) where
  type BinaryCoproduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryCoproduct c1 a b)
  type BinaryCoproduct (c1 :>>: c2) (I1 a) (I2 b) = I2 b
  type BinaryCoproduct (c1 :>>: c2) (I2 a) (I1 b) = I2 a
  type BinaryCoproduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryCoproduct c2 a b)

  inj1 :: Obj (c1 :>>: c2) x
-> Obj (c1 :>>: c2) y
-> (:>>:) c1 c2 x (BinaryCoproduct (c1 :>>: c2) x y)
inj1 (DC (I1A c a1 b1
a)) (DC (I1A c a1 b1
b)) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I1 a1)
  (I1 (BinaryCoproduct c1 b1 b1))
-> (:>>:) c1 c2 (I1 a1) (I1 (BinaryCoproduct c1 b1 b1))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 (BinaryCoproduct c1 b1 b1)
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I1 a1)
     (I1 (BinaryCoproduct c1 b1 b1))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (Obj c a1 -> Obj c a1 -> c a1 (BinaryCoproduct c a1 a1)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj c a1
c a1 b1
a Obj c a1
c a1 b1
b))
  inj1 (DC (I1A c a1 b1
a)) (DC (I2A d a2 b2
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
-> (:>>:) c1 c2 (I1 a1) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a1
-> Obj d a2
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a1, a2))
-> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a1
c a1 b1
a Obj d a2
d a2 b2
b (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
  inj1 (DC (I2A d a2 b2
a)) (DC (I1A c a1 b1
_)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
-> (:>>:) c1 c2 (I2 a2) (I2 b2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 b2 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A d a2 b2
a)
  inj1 (DC (I2A d a2 b2
a)) (DC (I2A d a2 b2
b)) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I2 a2)
  (I2 (BinaryCoproduct c2 b2 b2))
-> (:>>:) c1 c2 (I2 a2) (I2 (BinaryCoproduct c2 b2 b2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 (BinaryCoproduct c2 b2 b2)
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I2 a2)
     (I2 (BinaryCoproduct c2 b2 b2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (Obj d a2 -> Obj d a2 -> d a2 (BinaryCoproduct d a2 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj d a2
d a2 b2
a Obj d a2
d a2 b2
b))

  inj2 :: Obj (c1 :>>: c2) x
-> Obj (c1 :>>: c2) y
-> (:>>:) c1 c2 y (BinaryCoproduct (c1 :>>: c2) x y)
inj2 (DC (I1A c a1 b1
a)) (DC (I1A c a1 b1
b)) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I1 a1)
  (I1 (BinaryCoproduct c1 b1 b1))
-> (:>>:) c1 c2 (I1 a1) (I1 (BinaryCoproduct c1 b1 b1))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 (BinaryCoproduct c1 b1 b1)
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I1 a1)
     (I1 (BinaryCoproduct c1 b1 b1))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (Obj c a1 -> Obj c a1 -> c a1 (BinaryCoproduct c a1 a1)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj c a1
c a1 b1
a Obj c a1
c a1 b1
b))
  inj2 (DC (I1A c a1 b1
_)) (DC (I2A d a2 b2
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
-> (:>>:) c1 c2 (I2 a2) (I2 b2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 b2 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A d a2 b2
b)
  inj2 (DC (I2A d a2 b2
a)) (DC (I1A c a1 b1
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
-> (:>>:) c1 c2 (I1 a1) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a1
-> Obj d a2
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a1, a2))
-> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a1
c a1 b1
b Obj d a2
d a2 b2
a (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
  inj2 (DC (I2A d a2 b2
a)) (DC (I2A d a2 b2
b)) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I2 a2)
  (I2 (BinaryCoproduct c2 b2 b2))
-> (:>>:) c1 c2 (I2 a2) (I2 (BinaryCoproduct c2 b2 b2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 (BinaryCoproduct c2 b2 b2)
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I2 a2)
     (I2 (BinaryCoproduct c2 b2 b2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (Obj d a2 -> Obj d a2 -> d a2 (BinaryCoproduct d a2 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj d a2
d a2 b2
a Obj d a2
d a2 b2
b))

  DC (I1A c a1 b1
a) ||| :: (:>>:) c1 c2 x a
-> (:>>:) c1 c2 y a
-> (:>>:) c1 c2 (BinaryCoproduct (c1 :>>: c2) x y) a
||| DC (I1A c a1 b1
b) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I1 (BinaryCoproduct c1 a1 a1))
  (I1 b1)
-> (:>>:) c1 c2 (I1 (BinaryCoproduct c1 a1 a1)) (I1 b1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c (BinaryCoproduct c1 a1 a1) b1
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I1 (BinaryCoproduct c1 a1 a1))
     (I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (c a1 b1
a c a1 b1 -> c a1 b1 -> c (BinaryCoproduct c a1 a1) b1
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| c a1 b1
c a1 b1
b))
  DC (I2A d a2 b2
a) ||| DC (I12 Obj c a
_ Obj d b
_ Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) = Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
-> (:>>:) c1 c2 (I2 a2) (I2 b2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 b2 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A d a2 b2
a)
  DC (I12 Obj c a
_ Obj d b
_ Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) ||| DC (I2A d a2 b2
b) = Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
-> (:>>:) c1 c2 (I2 a2) (I2 b2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 b2 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A d a2 b2
b)
  DC (I2A d a2 b2
a) ||| DC (I2A d a2 b2
b) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I2 (BinaryCoproduct c2 a2 a2))
  (I2 b2)
-> (:>>:) c1 c2 (I2 (BinaryCoproduct c2 a2 a2)) (I2 b2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d (BinaryCoproduct c2 a2 a2) b2
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I2 (BinaryCoproduct c2 a2 a2))
     (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (d a2 b2
a d a2 b2 -> d a2 b2 -> d (BinaryCoproduct d a2 a2) b2
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| d a2 b2
d a2 b2
b))
  DC (I12 Obj c a
a1 Obj d b
b Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) ||| DC (I12 Obj c a
a2 Obj d b
_ Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) = Cograph
  (Const (Op c1 :**: c2) (->) ())
  (I1 (BinaryCoproduct c1 a a))
  (I2 b)
-> (:>>:) c1 c2 (I1 (BinaryCoproduct c1 a a)) (I2 b)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c (BinaryCoproduct c1 a a)
-> Obj d b
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (BinaryCoproduct c1 a a, b))
-> Cograph
     (Const (Op c1 :**: c2) (->) ())
     (I1 (BinaryCoproduct c1 a a))
     (I2 b)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 (Obj c a
a1 Obj c a
-> c a a -> c (BinaryCoproduct c a a) (BinaryCoproduct c a a)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ c a a
Obj c a
a2) Obj d b
b (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())


data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor
-- | Binary coproduct as a bifunctor.
instance HasBinaryCoproducts k => Functor (CoproductFunctor k) where
  type Dom (CoproductFunctor k) = k :**: k
  type Cod (CoproductFunctor k) = k
  type CoproductFunctor k :% (a, b) = BinaryCoproduct k a b

  CoproductFunctor k
CoproductFunctor % :: CoproductFunctor k
-> Dom (CoproductFunctor k) a b
-> Cod
     (CoproductFunctor k)
     (CoproductFunctor k :% a)
     (CoproductFunctor k :% b)
% (a1 :**: a2) = k a1 b1
a1 k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ k a2 b2
a2

-- | A specialisation of the colimit adjunction to coproducts.
coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)
coprodAdj :: Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)
coprodAdj = CoproductFunctor k
-> DiagProd k
-> (forall a.
    Obj (k :**: k) a
    -> Component (Id (k :**: k)) (DiagProd k :.: CoproductFunctor k) a)
-> (forall a.
    Obj k a -> Component (CoproductFunctor k :.: DiagProd k) (Id k) a)
-> Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionUnits CoproductFunctor k
forall (k :: * -> * -> *). CoproductFunctor k
CoproductFunctor DiagProd k
forall (k :: * -> * -> *). DiagProd k
DiagProd (\(l :**: r) -> Obj k a1 -> Obj k a2 -> k a1 (BinaryCoproduct k a1 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj k a1
k a1 b1
l Obj k a2
k a2 b2
r k a1 (BinaryCoproduct k b1 b2)
-> k a2 (BinaryCoproduct k b1 b2)
-> (:**:)
     k k (a1, a2) (BinaryCoproduct k b1 b2, BinaryCoproduct k b1 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj k a1 -> Obj k a2 -> k a2 (BinaryCoproduct k a1 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj k a1
k a1 b1
l Obj k a2
k a2 b2
r) (\Obj k a
x -> Obj k a
x Obj k a -> Obj k a -> k (BinaryCoproduct k a a) a
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| Obj k a
x)

data p :+: q where
  (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q
-- | The coproduct of two functors, passing the same object to both functors and taking the coproduct of the results.
instance (Category (Dom p), Category (Cod p)) => Functor (p :+: q) where
  type Dom (p :+: q) = Dom p
  type Cod (p :+: q) = Cod p
  type (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a)

  (p
p :+: q
q) % :: (p :+: q)
-> Dom (p :+: q) a b
-> Cod (p :+: q) ((p :+: q) :% a) ((p :+: q) :% b)
% Dom (p :+: q) a b
f = (p
p p -> Dom p a b -> Cod p (p :% a) (p :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom p a b
Dom (p :+: q) a b
f) Cod p (p :% a) (p :% b)
-> Cod p (q :% a) (q :% b)
-> Cod
     p
     (BinaryCoproduct (Cod p) (p :% a) (q :% a))
     (BinaryCoproduct (Cod p) (p :% b) (q :% b))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ (q
q q -> Dom q a b -> Cod q (q :% a) (q :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom q a b
Dom (p :+: q) a b
f)

-- | The functor coproduct ':+:' is the binary coproduct in functor categories.
instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where
  type BinaryCoproduct (Nat c d) x y = x :+: y

  inj1 :: Obj (Nat c d) x
-> Obj (Nat c d) y -> Nat c d x (BinaryCoproduct (Nat c d) x y)
inj1 (Nat x
f x
_ forall z. Obj c z -> Component x x z
_) (Nat y
g y
_ forall z. Obj c z -> Component y y z
_) = x
-> (x :+: y)
-> (forall z. Obj c z -> Component x (x :+: y) z)
-> Nat c d x (x :+: y)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat x
f (x
f x -> y -> x :+: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryCoproducts k) =>
p -> q -> p :+: q
:+: y
g) (\Obj c z
z -> Obj d (x :% z)
-> Obj d (y :% z)
-> d (x :% z) (BinaryCoproduct d (x :% z) (y :% z))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 (x
f x -> Dom x z z -> Cod x (x :% z) (x :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom x z z
z) (y
g y -> Dom y z z -> Cod y (y :% z) (y :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom y z z
z))
  inj2 :: Obj (Nat c d) x
-> Obj (Nat c d) y -> Nat c d y (BinaryCoproduct (Nat c d) x y)
inj2 (Nat x
f x
_ forall z. Obj c z -> Component x x z
_) (Nat y
g y
_ forall z. Obj c z -> Component y y z
_) = y
-> (x :+: y)
-> (forall z. Obj c z -> Component y (x :+: y) z)
-> Nat c d y (x :+: y)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat y
g (x
f x -> y -> x :+: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryCoproducts k) =>
p -> q -> p :+: q
:+: y
g) (\Obj c z
z -> Obj d (x :% z)
-> Obj d (y :% z)
-> d (y :% z) (BinaryCoproduct d (x :% z) (y :% z))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 (x
f x -> Dom x z z -> Cod x (x :% z) (x :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom x z z
z) (y
g y -> Dom y z z -> Cod y (y :% z) (y :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom y z z
z))

  Nat x
f a
a forall z. Obj c z -> Component x a z
fa ||| :: Nat c d x a
-> Nat c d y a -> Nat c d (BinaryCoproduct (Nat c d) x y) a
||| Nat y
g a
_ forall z. Obj c z -> Component y a z
ga = (x :+: y)
-> a
-> (forall z. Obj c z -> Component (x :+: y) a z)
-> Nat c d (x :+: y) a
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (x
f x -> y -> x :+: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryCoproducts k) =>
p -> q -> p :+: q
:+: y
g) a
a (\Obj c z
z -> Obj c z -> Component x a z
forall z. Obj c z -> Component x a z
fa Obj c z
z d (x :% z) (a :% z)
-> d (y :% z) (a :% z)
-> d (BinaryCoproduct d (x :% z) (y :% z)) (a :% z)
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| Obj c z -> Component y a z
forall z. Obj c z -> Component y a z
ga Obj c z
z)
  Nat a1
f1 b1
f2 forall z. Obj c z -> Component a1 b1 z
f +++ :: Nat c d a1 b1
-> Nat c d a2 b2
-> Nat
     c
     d
     (BinaryCoproduct (Nat c d) a1 a2)
     (BinaryCoproduct (Nat c d) b1 b2)
+++ Nat a2
g1 b2
g2 forall z. Obj c z -> Component a2 b2 z
g = (a1 :+: a2)
-> (b1 :+: b2)
-> (forall z. Obj c z -> Component (a1 :+: a2) (b1 :+: b2) z)
-> Nat c d (a1 :+: a2) (b1 :+: b2)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (a1
f1 a1 -> a2 -> a1 :+: a2
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryCoproducts k) =>
p -> q -> p :+: q
:+: a2
g1) (b1
f2 b1 -> b2 -> b1 :+: b2
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryCoproducts k) =>
p -> q -> p :+: q
:+: b2
g2) (\Obj c z
z -> Obj c z -> Component a1 b1 z
forall z. Obj c z -> Component a1 b1 z
f Obj c z
z d (a1 :% z) (b1 :% z)
-> d (a2 :% z) (b2 :% z)
-> d (BinaryCoproduct d (a1 :% z) (a2 :% z))
     (BinaryCoproduct d (b1 :% z) (b2 :% z))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ Obj c z -> Component a2 b2 z
forall z. Obj c z -> Component a2 b2 z
g Obj c z
z)

-- | Terminal objects are the dual of initial objects.
instance HasInitialObject k => HasTerminalObject (Op k) where
  type TerminalObject (Op k) = InitialObject k
  terminalObject :: Obj (Op k) (TerminalObject (Op k))
terminalObject = k (InitialObject k) (InitialObject k)
-> Op k (InitialObject k) (InitialObject k)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k (InitialObject k) (InitialObject k)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject
  terminate :: Obj (Op k) a -> Op k a (TerminalObject (Op k))
terminate (Op k a a
f) = k (InitialObject k) a -> Op k a (InitialObject k)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k a a -> k (InitialObject k) a
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize k a a
f)

-- | Terminal objects are the dual of initial objects.
instance HasTerminalObject k => HasInitialObject (Op k) where
  type InitialObject (Op k) = TerminalObject k
  initialObject :: Obj (Op k) (InitialObject (Op k))
initialObject = k (TerminalObject k) (TerminalObject k)
-> Op k (TerminalObject k) (TerminalObject k)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k (TerminalObject k) (TerminalObject k)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject
  initialize :: Obj (Op k) a -> Op k (InitialObject (Op k)) a
initialize (Op k a a
f) = k a (TerminalObject k) -> Op k (TerminalObject k) a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k a a -> k a (TerminalObject k)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate k a a
f)

-- | Binary products are the dual of binary coproducts.
instance HasBinaryCoproducts k => HasBinaryProducts (Op k) where
  type BinaryProduct (Op k) x y = BinaryCoproduct k x y

  proj1 :: Obj (Op k) x -> Obj (Op k) y -> Op k (BinaryProduct (Op k) x y) x
proj1 (Op k x x
x) (Op k y y
y) = k x (BinaryCoproduct k x y) -> Op k (BinaryCoproduct k x y) x
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k x x -> k y y -> k x (BinaryCoproduct k x y)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 k x x
x k y y
y)
  proj2 :: Obj (Op k) x -> Obj (Op k) y -> Op k (BinaryProduct (Op k) x y) y
proj2 (Op k x x
x) (Op k y y
y) = k y (BinaryCoproduct k x y) -> Op k (BinaryCoproduct k x y) y
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k x x -> k y y -> k y (BinaryCoproduct k x y)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 k x x
x k y y
y)
  Op k x a
f &&& :: Op k a x -> Op k a y -> Op k a (BinaryProduct (Op k) x y)
&&& Op k y a
g = k (BinaryCoproduct k x y) a -> Op k a (BinaryCoproduct k x y)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k x a
f k x a -> k y a -> k (BinaryCoproduct k x y) a
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| k y a
g)
  Op k b1 a1
f *** :: Op k a1 b1
-> Op k a2 b2
-> Op k (BinaryProduct (Op k) a1 a2) (BinaryProduct (Op k) b1 b2)
*** Op k b2 a2
g = k (BinaryCoproduct k b1 b2) (BinaryCoproduct k a1 a2)
-> Op k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k b1 a1
f k b1 a1
-> k b2 a2 -> k (BinaryCoproduct k b1 b2) (BinaryCoproduct k a1 a2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ k b2 a2
g)

-- | Binary products are the dual of binary coproducts.
instance HasBinaryProducts k => HasBinaryCoproducts (Op k) where
  type BinaryCoproduct (Op k) x y = BinaryProduct k x y

  inj1 :: Obj (Op k) x -> Obj (Op k) y -> Op k x (BinaryCoproduct (Op k) x y)
inj1 (Op k x x
x) (Op k y y
y) = k (BinaryProduct k x y) x -> Op k x (BinaryProduct k x y)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k x x -> k y y -> k (BinaryProduct k x y) x
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 k x x
x k y y
y)
  inj2 :: Obj (Op k) x -> Obj (Op k) y -> Op k y (BinaryCoproduct (Op k) x y)
inj2 (Op k x x
x) (Op k y y
y) = k (BinaryProduct k x y) y -> Op k y (BinaryProduct k x y)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k x x -> k y y -> k (BinaryProduct k x y) y
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 k x x
x k y y
y)
  Op k a x
f ||| :: Op k x a -> Op k y a -> Op k (BinaryCoproduct (Op k) x y) a
||| Op k a y
g = k a (BinaryProduct k x y) -> Op k (BinaryProduct k x y) a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k a x
f k a x -> k a y -> k a (BinaryProduct k x y)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& k a y
g)
  Op k b1 a1
f +++ :: Op k a1 b1
-> Op k a2 b2
-> Op
     k (BinaryCoproduct (Op k) a1 a2) (BinaryCoproduct (Op k) b1 b2)
+++ Op k b2 a2
g = k (BinaryProduct k b1 b2) (BinaryProduct k a1 a2)
-> Op k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k b1 a1
f k b1 a1
-> k b2 a2 -> k (BinaryProduct k b1 b2) (BinaryProduct k a1 a2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** k b2 a2
g)




type instance LimitFam Unit k f = f :% ()

-- | The limit of a single object is that object.
instance Category k => HasLimits Unit k where

  limit :: Obj (Nat Unit k) f -> Cone Unit k f (LimitFam Unit k f)
limit (Nat f
f f
_ forall z. Obj Unit z -> Component f f z
_) = Const Unit k (f :% ())
-> f
-> (forall z. Obj Unit z -> Component (Const Unit k (f :% ())) f z)
-> Nat Unit k (Const Unit k (f :% ())) f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj k (f :% ()) -> Const Unit k (f :% ())
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f -> Dom f () () -> Cod f (f :% ()) (f :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f () ()
Obj Unit ()
Unit)) f
f (\Obj Unit z
Unit -> f
f f -> Dom f () () -> Cod f (f :% ()) (f :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f () ()
Obj Unit ()
Unit)
  limitFactorizer :: Cone Unit k f n -> k n (LimitFam Unit k f)
limitFactorizer Cone Unit k f n
n = Cone Unit k f n
n Cone Unit k f n
-> Obj Unit () -> k (Const Unit k n :% ()) (f :% ())
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj Unit ()
Unit

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

-- | The limit of any diagram with an initial object, has the limit at the initial object.
instance (HasInitialObject (i :>>: j), Category i, Category j, Category k) => HasLimits (i :>>: j) k where

  limit :: Obj (Nat (i :>>: j) k) f
-> Cone (i :>>: j) k f (LimitFam (i :>>: j) k f)
limit (Nat f
f f
_ forall z. Obj (i :>>: j) z -> Component f f z
_) = Const (i :>>: j) k (f :% I1 (InitialObject i))
-> f
-> (forall z.
    Obj (i :>>: j) z
    -> Component (Const (i :>>: j) k (f :% I1 (InitialObject i))) f z)
-> Nat
     (i :>>: j) k (Const (i :>>: j) k (f :% I1 (InitialObject i))) f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj k (f :% I1 (InitialObject i))
-> Const (i :>>: j) k (f :% I1 (InitialObject i))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f
-> Dom f (I1 (InitialObject i)) (I1 (InitialObject i))
-> Cod f (f :% I1 (InitialObject i)) (f :% I1 (InitialObject i))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f (I1 (InitialObject i)) (I1 (InitialObject i))
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)) f
f (\Obj (i :>>: j) z
z -> f
f f
-> Dom f (I1 (InitialObject i)) z
-> Cod f (f :% I1 (InitialObject i)) (f :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (i :>>: j) z -> (:>>:) i j (InitialObject (i :>>: j)) z
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj (i :>>: j) z
z)
  limitFactorizer :: Cone (i :>>: j) k f n -> k n (LimitFam (i :>>: j) k f)
limitFactorizer Cone (i :>>: j) k f n
n = Cone (i :>>: j) k f n
n Cone (i :>>: j) k f n
-> (:>>:) i j (I1 (InitialObject i)) (I1 (InitialObject i))
-> k (Const (i :>>: j) k n :% I1 (InitialObject i))
     (f :% I1 (InitialObject i))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! (:>>:) i j (I1 (InitialObject i)) (I1 (InitialObject i))
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject


type instance ColimitFam Unit k f = f :% ()

-- | The colimit of a single object is that object.
instance Category k => HasColimits Unit k where

  colimit :: Obj (Nat Unit k) f -> Cocone Unit k f (ColimitFam Unit k f)
colimit (Nat f
f f
_ forall z. Obj Unit z -> Component f f z
_) = f
-> Const Unit k (f :% ())
-> (forall z. Obj Unit z -> Component f (Const Unit k (f :% ())) z)
-> Nat Unit k f (Const Unit k (f :% ()))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (Obj k (f :% ()) -> Const Unit k (f :% ())
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f -> Dom f () () -> Cod f (f :% ()) (f :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f () ()
Obj Unit ()
Unit)) (\Obj Unit z
Unit -> f
f f -> Dom f () () -> Cod f (f :% ()) (f :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f () ()
Obj Unit ()
Unit)
  colimitFactorizer :: Cocone Unit k f n -> k (ColimitFam Unit k f) n
colimitFactorizer Cocone Unit k f n
n = Cocone Unit k f n
n Cocone Unit k f n
-> Obj Unit () -> k (f :% ()) (Const Unit k n :% ())
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj Unit ()
Unit

type instance ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)

-- | The colimit of any diagram with a terminal object, has the limit at the terminal object.
instance (HasTerminalObject (i :>>: j), Category i, Category j, Category k) => HasColimits (i :>>: j) k where

  colimit :: Obj (Nat (i :>>: j) k) f
-> Cocone (i :>>: j) k f (ColimitFam (i :>>: j) k f)
colimit (Nat f
f f
_ forall z. Obj (i :>>: j) z -> Component f f z
_) = f
-> Const (i :>>: j) k (f :% I2 (TerminalObject j))
-> (forall z.
    Obj (i :>>: j) z
    -> Component f (Const (i :>>: j) k (f :% I2 (TerminalObject j))) z)
-> Nat
     (i :>>: j) k f (Const (i :>>: j) k (f :% I2 (TerminalObject j)))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (Obj k (f :% I2 (TerminalObject j))
-> Const (i :>>: j) k (f :% I2 (TerminalObject j))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f
-> Dom f (I2 (TerminalObject j)) (I2 (TerminalObject j))
-> Cod f (f :% I2 (TerminalObject j)) (f :% I2 (TerminalObject j))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f (I2 (TerminalObject j)) (I2 (TerminalObject j))
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject)) (\Obj (i :>>: j) z
z -> f
f f
-> Dom f z (I2 (TerminalObject j))
-> Cod f (f :% z) (f :% I2 (TerminalObject j))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (i :>>: j) z -> (:>>:) i j z (TerminalObject (i :>>: j))
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj (i :>>: j) z
z)
  colimitFactorizer :: Cocone (i :>>: j) k f n -> k (ColimitFam (i :>>: j) k f) n
colimitFactorizer Cocone (i :>>: j) k f n
n = Cocone (i :>>: j) k f n
n Cocone (i :>>: j) k f n
-> (:>>:) i j (I2 (TerminalObject j)) (I2 (TerminalObject j))
-> k (f :% I2 (TerminalObject j))
     (Const (i :>>: j) k n :% I2 (TerminalObject j))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! (:>>:) i j (I2 (TerminalObject j)) (I2 (TerminalObject j))
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject


data ForAll f = ForAll (forall a. Obj (->) a -> f :% a)
type instance LimitFam (->) (->) f = ForAll f

instance HasLimits (->) (->) where
  limit :: Obj (Nat (->) (->)) f -> Cone (->) (->) f (LimitFam (->) (->) f)
limit (Nat f
f f
_ forall z. Obj (->) z -> Component f f z
_) = Const (->) (->) (ForAll f)
-> f
-> (forall z.
    Obj (->) z -> Component (Const (->) (->) (ForAll f)) f z)
-> Nat (->) (->) (Const (->) (->) (ForAll f)) f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj (->) (ForAll f) -> Const (->) (->) (ForAll f)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\ForAll f
x -> ForAll f
x)) f
f (\Obj (->) z
a (ForAll forall a. Obj (->) a -> f :% a
g) -> Obj (->) z -> f :% z
forall a. Obj (->) a -> f :% a
g Obj (->) z
a)
  limitFactorizer :: Cone (->) (->) f n -> n -> LimitFam (->) (->) f
limitFactorizer Cone (->) (->) f n
n = \n
z -> (forall a. Obj (->) a -> f :% a) -> ForAll f
forall f. (forall a. Obj (->) a -> f :% a) -> ForAll f
ForAll (\Obj (->) a
a -> (Cone (->) (->) f n
n Cone (->) (->) f n
-> Obj (->) a -> (Const (->) (->) n :% a) -> f :% a
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj (->) a
a) n
z)

data Exists f = forall a. Exists (Obj (->) a) (f :% a)
type instance ColimitFam (->) (->) f = Exists f

instance HasColimits (->) (->) where
  colimit :: Obj (Nat (->) (->)) f
-> Cocone (->) (->) f (ColimitFam (->) (->) f)
colimit (Nat f
f f
_ forall z. Obj (->) z -> Component f f z
_) = f
-> Const (->) (->) (Exists f)
-> (forall z.
    Obj (->) z -> Component f (Const (->) (->) (Exists f)) z)
-> Nat (->) (->) f (Const (->) (->) (Exists f))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (Obj (->) (Exists f) -> Const (->) (->) (Exists f)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\Exists f
x -> Exists f
x)) forall z. Obj (->) z -> Component f (Const (->) (->) (Exists f)) z
forall f a. Obj (->) a -> (f :% a) -> Exists f
Exists
  colimitFactorizer :: Cocone (->) (->) f n -> ColimitFam (->) (->) f -> n
colimitFactorizer Cocone (->) (->) f n
n = \(Exists a fa) -> (Cocone (->) (->) f n
n Cocone (->) (->) f n
-> (a -> a) -> (f :% a) -> Const (->) (->) n :% a
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! a -> a
a) f :% a
fa