{-# LANGUAGE
  FlexibleContexts,
  FlexibleInstances,
  GADTs,
  PolyKinds,
  DataKinds,
  LinearTypes,
  LambdaCase,
  EmptyCase,
  BlockArguments,
  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
  , HasLimits(..)
  , Limit
  , LimitFunctor(..)
  , limitAdj
  , adjLimit
  , adjLimitFactorizer
  , rightAdjointPreservesLimits
  , rightAdjointPreservesLimitsInv

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

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

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

) where

import Data.Kind (Type)
import GHC.Exts (FUN)
import GHC.Types (Multiplicity(One))
import Prelude (Either(..))

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 :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type 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 % :: forall a b.
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 = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (Diag j k) a b
f)) (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (Diag j k) a b
f)) (\Obj j z
_ -> Dom (Diag j k) a b
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 :: forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
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 :: forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
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


-- | An instance of @HasLimits j k@ says that @k@ has all limits of type @j@.
class (Category j, Category k) => HasLimits j k where
  -- | Limits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.
  type LimitFam (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) (f :: Type) :: Type
  -- | '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)

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

data LimitFunctor (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) = 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 % :: forall a b.
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 = 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
n forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (LimitFunctor 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 :: forall (j :: * -> * -> *) (k :: * -> * -> *).
HasLimits j k =>
Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
limitAdj = 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 b. Obj c b -> c (f :% (g :% b)) b)
-> Adjunction c d f g
mkAdjunctionTerm forall (j :: * -> * -> *) (k :: * -> * -> *). Diag j k
Diag forall (j :: * -> * -> *) (k :: * -> * -> *). LimitFunctor j k
LimitFunctor (\Obj k a
_ -> forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer) 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 :: forall (k :: * -> * -> *) (j :: * -> * -> *) r f.
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
adj Obj (Nat j k) f
f = 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 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 :: forall (k :: * -> * -> *) (j :: * -> * -> *) r f n.
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
adj Cone j k f n
cone = 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 (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
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 :: forall (j :: * -> * -> *) (c :: * -> * -> *) (d :: * -> * -> *) f g
       t.
(HasLimits j c, HasLimits j d) =>
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
_) =
  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 (forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer Nat j c (Const j c (f :% LimitFam j d (g :.: t))) t
cone)
    where
      l :: Cone j d (g :.: t) (LimitFam j d (g :.: t))
l = forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit (forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (g
g 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 = 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 :: Nat j c (Const j c (f :% LimitFam j d (g :.: t))) t
cone = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj d (LimitFam j d (g :.: t))
x)) t
t (\Obj j z
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 forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj j z
z) (Cone j d (g :.: t) (LimitFam j d (g :.: t))
l 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 :: forall (j :: * -> * -> *) (c :: * -> * -> *) (d :: * -> * -> *) g
       t.
(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
g Obj (Nat j c) t
t = forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (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 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` 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))


-- | An instance of @HasColimits j k@ says that @k@ has all colimits of type @j@.
class (Category j, Category k) => HasColimits j k where
  -- | Colimits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.
  type ColimitFam (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) (f :: Type) :: Type
  -- | '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

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

data ColimitFunctor (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) = 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 % :: forall a b.
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 = forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (ColimitFunctor j k) a b
n) 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
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 :: forall (j :: * -> * -> *) (k :: * -> * -> *).
HasColimits j k =>
Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
colimitAdj = 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 -> d a (g :% (f :% a)))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionInit forall (j :: * -> * -> *) (k :: * -> * -> *). ColimitFunctor j k
ColimitFunctor forall (j :: * -> * -> *) (k :: * -> * -> *). Diag j k
Diag forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit (\Obj k 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 :: forall (k :: * -> * -> *) (j :: * -> * -> *) l f.
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)
adj Obj (Nat j k) f
f = 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 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 :: forall (k :: * -> * -> *) (j :: * -> * -> *) l f n.
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)
adj Cocone j k f n
cocone = 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 (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
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 :: forall (j :: * -> * -> *) (c :: * -> * -> *) (d :: * -> * -> *) f g
       t.
(HasColimits j c, HasColimits j d) =>
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
_) =
  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 (forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer Nat j d t (Const j d (g :% ColimitFam j c (f :.: t)))
cocone)
    where
      l :: Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
l = forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit (forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (f
f 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 = 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 :: Nat j d t (Const j d (g :% ColimitFam j c (f :.: t)))
cocone = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c (ColimitFam j c (f :.: t))
x)) (\Obj j z
z -> 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 forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj j z
z) (Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
l 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 :: forall (j :: * -> * -> *) (c :: * -> * -> *) (d :: * -> * -> *) f
       t.
(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
f Obj (Nat j d) t
t = forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (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 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` 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)


-- | A terminal object is the limit of the functor from /0/ to k.
instance (Category k, HasTerminalObject k) => HasLimits Void k where
  type LimitFam Void k f = TerminalObject k
  limit :: forall f. 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
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject) f
f
  limitFactorizer :: forall f n. Cone Void k f n -> k n (LimitFam Void k f)
limitFactorizer = forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. 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 = forall (m :: Multiplicity) a. Obj (FUN m) a
obj

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

data Top where
  Top :: a %1 -> Top
-- | The terminal object in the category of linear types is `Top`.
instance HasTerminalObject (FUN 'One) where
  type TerminalObject (FUN 'One) = Top

  terminalObject :: Obj (FUN 'One) (TerminalObject (FUN 'One))
terminalObject = forall (m :: Multiplicity) a. Obj (FUN m) a
obj

  terminate :: forall a. Obj (FUN 'One) a -> a %1 -> TerminalObject (FUN 'One)
terminate Obj (FUN 'One) a
_ = forall k. k -> Top
Top

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

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

  terminate :: forall (a :: * -> * -> *). Obj Cat a -> Cat a (TerminalObject Cat)
terminate (CatA ftag
_) = forall k.
(Functor k, Category (Dom k), Category (Cod k)) =>
k -> Cat (Dom k) (Cod k)
CatA (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const 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 = forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject)

  terminate :: forall a. 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
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject) (forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (a
f 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 = Unit () ()
Unit

  terminate :: forall a. Obj Unit a -> Unit a (TerminalObject Unit)
terminate Unit a a
Unit = 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 = forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject

  terminate :: forall a.
Obj (c1 :**: c2) a -> (:**:) c1 c2 a (TerminalObject (c1 :**: c2))
terminate (c1 a1 b1
a1 :**: c2 a2 b2
a2) = forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate c1 a1 b1
a1 forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate 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 = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (d :: * -> * -> *) k b1 (c :: * -> * -> *) f.
d k b1 -> Cograph c d f (I2 k) (I2 b1)
I2A forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject)

  terminate :: forall a.
Obj (c1 :>>: c2) a -> (:>>:) c1 c2 a (TerminalObject (c1 :>>: c2))
terminate (DC (I1A c1 a1 b1
a)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k (d :: * -> * -> *) b1 f.
Obj c k
-> Obj d b1 -> f -> (f :% (k, b1)) -> Cograph c d f (I1 k) (I2 b1)
I12 c1 a1 b1
a forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
  terminate (DC (I2A c2 a2 b2
a)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (d :: * -> * -> *) k b1 (c :: * -> * -> *) f.
d k b1 -> Cograph c d f (I2 k) (I2 b1)
I2A (forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate c2 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


-- | An initial object is the colimit of the functor from /0/ to k.
instance (Category k, HasInitialObject k) => HasColimits Void k where
  type ColimitFam Void k f = InitialObject k
  colimit :: forall f.
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
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)
  colimitFactorizer :: forall f n. Cocone Void k f n -> k (ColimitFam Void k f) n
colimitFactorizer = forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex


data Zero
absurd :: FUN m Zero a
absurd :: forall (m :: Multiplicity) a. Zero %m -> a
absurd = Zero %m -> a
\case

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

  initialObject :: Obj (FUN m) (InitialObject (FUN m))
initialObject = forall (m :: Multiplicity) a. Obj (FUN m) a
obj

  initialize :: forall a. Obj (FUN m) a -> InitialObject (FUN m) %m -> a
initialize Obj (FUN m) a
_ = forall (m :: Multiplicity) a. Zero %m -> a
absurd

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

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

  initialize :: forall (a :: * -> * -> *). Obj Cat a -> Cat (InitialObject Cat) a
initialize (CatA ftag
_) = forall k.
(Functor k, Category (Dom k), Category (Cod k)) =>
k -> Cat (Dom k) (Cod k)
CatA 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 = forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)

  initialize :: forall a. 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
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject) a
f (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (a
f 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 = forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject

  initialize :: forall a.
Obj (c1 :**: c2) a -> (:**:) c1 c2 (InitialObject (c1 :**: c2)) a
initialize (c1 a1 b1
a1 :**: c2 a2 b2
a2) = forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize c1 a1 b1
a1 forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize 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 = Unit () ()
Unit

  initialize :: forall a. Obj Unit a -> Unit (InitialObject Unit) a
initialize Unit a a
Unit = Unit () ()
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 = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k b1 (d :: * -> * -> *) f.
c k b1 -> Cograph c d f (I1 k) (I1 b1)
I1A forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)

  initialize :: forall a.
Obj (c1 :>>: c2) a -> (:>>:) c1 c2 (InitialObject (c1 :>>: c2)) a
initialize (DC (I1A c1 a1 b1
a)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k b1 (d :: * -> * -> *) f.
c k b1 -> Cograph c d f (I1 k) (I1 b1)
I1A (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize c1 a1 b1
a))
  initialize (DC (I2A c2 a2 b2
a)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k (d :: * -> * -> *) b1 f.
Obj c k
-> Obj d b1 -> f -> (f :% (k, b1)) -> Cograph c d f (I1 k) (I2 b1)
I12 forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject c2 a2 b2
a (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 forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a1 b1
l) (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a2 b2
r)) 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 forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a1 b1
l) (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a2 b2
r))


-- | 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
  type LimitFam (i :++: j) k f = BinaryProduct k
    (LimitFam i k (f :.: Inj1 i j))
    (LimitFam j k (f :.: Inj2 i j))

  limit :: forall f.
Obj (Nat (i :++: j) k) f
-> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
limit = 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' :: forall f.
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{} = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (Obj k (LimitFam i k (f :.: Inj1 i j))
x 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 k (LimitFam j k (f :.: Inj2 i j))
y)) (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
h
        where
          x :: Obj k (LimitFam i k (f :.: Inj1 i j))
x = 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 :: Obj k (LimitFam j k (f :.: Inj2 i j))
y = 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 = 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 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` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1)
          lim2 :: Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
lim2 = 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 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` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2)
          h :: Obj (i :++: j) z -> Component (ConstF f (LimitFam (i :++: j) k f)) f z
          h :: forall z.
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 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 forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. 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 Obj k (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 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 forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. 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 Obj k (LimitFam j k (f :.: Inj2 i j))
y

  limitFactorizer :: forall f n. Cone (i :++: j) k f n -> k n (LimitFam (i :++: j) k f)
limitFactorizer Cone (i :++: j) k f n
c =
    forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (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 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` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1))
    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)
&&&
    forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (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 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` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId 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 :: forall x y. Obj (->) x -> Obj (->) y -> BinaryProduct (->) x y -> x
proj1 Obj (->) x
_ Obj (->) y
_ = \(x
x, y
_) -> x
x
  proj2 :: forall x y. Obj (->) x -> Obj (->) y -> BinaryProduct (->) x y -> y
proj2 Obj (->) x
_ Obj (->) y
_ = \(x
_, y
y) -> y
y

  a -> x
f &&& :: forall a x y. (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 *** :: forall a1 b1 a2 b2.
(a1 -> b1)
-> (a2 -> b2)
-> BinaryProduct (->) a1 a2 -> BinaryProduct (->) b1 b2
*** a2 -> b2
g = \(a1
x, a2
y) -> (a1 -> b1
f a1
x, a2 -> b2
g a2
y)


newtype x & y = AddConj (forall r. Either (x %1-> r) (y %1-> r) %1-> r)

-- | The product in the category of linear types is a & b, where you have access to a and b, but not both at the same time.
instance HasBinaryProducts (FUN 'One) where
  type BinaryProduct (FUN 'One) x y = x & y

  proj1 :: forall x y.
Obj (FUN 'One) x
-> Obj (FUN 'One) y -> BinaryProduct (FUN 'One) x y %1 -> x
proj1 Obj (FUN 'One) x
_ Obj (FUN 'One) y
_ = \(AddConj forall r. Either (x %1 -> r) (y %1 -> r) %1 -> r
f) -> forall r. Either (x %1 -> r) (y %1 -> r) %1 -> r
f (forall a b. a -> Either a b
Left forall (m :: Multiplicity) a. Obj (FUN m) a
obj)
  proj2 :: forall x y.
Obj (FUN 'One) x
-> Obj (FUN 'One) y -> BinaryProduct (FUN 'One) x y %1 -> y
proj2 Obj (FUN 'One) x
_ Obj (FUN 'One) y
_ = \(AddConj forall r. Either (x %1 -> r) (y %1 -> r) %1 -> r
f) -> forall r. Either (x %1 -> r) (y %1 -> r) %1 -> r
f (forall a b. b -> Either a b
Right forall (m :: Multiplicity) a. Obj (FUN m) a
obj)

  a %1 -> x
f &&& :: forall a x y.
(a %1 -> x) -> (a %1 -> y) -> a %1 -> BinaryProduct (FUN 'One) x y
&&& a %1 -> y
g = \a
x -> forall x y.
(forall r. Either (x %1 -> r) (y %1 -> r) %1 -> r) -> x & y
AddConj \case
    Left x %1 -> r
h -> x %1 -> r
h (a %1 -> x
f a
x)
    Right y %1 -> r
h -> y %1 -> r
h (a %1 -> y
g a
x)
  a1 %1 -> b1
f *** :: forall a1 b1 a2 b2.
(a1 %1 -> b1)
-> (a2 %1 -> b2)
-> BinaryProduct (FUN 'One) a1 a2
%1 -> BinaryProduct (FUN 'One) b1 b2
*** a2 %1 -> b2
g = \(AddConj forall r. Either (a1 %1 -> r) (a2 %1 -> r) %1 -> r
h) -> forall x y.
(forall r. Either (x %1 -> r) (y %1 -> r) %1 -> r) -> x & y
AddConj \case
    Left b1 %1 -> r
l -> forall r. Either (a1 %1 -> r) (a2 %1 -> r) %1 -> r
h (forall a b. a -> Either a b
Left (\a1
x -> b1 %1 -> r
l (a1 %1 -> b1
f a1
x)))
    Right b2 %1 -> r
r -> forall r. Either (a1 %1 -> r) (a2 %1 -> r) %1 -> r
h (forall a b. b -> Either a b
Right (\a2
x -> b2 %1 -> r
r (a2 %1 -> b2
g a2
x)))



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

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

  CatA ftag
f1 &&& :: forall (a :: * -> * -> *) (x :: * -> * -> *) (y :: * -> * -> *).
Cat a x -> Cat a y -> Cat a (BinaryProduct Cat x y)
&&& CatA ftag
f2 = forall k.
(Functor k, Category (Dom k), Category (Cod k)) =>
k -> Cat (Dom k) (Cod k)
CatA ((ftag
f1 forall f1 f2. (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2
:***: ftag
f2) forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: forall (k :: * -> * -> *). DiagProd k
DiagProd)
  CatA ftag
f1 *** :: forall (a1 :: * -> * -> *) (b1 :: * -> * -> *) (a2 :: * -> * -> *)
       (b2 :: * -> * -> *).
Cat a1 b1
-> Cat a2 b2
-> Cat (BinaryProduct Cat a1 a2) (BinaryProduct Cat b1 b2)
*** CatA ftag
f2 = forall k.
(Functor k, Category (Dom k), Category (Cod k)) =>
k -> Cat (Dom k) (Cod k)
CatA (ftag
f1 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 :: forall x y.
Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) x
proj1 Unit x x
Unit Unit y y
Unit = Unit () ()
Unit
  proj2 :: forall x y.
Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) y
proj2 Unit x x
Unit Unit y y
Unit = Unit () ()
Unit

  Unit a x
Unit &&& :: forall a x y.
Unit a x -> Unit a y -> Unit a (BinaryProduct Unit x y)
&&& Unit a y
Unit = Unit () ()
Unit
  Unit a1 b1
Unit *** :: forall a1 b1 a2 b2.
Unit a1 b1
-> Unit a2 b2
-> Unit (BinaryProduct Unit a1 a2) (BinaryProduct Unit b1 b2)
*** Unit a2 b2
Unit = Unit () ()
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 :: forall x y.
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) = forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 c1 a1 b1
x1 c1 a1 b1
y1 forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 c2 a2 b2
x2 c2 a2 b2
y2
  proj2 :: forall x y.
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) = forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 c1 a1 b1
x1 c1 a1 b1
y1 forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 c2 a2 b2
x2 c2 a2 b2
y2

  (c1 a1 b1
f1 :**: c2 a2 b2
f2) &&& :: forall a x y.
(:**:) 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 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
g1) forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: (c2 a2 b2
f2 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
g2)
  (c1 a1 b1
f1 :**: c2 a2 b2
f2) *** :: forall a1 b1 a2 b2.
(:**:) 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 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) forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: (c2 a2 b2
f2 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 :: forall x y.
Obj (c1 :>>: c2) x
-> Obj (c1 :>>: c2) y
-> (:>>:) c1 c2 (BinaryProduct (c1 :>>: c2) x y) x
proj1 (DC (I1A c1 a1 b1
a)) (DC (I1A c1 a1 b1
b)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k b1 (d :: * -> * -> *) f.
c k b1 -> Cograph c d f (I1 k) (I1 b1)
I1A (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 c1 a1 b1
a c1 a1 b1
b))
  proj1 (DC (I1A c1 a1 b1
a)) (DC (I2A c2 a2 b2
_)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k b1 (d :: * -> * -> *) f.
c k b1 -> Cograph c d f (I1 k) (I1 b1)
I1A c1 a1 b1
a)
  proj1 (DC (I2A c2 a2 b2
a)) (DC (I1A c1 a1 b1
b)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k (d :: * -> * -> *) b1 f.
Obj c k
-> Obj d b1 -> f -> (f :% (k, b1)) -> Cograph c d f (I1 k) (I2 b1)
I12 c1 a1 b1
b c2 a2 b2
a (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
  proj1 (DC (I2A c2 a2 b2
a)) (DC (I2A c2 a2 b2
b)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (d :: * -> * -> *) k b1 (c :: * -> * -> *) f.
d k b1 -> Cograph c d f (I2 k) (I2 b1)
I2A (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 c2 a2 b2
a c2 a2 b2
b))

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

  DC (I1A c1 a1 b1
a) &&& :: forall a x y.
(:>>:) c1 c2 a x
-> (:>>:) c1 c2 a y
-> (:>>:) c1 c2 a (BinaryProduct (c1 :>>: c2) x y)
&&& DC (I1A c1 a1 b1
b) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k b1 (d :: * -> * -> *) f.
c k b1 -> Cograph c d f (I1 k) (I1 b1)
I1A (c1 a1 b1
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)
&&& c1 a1 b1
b))
  DC (I1A c1 a1 b1
a) &&& DC I12{} = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k b1 (d :: * -> * -> *) f.
c k b1 -> Cograph c d f (I1 k) (I1 b1)
I1A c1 a1 b1
a)
  DC I12{} &&& DC (I1A c1 a1 b1
b) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k b1 (d :: * -> * -> *) f.
c k b1 -> Cograph c d f (I1 k) (I1 b1)
I1A c1 a1 b1
b)
  DC (I2A c2 a2 b2
a) &&& DC (I2A c2 a2 b2
b) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (d :: * -> * -> *) k b1 (c :: * -> * -> *) f.
d k b1 -> Cograph c d f (I2 k) (I2 b1)
I2A (c2 a2 b2
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)
&&& c2 a2 b2
b))
  DC (I12 Obj c1 a
a Obj c2 b
b1 Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) &&& DC (I12 Obj c1 a
_ Obj c2 b
b2 Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k (d :: * -> * -> *) b1 f.
Obj c k
-> Obj d b1 -> f -> (f :% (k, b1)) -> Cograph c d f (I1 k) (I2 b1)
I12 Obj c1 a
a (Obj c2 b
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)
*** Obj c2 b
b2) (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())


data ProductFunctor (k :: Type -> Type -> Type) = 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 % :: forall a b.
ProductFunctor k
-> Dom (ProductFunctor k) a b
-> Cod
     (ProductFunctor k) (ProductFunctor k :% a) (ProductFunctor k :% b)
% (k a1 b1
a1 :**: k a2 b2
a2) = k a1 b1
a1 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 :: forall (k :: * -> * -> *).
HasBinaryProducts k =>
Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
prodAdj = 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 b. Obj c b -> c (f :% (g :% b)) b)
-> Adjunction c d f g
mkAdjunctionTerm forall (k :: * -> * -> *). DiagProd k
DiagProd forall (k :: * -> * -> *). ProductFunctor k
ProductFunctor (\Obj k a
_ (k a1 b1
l :**: k a2 b2
r) -> k a1 b1
l 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 a1 b1
l :**: k a2 b2
r) -> 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
l k a2 b2
r forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: 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
l 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) % :: forall a b.
(p :*: q)
-> Dom (p :*: q) a b
-> Cod (p :*: q) ((p :*: q) :% a) ((p :*: q) :% b)
% Dom (p :*: q) a b
f = (p
p forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom (p :*: q) a b
f) 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 forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% 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 :: forall x y.
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
_) = 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 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 -> 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 forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
z) (y
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
z))
  proj2 :: forall x y.
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
_) = 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 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 -> 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 forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
z) (y
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
z))

  Nat a
a x
f forall z. Obj c z -> Component a x z
af &&& :: forall a x y.
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 = 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 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 -> forall z. Obj c z -> Component a x z
af Obj c z
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)
&&& 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 *** :: forall a1 b1 a2 b2.
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 = 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 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 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 -> forall z. Obj c z -> Component a1 b1 z
f Obj c z
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)
*** 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 = (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a1 b1
l) (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a2 b2
r) 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) 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
||| (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a1 b1
l) (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a2 b2
r) 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)


-- | 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
  type ColimitFam (i :++: j) k f = BinaryCoproduct k
    (ColimitFam i k (f :.: Inj1 i j))
    (ColimitFam j k (f :.: Inj2 i j))

  colimit :: forall f.
Obj (Nat (i :++: j) k) f
-> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
colimit = 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' :: forall f.
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{} = 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 (forall (c :: * -> * -> *) (d :: * -> * -> *) f g. Nat c d f g -> f
srcF Obj (Nat (i :++: j) k) f
l) (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (Obj k (ColimitFam i k (f :.: Inj1 i j))
x 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 k (ColimitFam j k (f :.: Inj2 i j))
y)) forall z.
Obj (i :++: j) z
-> Component f (ConstF f (ColimitFam (i :++: j) k f)) z
h
        where
          x :: Obj k (ColimitFam i k (f :.: Inj1 i j))
x = 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 :: Obj k (ColimitFam j k (f :.: Inj2 i j))
y = 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 = 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 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` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1)
          col2 :: Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
col2 = 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 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` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2)
          h :: Obj (i :++: j) z -> Component f (ConstF f (ColimitFam (i :++: j) k f)) z
          h :: forall z.
Obj (i :++: j) z
-> Component f (ConstF f (ColimitFam (i :++: j) k f)) z
h (I1 i a1 b1
n) = 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 Obj k (ColimitFam j k (f :.: Inj2 i j))
y 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 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) = 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 Obj k (ColimitFam j k (f :.: Inj2 i j))
y 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 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 :: forall f n.
Cocone (i :++: j) k f n -> k (ColimitFam (i :++: j) k f) n
colimitFactorizer Cocone (i :++: j) k f n
c =
    forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (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 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` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1))
    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
|||
    forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (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 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` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2))


instance HasBinaryCoproducts (FUN m) where
  type BinaryCoproduct (FUN m) a b = Either a b

  inj1 :: forall x y.
Obj (FUN m) x
-> Obj (FUN m) y -> x %m -> BinaryCoproduct (FUN m) x y
inj1 Obj (FUN m) x
_ Obj (FUN m) y
_ = forall a b. a -> Either a b
Left
  inj2 :: forall x y.
Obj (FUN m) x
-> Obj (FUN m) y -> y %m -> BinaryCoproduct (FUN m) x y
inj2 Obj (FUN m) x
_ Obj (FUN m) y
_ = forall a b. b -> Either a b
Right

  x %m -> a
f ||| :: forall x a y.
(x %m -> a) -> (y %m -> a) -> BinaryCoproduct (FUN m) x y %m -> a
||| y %m -> a
g = \case
    Left x
a -> x %m -> a
f x
a
    Right y
b -> y %m -> a
g y
b
  a1 %m -> b1
f +++ :: forall a1 b1 a2 b2.
(a1 %m -> b1)
-> (a2 %m -> b2)
-> BinaryCoproduct (FUN m) a1 a2
%m -> BinaryCoproduct (FUN m) b1 b2
+++ a2 %m -> b2
g = \case
    Left a1
a -> forall a b. a -> Either a b
Left (a1 %m -> b1
f a1
a)
    Right a2
b -> forall a b. b -> Either a b
Right (a2 %m -> b2
g a2
b)

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

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

  CatA ftag
f1 ||| :: forall (x :: * -> * -> *) (a :: * -> * -> *) (y :: * -> * -> *).
Cat x a -> Cat y a -> Cat (BinaryCoproduct Cat x y) a
||| CatA ftag
f2 = forall k.
(Functor k, Category (Dom k), Category (Cod k)) =>
k -> Cat (Dom k) (Cod k)
CatA (forall (k :: * -> * -> *). CodiagCoprod k
CodiagCoprod forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: (ftag
f1 forall f1 f2. f1 -> f2 -> f1 :+++: f2
:+++: ftag
f2))
  CatA ftag
f1 +++ :: forall (a1 :: * -> * -> *) (b1 :: * -> * -> *) (a2 :: * -> * -> *)
       (b2 :: * -> * -> *).
Cat a1 b1
-> Cat a2 b2
-> Cat (BinaryCoproduct Cat a1 a2) (BinaryCoproduct Cat b1 b2)
+++ CatA ftag
f2 = forall k.
(Functor k, Category (Dom k), Category (Cod k)) =>
k -> Cat (Dom k) (Cod k)
CatA (ftag
f1 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 :: forall x y.
Obj Unit x -> Obj Unit y -> Unit x (BinaryCoproduct Unit x y)
inj1 Unit x x
Unit Unit y y
Unit = Unit () ()
Unit
  inj2 :: forall x y.
Obj Unit x -> Obj Unit y -> Unit y (BinaryCoproduct Unit x y)
inj2 Unit x x
Unit Unit y y
Unit = Unit () ()
Unit

  Unit x a
Unit ||| :: forall x a y.
Unit x a -> Unit y a -> Unit (BinaryCoproduct Unit x y) a
||| Unit y a
Unit = Unit () ()
Unit
  Unit a1 b1
Unit +++ :: forall a1 b1 a2 b2.
Unit a1 b1
-> Unit a2 b2
-> Unit (BinaryCoproduct Unit a1 a2) (BinaryCoproduct Unit b1 b2)
+++ Unit a2 b2
Unit = Unit () ()
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 :: forall x y.
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) = forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 c1 a1 b1
x1 c1 a1 b1
y1 forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (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 c2 a2 b2
x2 c2 a2 b2
y2
  inj2 :: forall x y.
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) = forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 c1 a1 b1
x1 c1 a1 b1
y1 forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (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 c2 a2 b2
x2 c2 a2 b2
y2

  (c1 a1 b1
f1 :**: c2 a2 b2
f2) ||| :: forall x a y.
(:**:) 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 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
g1) forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: (c2 a2 b2
f2 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
g2)
  (c1 a1 b1
f1 :**: c2 a2 b2
f2) +++ :: forall a1 b1 a2 b2.
(:**:) 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 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) forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: (c2 a2 b2
f2 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 :: forall x y.
Obj (c1 :>>: c2) x
-> Obj (c1 :>>: c2) y
-> (:>>:) c1 c2 x (BinaryCoproduct (c1 :>>: c2) x y)
inj1 (DC (I1A c1 a1 b1
a)) (DC (I1A c1 a1 b1
b)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k b1 (d :: * -> * -> *) f.
c k b1 -> Cograph c d f (I1 k) (I1 b1)
I1A (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 c1 a1 b1
a c1 a1 b1
b))
  inj1 (DC (I1A c1 a1 b1
a)) (DC (I2A c2 a2 b2
b)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k (d :: * -> * -> *) b1 f.
Obj c k
-> Obj d b1 -> f -> (f :% (k, b1)) -> Cograph c d f (I1 k) (I2 b1)
I12 c1 a1 b1
a c2 a2 b2
b (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
  inj1 (DC (I2A c2 a2 b2
a)) (DC (I1A c1 a1 b1
_)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (d :: * -> * -> *) k b1 (c :: * -> * -> *) f.
d k b1 -> Cograph c d f (I2 k) (I2 b1)
I2A c2 a2 b2
a)
  inj1 (DC (I2A c2 a2 b2
a)) (DC (I2A c2 a2 b2
b)) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (d :: * -> * -> *) k b1 (c :: * -> * -> *) f.
d k b1 -> Cograph c d f (I2 k) (I2 b1)
I2A (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 c2 a2 b2
a c2 a2 b2
b))

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

  DC (I1A c1 a1 b1
a) ||| :: forall x a y.
(:>>:) c1 c2 x a
-> (:>>:) c1 c2 y a
-> (:>>:) c1 c2 (BinaryCoproduct (c1 :>>: c2) x y) a
||| DC (I1A c1 a1 b1
b) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k b1 (d :: * -> * -> *) f.
c k b1 -> Cograph c d f (I1 k) (I1 b1)
I1A (c1 a1 b1
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
||| c1 a1 b1
b))
  DC (I2A c2 a2 b2
a) ||| DC I12{} = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (d :: * -> * -> *) k b1 (c :: * -> * -> *) f.
d k b1 -> Cograph c d f (I2 k) (I2 b1)
I2A c2 a2 b2
a)
  DC I12{} ||| DC (I2A c2 a2 b2
b) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (d :: * -> * -> *) k b1 (c :: * -> * -> *) f.
d k b1 -> Cograph c d f (I2 k) (I2 b1)
I2A c2 a2 b2
b)
  DC (I2A c2 a2 b2
a) ||| DC (I2A c2 a2 b2
b) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (d :: * -> * -> *) k b1 (c :: * -> * -> *) f.
d k b1 -> Cograph c d f (I2 k) (I2 b1)
I2A (c2 a2 b2
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
||| c2 a2 b2
b))
  DC (I12 Obj c1 a
a1 Obj c2 b
b Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) ||| DC (I12 Obj c1 a
a2 Obj c2 b
_ Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) = forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b
-> (:>>:) c1 c2 a b
DC (forall (c :: * -> * -> *) k (d :: * -> * -> *) b1 f.
Obj c k
-> Obj d b1 -> f -> (f :% (k, b1)) -> Cograph c d f (I1 k) (I2 b1)
I12 (Obj c1 a
a1 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 c1 a
a2) Obj c2 b
b (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())


data CoproductFunctor (k :: Type -> Type -> Type) = 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 % :: forall a b.
CoproductFunctor k
-> Dom (CoproductFunctor k) a b
-> Cod
     (CoproductFunctor k)
     (CoproductFunctor k :% a)
     (CoproductFunctor k :% b)
% (k a1 b1
a1 :**: k a2 b2
a2) = k a1 b1
a1 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 :: forall (k :: * -> * -> *).
HasBinaryCoproducts k =>
Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)
coprodAdj = 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 -> d a (g :% (f :% a)))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionInit forall (k :: * -> * -> *). CoproductFunctor k
CoproductFunctor forall (k :: * -> * -> *). DiagProd k
DiagProd (\(k a1 b1
l :**: k a2 b2
r) -> 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
l k a2 b2
r forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (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
l k a2 b2
r) (\Obj k b
_ (k a1 b1
l :**: k a2 b2
r) -> k a1 b1
l 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 a2 b2
r)

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) % :: forall a b.
(p :+: q)
-> Dom (p :+: q) a b
-> Cod (p :+: q) ((p :+: q) :% a) ((p :+: q) :% b)
% Dom (p :+: q) a b
f = (p
p forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom (p :+: q) a b
f) 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 forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% 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 :: forall x y.
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
_) = 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 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 -> 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 forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
z) (y
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
z))
  inj2 :: forall x y.
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
_) = 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 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 -> 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 forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
z) (y
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
z))

  Nat x
f a
a forall z. Obj c z -> Component x a z
fa ||| :: forall x a y.
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 = 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 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 -> forall z. Obj c z -> Component x a z
fa Obj c z
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
||| 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 +++ :: forall a1 b1 a2 b2.
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 = 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 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 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 -> forall z. Obj c z -> Component a1 b1 z
f Obj c z
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)
+++ 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 = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject
  terminate :: forall (a :: k). Obj (Op k) a -> Op k a (TerminalObject (Op k))
terminate (Op k a a
f) = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (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 = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject
  initialize :: forall (a :: k). Obj (Op k) a -> Op k (InitialObject (Op k)) a
initialize (Op k a a
f) = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (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 :: forall (x :: k) (y :: k).
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) = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (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 :: forall (x :: k) (y :: k).
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) = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (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 &&& :: forall (a :: k) (x :: k) (y :: k).
Op k a x -> Op k a y -> Op k a (BinaryProduct (Op k) x y)
&&& Op k y a
g = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (k x a
f 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 *** :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k).
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 = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (k b1 a1
f 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 :: forall (x :: k) (y :: k).
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) = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (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 :: forall (x :: k) (y :: k).
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) = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (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 ||| :: forall (x :: k) (a :: k) (y :: k).
Op k x a -> Op k y a -> Op k (BinaryCoproduct (Op k) x y) a
||| Op k a y
g = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (k a x
f 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 +++ :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k).
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 = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (k b1 a1
f 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)




-- | The limit of a single object is that object.
instance Category k => HasLimits Unit k where
  type LimitFam Unit k f = f :% ()
  limit :: forall f. 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
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Unit () ()
Unit)) f
f (\Obj Unit z
Unit -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Unit () ()
Unit)
  limitFactorizer :: forall f n. Cone Unit k f n -> k n (LimitFam Unit k f)
limitFactorizer Cone Unit k f n
n = Cone Unit k f n
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)
! Unit () ()
Unit

-- | 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
  type LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)
  limit :: forall f.
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
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)) f
f (\Obj (i :>>: j) z
z -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj (i :>>: j) z
z)
  limitFactorizer :: forall f n. 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 forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject


-- | The colimit of a single object is that object.
instance Category k => HasColimits Unit k where
  type ColimitFam Unit k f = f :% ()
  colimit :: forall f.
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
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Unit () ()
Unit)) (\Obj Unit z
Unit -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Unit () ()
Unit)
  colimitFactorizer :: forall f n. Cocone Unit k f n -> k (ColimitFam Unit k f) n
colimitFactorizer Cocone Unit k f n
n = Cocone Unit k f n
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)
! Unit () ()
Unit

-- | 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
  type ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)
  colimit :: forall f.
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
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject)) (\Obj (i :>>: j) z
z -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj (i :>>: j) z
z)
  colimitFactorizer :: forall f n.
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 forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject


newtype ForAll f = ForAll (forall a. Obj (->) a -> f :% a)

instance HasLimits (->) (->) where
  type LimitFam (->) (->) f = ForAll f
  limit :: forall f.
Obj (Nat (->) (->)) f -> Cone (->) (->) f (LimitFam (->) (->) f)
limit (Nat f
f f
_ forall z. Obj (->) z -> Component f f z
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const forall (m :: Multiplicity) a. Obj (FUN m) a
obj) f
f (\Obj (->) z
a (ForAll forall a. Obj (->) a -> f :% a
g) -> forall a. Obj (->) a -> f :% a
g Obj (->) z
a)
  limitFactorizer :: forall f n. Cone (->) (->) f n -> n -> LimitFam (->) (->) f
limitFactorizer Cone (->) (->) f n
n = \n
z -> forall f. (forall a. Obj (->) a -> f :% a) -> ForAll f
ForAll (\Obj (->) a
a -> (Cone (->) (->) f n
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 (->) a
a) n
z)

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

instance HasColimits (->) (->) where
  type ColimitFam (->) (->) f = Exists f
  colimit :: forall f.
Obj (Nat (->) (->)) f
-> Cocone (->) (->) f (ColimitFam (->) (->) f)
colimit (Nat f
f f
_ forall z. Obj (->) z -> Component f f z
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const forall (m :: Multiplicity) a. Obj (FUN m) a
obj) forall f a. Obj (->) a -> (f :% a) -> Exists f
Exists
  colimitFactorizer :: forall f n. Cocone (->) (->) f n -> ColimitFam (->) (->) f -> n
colimitFactorizer Cocone (->) (->) f n
n = \(Exists Obj (->) a
a f :% a
fa) -> (Cocone (->) (->) f n
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 (->) a
a) f :% a
fa