{-# LANGUAGE
FlexibleContexts,
FlexibleInstances,
GADTs,
PolyKinds,
DataKinds,
MultiParamTypeClasses,
RankNTypes,
ScopedTypeVariables,
TypeOperators,
TypeFamilies,
TypeSynonymInstances,
UndecidableInstances,
NoImplicitPrelude #-}
module Data.Category.Limit (
Diag(..)
, DiagF
, Cone
, Cocone
, coneVertex
, coconeVertex
, LimitFam
, Limit
, HasLimits(..)
, LimitFunctor(..)
, limitAdj
, adjLimit
, adjLimitFactorizer
, rightAdjointPreservesLimits
, rightAdjointPreservesLimitsInv
, ColimitFam
, Colimit
, HasColimits(..)
, ColimitFunctor(..)
, colimitAdj
, adjColimit
, adjColimitFactorizer
, leftAdjointPreservesColimits
, leftAdjointPreservesColimitsInv
, HasTerminalObject(..)
, HasInitialObject(..)
, Zero
, HasBinaryProducts(..)
, ProductFunctor(..)
, (:*:)(..)
, prodAdj
, HasBinaryCoproducts(..)
, CoproductFunctor(..)
, (:+:)(..)
, coprodAdj
) where
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Adjunction
import Data.Category.Product
import Data.Category.Coproduct
import Data.Category.Unit
import Data.Category.Void
infixl 3 ***
infixl 3 &&&
infixl 2 +++
infixl 2 |||
data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
Diag :: Diag j k
instance (Category j, Category k) => Functor (Diag j k) where
type Dom (Diag j k) = k
type Cod (Diag j k) = Nat j k
type Diag j k :% a = Const j k a
Diag j k
Diag % :: Diag j k
-> Dom (Diag j k) a b
-> Cod (Diag j k) (Diag j k :% a) (Diag j k :% b)
% Dom (Diag j k) a b
f = Const j k a
-> Const j k b
-> (forall z. Obj j z -> Component (Const j k a) (Const j k b) z)
-> Nat j k (Const j k a) (Const j k b)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj k a -> Const j k a
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (k a b -> Obj k a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a b
Dom (Diag j k) a b
f)) (Obj k b -> Const j k b
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (k a b -> Obj k b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a b
Dom (Diag j k) a b
f)) (\Obj j z
_ -> Dom (Diag j k) a b
Component (Const j k a) (Const j k b) z
f)
type DiagF f = Diag (Dom f) (Cod f)
type Cone j k f n = Nat j k (Const j k n) f
type Cocone j k f n = Nat j k f (Const j k n)
coneVertex :: Cone j k f n -> Obj k n
coneVertex :: Cone j k f n -> Obj k n
coneVertex (Nat (Const Obj k n
x) f
_ forall z. Obj j z -> Component (Const j k n) f z
_) = Obj k n
x
coconeVertex :: Cocone j k f n -> Obj k n
coconeVertex :: Cocone j k f n -> Obj k n
coconeVertex (Nat f
_ (Const Obj k n
x) forall z. Obj j z -> Component f (Const j k n) z
_) = Obj k n
x
type family LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *
type Limit f = LimitFam (Dom f) (Cod f) f
class (Category j, Category k) => HasLimits j k where
limit :: Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limitFactorizer :: Cone j k f n -> k n (LimitFam j k f)
data LimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = LimitFunctor
instance HasLimits j k => Functor (LimitFunctor j k) where
type Dom (LimitFunctor j k) = Nat j k
type Cod (LimitFunctor j k) = k
type LimitFunctor j k :% f = LimitFam j k f
LimitFunctor j k
LimitFunctor % :: LimitFunctor j k
-> Dom (LimitFunctor j k) a b
-> Cod
(LimitFunctor j k) (LimitFunctor j k :% a) (LimitFunctor j k :% b)
% Dom (LimitFunctor j k) a b
n = Cone j k b (LimitFam j k a) -> k (LimitFam j k a) (LimitFam j k b)
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (Dom (LimitFunctor j k) a b
Nat j k a b
n Nat j k a b
-> Nat j k (Const j k (LimitFam j k a)) a
-> Cone j k b (LimitFam j k a)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj (Nat j k) a -> Nat j k (Const j k (LimitFam j k a)) a
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit (Nat j k a b -> Obj (Nat j k) a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (LimitFunctor j k) a b
Nat j k a b
n))
limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
limitAdj :: Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
limitAdj = Diag j k
-> LimitFunctor j k
-> (forall a b.
Obj k a
-> Nat j k (Diag j k :% a) b -> k a (LimitFunctor j k :% b))
-> (forall a.
Obj (Nat j k) a
-> Component (Diag j k :.: LimitFunctor j k) (Id (Nat j k)) a)
-> Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionCounit Diag j k
forall (j :: * -> * -> *) (k :: * -> * -> *). Diag j k
Diag LimitFunctor j k
forall (j :: * -> * -> *) (k :: * -> * -> *). LimitFunctor j k
LimitFunctor (\Obj k a
_ -> Nat j k (Diag j k :% a) b -> k a (LimitFunctor j k :% b)
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer) forall a.
Obj (Nat j k) a
-> Component (Diag j k :.: LimitFunctor j k) (Id (Nat j k)) a
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit
adjLimit :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Obj (Nat j k) f -> Cone j k f (r :% f)
adjLimit :: Adjunction (Nat j k) k (Diag j k) r
-> Obj (Nat j k) f -> Cone j k f (r :% f)
adjLimit Adjunction (Nat j k) k (Diag j k) r
adj Obj (Nat j k) f
f = Adjunction (Nat j k) k (Diag j k) r
-> Nat (Nat j k) (Nat j k) (Diag j k :.: r) (Id (Nat j k))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit Adjunction (Nat j k) k (Diag j k) r
adj Nat (Nat j k) (Nat j k) (Diag j k :.: r) (Id (Nat j k))
-> Obj (Nat j k) f
-> Nat j k ((Diag j k :.: r) :% f) (Id (Nat j k) :% f)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj (Nat j k) f
f
adjLimitFactorizer :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Cone j k f n -> k n (r :% f)
adjLimitFactorizer :: Adjunction (Nat j k) k (Diag j k) r -> Cone j k f n -> k n (r :% f)
adjLimitFactorizer Adjunction (Nat j k) k (Diag j k) r
adj Cone j k f n
cone = Adjunction (Nat j k) k (Diag j k) r
-> Obj k n -> Nat j k (Diag j k :% n) f -> k n (r :% f)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct Adjunction (Nat j k) k (Diag j k) r
adj (Cone j k f n -> Obj k n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
coneVertex Cone j k f n
cone) Cone j k f n
Nat j k (Diag j k :% n) f
cone
rightAdjointPreservesLimits
:: (HasLimits j c, HasLimits j d)
=> Adjunction c d f g -> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t)
rightAdjointPreservesLimits :: Adjunction c d f g
-> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t)
rightAdjointPreservesLimits adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) (Nat t
t t
_ forall z. Obj j z -> Component t t z
_) =
Adjunction c d f g
-> Obj d (LimitFam j d (g :.: t))
-> c (f :% LimitFam j d (g :.: t)) (LimitFam j c t)
-> d (LimitFam j d (g :.: t)) (g :% LimitFam j c t)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct Adjunction c d f g
adj Obj d (LimitFam j d (g :.: t))
x (Cone j c t (f :% LimitFam j d (g :.: t))
-> c (f :% LimitFam j d (g :.: t)) (LimitFam j c t)
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer Cone j c t (f :% LimitFam j d (g :.: t))
cone)
where
l :: Cone j d (g :.: t) (LimitFam j d (g :.: t))
l = Obj (Nat j d) (g :.: t)
-> Cone j d (g :.: t) (LimitFam j d (g :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit ((g :.: t)
-> Nat (Dom (g :.: t)) (Cod (g :.: t)) (g :.: t) (g :.: t)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (g
g g -> t -> g :.: t
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: t
t))
x :: Obj d (LimitFam j d (g :.: t))
x = Cone j d (g :.: t) (LimitFam j d (g :.: t))
-> Obj d (LimitFam j d (g :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
coneVertex Cone j d (g :.: t) (LimitFam j d (g :.: t))
l
cone :: Cone j c t (f :% LimitFam j d (g :.: t))
cone = Const j c (f :% LimitFam j d (g :.: t))
-> t
-> (forall z.
Obj j z -> Component (Const j c (f :% LimitFam j d (g :.: t))) t z)
-> Cone j c t (f :% LimitFam j d (g :.: t))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj c (f :% LimitFam j d (g :.: t))
-> Const j c (f :% LimitFam j d (g :.: t))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f
-> Dom f (LimitFam j d (g :.: t)) (LimitFam j d (g :.: t))
-> Cod
f (f :% LimitFam j d (g :.: t)) (f :% LimitFam j d (g :.: t))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj d (LimitFam j d (g :.: t))
Dom f (LimitFam j d (g :.: t)) (LimitFam j d (g :.: t))
x)) t
t (\Obj j z
z -> Adjunction c d f g
-> Obj c (t :% z)
-> d (LimitFam j d (g :.: t)) (g :% (t :% z))
-> c (f :% LimitFam j d (g :.: t)) (t :% z)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct Adjunction c d f g
adj (t
t t -> Dom t z z -> Cod t (t :% z) (t :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj j z
Dom t z z
z) (Cone j d (g :.: t) (LimitFam j d (g :.: t))
l Cone j d (g :.: t) (LimitFam j d (g :.: t))
-> Obj j z
-> d (Const j d (LimitFam j d (g :.: t)) :% z) ((g :.: t) :% z)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj j z
z))
rightAdjointPreservesLimitsInv
:: (HasLimits j c, HasLimits j d)
=> Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% LimitFam j c t) (LimitFam j d (g :.: t))
rightAdjointPreservesLimitsInv :: Obj (Nat c d) g
-> Obj (Nat j c) t
-> d (g :% LimitFam j c t) (LimitFam j d (g :.: t))
rightAdjointPreservesLimitsInv Obj (Nat c d) g
g Obj (Nat j c) t
t = Cone j d (g :.: t) (g :% LimitFam j c t)
-> d (g :% LimitFam j c t) (LimitFam j d (g :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (Nat j d (g :.: Const j c (LimitFam j c t)) (g :.: t)
-> Cone j d (g :.: t) (g :% LimitFam j c t)
forall (j :: * -> * -> *) (d :: * -> * -> *) f (c :: * -> * -> *) x
g.
Nat j d (f :.: Const j c x) g -> Nat j d (Const j d (f :% x)) g
constPrecompIn (Obj (Nat c d) g
g Obj (Nat c d) g
-> Nat j c (Const j c (LimitFam j c t)) t
-> Nat j d (g :.: Const j c (LimitFam j c t)) (g :.: t)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Obj (Nat j c) t -> Nat j c (Const j c (LimitFam j c t)) t
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit Obj (Nat j c) t
t))
type family ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *
type Colimit f = ColimitFam (Dom f) (Cod f) f
class (Category j, Category k) => HasColimits j k where
colimit :: Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimitFactorizer :: Cocone j k f n -> k (ColimitFam j k f) n
data ColimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = ColimitFunctor
instance HasColimits j k => Functor (ColimitFunctor j k) where
type Dom (ColimitFunctor j k) = Nat j k
type Cod (ColimitFunctor j k) = k
type ColimitFunctor j k :% f = ColimitFam j k f
ColimitFunctor j k
ColimitFunctor % :: ColimitFunctor j k
-> Dom (ColimitFunctor j k) a b
-> Cod
(ColimitFunctor j k)
(ColimitFunctor j k :% a)
(ColimitFunctor j k :% b)
% Dom (ColimitFunctor j k) a b
n = Cocone j k a (ColimitFam j k b)
-> k (ColimitFam j k a) (ColimitFam j k b)
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (Obj (Nat j k) b -> Cocone j k b (ColimitFam j k b)
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit (Nat j k a b -> Obj (Nat j k) b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (ColimitFunctor j k) a b
Nat j k a b
n) Cocone j k b (ColimitFam j k b)
-> Nat j k a b -> Cocone j k a (ColimitFam j k b)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Dom (ColimitFunctor j k) a b
Nat j k a b
n)
colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
colimitAdj :: Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
colimitAdj = ColimitFunctor j k
-> Diag j k
-> (forall a.
Obj (Nat j k) a
-> Component (Id (Nat j k)) (Diag j k :.: ColimitFunctor j k) a)
-> (forall a b.
Obj k b
-> Nat j k a (Diag j k :% b) -> k (ColimitFunctor j k :% a) b)
-> Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionUnit ColimitFunctor j k
forall (j :: * -> * -> *) (k :: * -> * -> *). ColimitFunctor j k
ColimitFunctor Diag j k
forall (j :: * -> * -> *) (k :: * -> * -> *). Diag j k
Diag forall a.
Obj (Nat j k) a
-> Component (Id (Nat j k)) (Diag j k :.: ColimitFunctor j k) a
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit (\Obj k b
_ -> Nat j k a (Diag j k :% b) -> k (ColimitFunctor j k :% a) b
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer)
adjColimit :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Obj (Nat j k) f -> Cocone j k f (l :% f)
adjColimit :: Adjunction k (Nat j k) l (Diag j k)
-> Obj (Nat j k) f -> Cocone j k f (l :% f)
adjColimit Adjunction k (Nat j k) l (Diag j k)
adj Obj (Nat j k) f
f = Adjunction k (Nat j k) l (Diag j k)
-> Nat (Nat j k) (Nat j k) (Id (Nat j k)) (Diag j k :.: l)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction k (Nat j k) l (Diag j k)
adj Nat (Nat j k) (Nat j k) (Id (Nat j k)) (Diag j k :.: l)
-> Obj (Nat j k) f
-> Nat j k (Id (Nat j k) :% f) ((Diag j k :.: l) :% f)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj (Nat j k) f
f
adjColimitFactorizer :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Cocone j k f n -> k (l :% f) n
adjColimitFactorizer :: Adjunction k (Nat j k) l (Diag j k)
-> Cocone j k f n -> k (l :% f) n
adjColimitFactorizer Adjunction k (Nat j k) l (Diag j k)
adj Cocone j k f n
cocone = Adjunction k (Nat j k) l (Diag j k)
-> Obj k n -> Nat j k f (Diag j k :% n) -> k (l :% f) n
forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct Adjunction k (Nat j k) l (Diag j k)
adj (Cocone j k f n -> Obj k n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex Cocone j k f n
cocone) Cocone j k f n
Nat j k f (Diag j k :% n)
cocone
leftAdjointPreservesColimits
:: (HasColimits j c, HasColimits j d)
=> Adjunction c d f g -> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t))
leftAdjointPreservesColimits :: Adjunction c d f g
-> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t))
leftAdjointPreservesColimits adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) (Nat t
t t
_ forall z. Obj j z -> Component t t z
_) =
Adjunction c d f g
-> Obj c (ColimitFam j c (f :.: t))
-> d (ColimitFam j d t) (g :% ColimitFam j c (f :.: t))
-> c (f :% ColimitFam j d t) (ColimitFam j c (f :.: t))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct Adjunction c d f g
adj Obj c (ColimitFam j c (f :.: t))
x (Cocone j d t (g :% ColimitFam j c (f :.: t))
-> d (ColimitFam j d t) (g :% ColimitFam j c (f :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer Cocone j d t (g :% ColimitFam j c (f :.: t))
cocone)
where
l :: Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
l = Obj (Nat j c) (f :.: t)
-> Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit ((f :.: t)
-> Nat (Dom (f :.: t)) (Cod (f :.: t)) (f :.: t) (f :.: t)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (f
f f -> t -> f :.: t
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: t
t))
x :: Obj c (ColimitFam j c (f :.: t))
x = Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
-> Obj c (ColimitFam j c (f :.: t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
l
cocone :: Cocone j d t (g :% ColimitFam j c (f :.: t))
cocone = t
-> Const j d (g :% ColimitFam j c (f :.: t))
-> (forall z.
Obj j z
-> Component t (Const j d (g :% ColimitFam j c (f :.: t))) z)
-> Cocone j d t (g :% ColimitFam j c (f :.: t))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat t
t (Obj d (g :% ColimitFam j c (f :.: t))
-> Const j d (g :% ColimitFam j c (f :.: t))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (g
g g
-> Dom g (ColimitFam j c (f :.: t)) (ColimitFam j c (f :.: t))
-> Cod
g (g :% ColimitFam j c (f :.: t)) (g :% ColimitFam j c (f :.: t))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c (ColimitFam j c (f :.: t))
Dom g (ColimitFam j c (f :.: t)) (ColimitFam j c (f :.: t))
x)) (\Obj j z
z -> Adjunction c d f g
-> Obj d (t :% z)
-> c (f :% (t :% z)) (ColimitFam j c (f :.: t))
-> d (t :% z) (g :% ColimitFam j c (f :.: t))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct Adjunction c d f g
adj (t
t t -> Dom t z z -> Cod t (t :% z) (t :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj j z
Dom t z z
z) (Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
l Cocone j c (f :.: t) (ColimitFam j c (f :.: t))
-> Obj j z
-> c ((f :.: t) :% z) (Const j c (ColimitFam j c (f :.: t)) :% z)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj j z
z))
leftAdjointPreservesColimitsInv
:: (HasColimits j c, HasColimits j d)
=> Obj (Nat d c) f -> Obj (Nat j d) t -> c (ColimitFam j c (f :.: t)) (f :% ColimitFam j d t)
leftAdjointPreservesColimitsInv :: Obj (Nat d c) f
-> Obj (Nat j d) t
-> c (ColimitFam j c (f :.: t)) (f :% ColimitFam j d t)
leftAdjointPreservesColimitsInv Obj (Nat d c) f
f Obj (Nat j d) t
t = Cocone j c (f :.: t) (f :% ColimitFam j d t)
-> c (ColimitFam j c (f :.: t)) (f :% ColimitFam j d t)
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (Nat j c (f :.: t) (f :.: Const j d (ColimitFam j d t))
-> Cocone j c (f :.: t) (f :% ColimitFam j d t)
forall (j :: * -> * -> *) (d :: * -> * -> *) f g (c :: * -> * -> *)
x.
Nat j d f (g :.: Const j c x) -> Nat j d f (Const j d (g :% x))
constPrecompOut (Obj (Nat d c) f
f Obj (Nat d c) f
-> Nat j d t (Const j d (ColimitFam j d t))
-> Nat j c (f :.: t) (f :.: Const j d (ColimitFam j d t))
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Obj (Nat j d) t -> Nat j d t (Const j d (ColimitFam j d t))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit Obj (Nat j d) t
t))
class Category k => HasTerminalObject k where
type TerminalObject k :: Kind k
terminalObject :: Obj k (TerminalObject k)
terminate :: Obj k a -> k a (TerminalObject k)
type instance LimitFam Void k f = TerminalObject k
instance (Category k, HasTerminalObject k) => HasLimits Void k where
limit :: Obj (Nat Void k) f -> Cone Void k f (LimitFam Void k f)
limit (Nat f
f f
_ forall z. Obj Void z -> Component f f z
_) = Const Void k (TerminalObject k)
-> f -> Nat Void k (Const Void k (TerminalObject k)) f
forall f g (d :: * -> * -> *).
(Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d,
Cod g ~ d) =>
f -> g -> Nat Void d f g
voidNat (Obj k (TerminalObject k) -> Const Void k (TerminalObject k)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj k (TerminalObject k)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject) f
f
limitFactorizer :: Cone Void k f n -> k n (LimitFam Void k f)
limitFactorizer = Obj k n -> k n (TerminalObject k)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate (Obj k n -> k n (TerminalObject k))
-> (Cone Void k f n -> Obj k n)
-> Cone Void k f n
-> k n (TerminalObject k)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cone Void k f n -> Obj k n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
coneVertex
instance HasTerminalObject (->) where
type TerminalObject (->) = ()
terminalObject :: Obj (->) (TerminalObject (->))
terminalObject = \TerminalObject (->)
x -> TerminalObject (->)
x
terminate :: Obj (->) a -> a -> TerminalObject (->)
terminate Obj (->) a
_ a
_ = ()
instance HasTerminalObject Cat where
type TerminalObject Cat = Unit
terminalObject :: Obj Cat (TerminalObject Cat)
terminalObject = Id Unit -> Cat (Dom (Id Unit)) (Cod (Id Unit))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Id Unit
forall (k :: * -> * -> *). Id k
Id
terminate :: Obj Cat a -> Cat a (TerminalObject Cat)
terminate (CatA ftag
_) = Const a Unit ()
-> Cat (Dom (Const a Unit ())) (Cod (Const a Unit ()))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA (Obj Unit () -> Const a Unit ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj Unit ()
Unit)
instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) where
type TerminalObject (Nat c d) = Const c d (TerminalObject d)
terminalObject :: Obj (Nat c d) (TerminalObject (Nat c d))
terminalObject = Const c d (TerminalObject d)
-> Nat
(Dom (Const c d (TerminalObject d)))
(Cod (Const c d (TerminalObject d)))
(Const c d (TerminalObject d))
(Const c d (TerminalObject d))
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (Obj d (TerminalObject d) -> Const c d (TerminalObject d)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj d (TerminalObject d)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject)
terminate :: Obj (Nat c d) a -> Nat c d a (TerminalObject (Nat c d))
terminate (Nat a
f a
_ forall z. Obj c z -> Component a a z
_) = a
-> Const c d (TerminalObject d)
-> (forall z.
Obj c z -> Component a (Const c d (TerminalObject d)) z)
-> Nat c d a (Const c d (TerminalObject d))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat a
f (Obj d (TerminalObject d) -> Const c d (TerminalObject d)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj d (TerminalObject d)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject) (Obj d (a :% z) -> d (a :% z) (TerminalObject d)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate (Obj d (a :% z) -> d (a :% z) (TerminalObject d))
-> (c z z -> Obj d (a :% z))
-> c z z
-> d (a :% z) (TerminalObject d)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (a
f a -> Dom a z z -> Cod a (a :% z) (a :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
%))
instance HasTerminalObject Unit where
type TerminalObject Unit = ()
terminalObject :: Obj Unit (TerminalObject Unit)
terminalObject = Obj Unit ()
Obj Unit (TerminalObject Unit)
Unit
terminate :: Obj Unit a -> Unit a (TerminalObject Unit)
terminate Obj Unit a
Unit = Unit a (TerminalObject Unit)
Obj Unit ()
Unit
instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2) where
type TerminalObject (c1 :**: c2) = (TerminalObject c1, TerminalObject c2)
terminalObject :: Obj (c1 :**: c2) (TerminalObject (c1 :**: c2))
terminalObject = Obj c1 (TerminalObject c1)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject Obj c1 (TerminalObject c1)
-> c2 (TerminalObject c2) (TerminalObject c2)
-> (:**:)
c1
c2
(TerminalObject c1, TerminalObject c2)
(TerminalObject c1, TerminalObject c2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: c2 (TerminalObject c2) (TerminalObject c2)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject
terminate :: Obj (c1 :**: c2) a -> (:**:) c1 c2 a (TerminalObject (c1 :**: c2))
terminate (c1 a1 b1
a1 :**: c2 a2 b2
a2) = Obj c1 a1 -> c1 a1 (TerminalObject c1)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj c1 a1
c1 a1 b1
a1 c1 a1 (TerminalObject c1)
-> c2 a2 (TerminalObject c2)
-> (:**:) c1 c2 (a1, a2) (TerminalObject c1, TerminalObject c2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> c2 a2 (TerminalObject c2)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj c2 a2
c2 a2 b2
a2
instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2) where
type TerminalObject (c1 :>>: c2) = I2 (TerminalObject c2)
terminalObject :: Obj (c1 :>>: c2) (TerminalObject (c1 :>>: c2))
terminalObject = Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 (TerminalObject c2))
(I2 (TerminalObject c2))
-> (:>>:) c1 c2 (I2 (TerminalObject c2)) (I2 (TerminalObject c2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c2 (TerminalObject c2) (TerminalObject c2)
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 (TerminalObject c2))
(I2 (TerminalObject c2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A c2 (TerminalObject c2) (TerminalObject c2)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject)
terminate :: Obj (c1 :>>: c2) a -> (:>>:) c1 c2 a (TerminalObject (c1 :>>: c2))
terminate (DC (I1A c a1 b1
a)) = Cograph
(Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 (TerminalObject c2))
-> (:>>:) c1 c2 (I1 a1) (I2 (TerminalObject c2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a1
-> c2 (TerminalObject c2) (TerminalObject c2)
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a1, TerminalObject c2))
-> Cograph
(Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 (TerminalObject c2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a1
c a1 b1
a c2 (TerminalObject c2) (TerminalObject c2)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
terminate (DC (I2A d a2 b2
a)) = Cograph
(Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 (TerminalObject c2))
-> (:>>:) c1 c2 (I2 a2) (I2 (TerminalObject c2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 (TerminalObject c2)
-> Cograph
(Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 (TerminalObject c2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (Obj d a2 -> d a2 (TerminalObject d)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj d a2
d a2 b2
a))
class Category k => HasInitialObject k where
type InitialObject k :: Kind k
initialObject :: Obj k (InitialObject k)
initialize :: Obj k a -> k (InitialObject k) a
type instance ColimitFam Void k f = InitialObject k
instance (Category k, HasInitialObject k) => HasColimits Void k where
colimit :: Obj (Nat Void k) f -> Cocone Void k f (ColimitFam Void k f)
colimit (Nat f
f f
_ forall z. Obj Void z -> Component f f z
_) = f
-> Const Void k (InitialObject k)
-> Nat Void k f (Const Void k (InitialObject k))
forall f g (d :: * -> * -> *).
(Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d,
Cod g ~ d) =>
f -> g -> Nat Void d f g
voidNat f
f (Obj k (InitialObject k) -> Const Void k (InitialObject k)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj k (InitialObject k)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)
colimitFactorizer :: Cocone Void k f n -> k (ColimitFam Void k f) n
colimitFactorizer = Obj k n -> k (InitialObject k) n
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize (Obj k n -> k (InitialObject k) n)
-> (Cocone Void k f n -> Obj k n)
-> Cocone Void k f n
-> k (InitialObject k) n
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cocone Void k f n -> Obj k n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex
data Zero
instance HasInitialObject (->) where
type InitialObject (->) = Zero
initialObject :: Obj (->) (InitialObject (->))
initialObject = \InitialObject (->)
x -> InitialObject (->)
x
initialize :: Obj (->) a -> InitialObject (->) -> a
initialize = Obj (->) a -> InitialObject (->) -> a
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize
instance HasInitialObject Cat where
type InitialObject Cat = Void
initialObject :: Obj Cat (InitialObject Cat)
initialObject = Id Void -> Cat (Dom (Id Void)) (Cod (Id Void))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Id Void
forall (k :: * -> * -> *). Id k
Id
initialize :: Obj Cat a -> Cat (InitialObject Cat) a
initialize (CatA ftag
_) = Magic a -> Cat (Dom (Magic a)) (Cod (Magic a))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Magic a
forall (k :: * -> * -> *). Magic k
Magic
instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d) where
type InitialObject (Nat c d) = Const c d (InitialObject d)
initialObject :: Obj (Nat c d) (InitialObject (Nat c d))
initialObject = Const c d (InitialObject d)
-> Nat
(Dom (Const c d (InitialObject d)))
(Cod (Const c d (InitialObject d)))
(Const c d (InitialObject d))
(Const c d (InitialObject d))
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (Obj d (InitialObject d) -> Const c d (InitialObject d)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj d (InitialObject d)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)
initialize :: Obj (Nat c d) a -> Nat c d (InitialObject (Nat c d)) a
initialize (Nat a
f a
_ forall z. Obj c z -> Component a a z
_) = Const c d (InitialObject d)
-> a
-> (forall z.
Obj c z -> Component (Const c d (InitialObject d)) a z)
-> Nat c d (Const c d (InitialObject d)) a
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj d (InitialObject d) -> Const c d (InitialObject d)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj d (InitialObject d)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject) a
f (Obj d (a :% z) -> d (InitialObject d) (a :% z)
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize (Obj d (a :% z) -> d (InitialObject d) (a :% z))
-> (c z z -> Obj d (a :% z))
-> c z z
-> d (InitialObject d) (a :% z)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (a
f a -> Dom a z z -> Cod a (a :% z) (a :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
%))
instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2) where
type InitialObject (c1 :**: c2) = (InitialObject c1, InitialObject c2)
initialObject :: Obj (c1 :**: c2) (InitialObject (c1 :**: c2))
initialObject = Obj c1 (InitialObject c1)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject Obj c1 (InitialObject c1)
-> c2 (InitialObject c2) (InitialObject c2)
-> (:**:)
c1
c2
(InitialObject c1, InitialObject c2)
(InitialObject c1, InitialObject c2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: c2 (InitialObject c2) (InitialObject c2)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject
initialize :: Obj (c1 :**: c2) a -> (:**:) c1 c2 (InitialObject (c1 :**: c2)) a
initialize (c1 a1 b1
a1 :**: c2 a2 b2
a2) = Obj c1 a1 -> c1 (InitialObject c1) a1
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj c1 a1
c1 a1 b1
a1 c1 (InitialObject c1) a1
-> c2 (InitialObject c2) a2
-> (:**:) c1 c2 (InitialObject c1, InitialObject c2) (a1, a2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> c2 (InitialObject c2) a2
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj c2 a2
c2 a2 b2
a2
instance HasInitialObject Unit where
type InitialObject Unit = ()
initialObject :: Obj Unit (InitialObject Unit)
initialObject = Obj Unit ()
Obj Unit (InitialObject Unit)
Unit
initialize :: Obj Unit a -> Unit (InitialObject Unit) a
initialize Obj Unit a
Unit = Obj Unit ()
Unit (InitialObject Unit) a
Unit
instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2) where
type InitialObject (c1 :>>: c2) = I1 (InitialObject c1)
initialObject :: Obj (c1 :>>: c2) (InitialObject (c1 :>>: c2))
initialObject = Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 (InitialObject c1))
(I1 (InitialObject c1))
-> (:>>:) c1 c2 (I1 (InitialObject c1)) (I1 (InitialObject c1))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c1 (InitialObject c1) (InitialObject c1)
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 (InitialObject c1))
(I1 (InitialObject c1))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A c1 (InitialObject c1) (InitialObject c1)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)
initialize :: Obj (c1 :>>: c2) a -> (:>>:) c1 c2 (InitialObject (c1 :>>: c2)) a
initialize (DC (I1A c a1 b1
a)) = Cograph
(Const (Op c1 :**: c2) (->) ()) (I1 (InitialObject c1)) (I1 a1)
-> (:>>:) c1 c2 (I1 (InitialObject c1)) (I1 a1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c (InitialObject c1) a1
-> Cograph
(Const (Op c1 :**: c2) (->) ()) (I1 (InitialObject c1)) (I1 a1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (Obj c a1 -> c (InitialObject c) a1
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj c a1
c a1 b1
a))
initialize (DC (I2A d a2 b2
a)) = Cograph
(Const (Op c1 :**: c2) (->) ()) (I1 (InitialObject c1)) (I2 a2)
-> (:>>:) c1 c2 (I1 (InitialObject c1)) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c1 (InitialObject c1) (InitialObject c1)
-> Obj d a2
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (InitialObject c1, a2))
-> Cograph
(Const (Op c1 :**: c2) (->) ()) (I1 (InitialObject c1)) (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 c1 (InitialObject c1) (InitialObject c1)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject Obj d a2
d a2 b2
a (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
class Category k => HasBinaryProducts k where
type BinaryProduct k (x :: Kind k) (y :: Kind k) :: Kind k
proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) y
(&&&) :: k a x -> k a y -> k a (BinaryProduct k x y)
(***) :: k a1 b1 -> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
k a1 b1
l *** k a2 b2
r = (k a1 b1
l k a1 b1
-> k (BinaryProduct k a1 a2) a1 -> k (BinaryProduct k a1 a2) b1
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k a1 -> Obj k a2 -> k (BinaryProduct k a1 a2) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 (k a1 b1 -> Obj k a1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a1 b1
l) (k a2 b2 -> Obj k a2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a2 b2
r)) k (BinaryProduct k a1 a2) b1
-> k (BinaryProduct k a1 a2) b2
-> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& (k a2 b2
r k a2 b2
-> k (BinaryProduct k a1 a2) a2 -> k (BinaryProduct k a1 a2) b2
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k a1 -> Obj k a2 -> k (BinaryProduct k a1 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 (k a1 b1 -> Obj k a1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a1 b1
l) (k a2 b2 -> Obj k a2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a2 b2
r))
type instance LimitFam (i :++: j) k f = BinaryProduct k
(LimitFam i k (f :.: Inj1 i j))
(LimitFam j k (f :.: Inj2 i j))
instance (HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (i :++: j) k where
limit :: Obj (Nat (i :++: j) k) f
-> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
limit = Obj (Nat (i :++: j) k) f
-> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
forall f.
Obj (Nat (i :++: j) k) f
-> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
limit'
where
limit' :: forall f. Obj (Nat (i :++: j) k) f -> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
limit' :: Obj (Nat (i :++: j) k) f
-> Cone (i :++: j) k f (LimitFam (i :++: j) k f)
limit' l :: Obj (Nat (i :++: j) k) f
l@Nat{} = Const
(i :++: j)
k
(BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
-> f
-> (forall z.
Obj (i :++: j) z
-> Component
(Const
(i :++: j)
k
(BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j))))
f
z)
-> Nat
(i :++: j)
k
(Const
(i :++: j)
k
(BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j))))
f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj
k
(BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
-> Const
(i :++: j)
k
(BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (Obj k (LimitFam i k (f :.: Inj1 i j))
x Obj k (LimitFam i k (f :.: Inj1 i j))
-> k (LimitFam j k (f :.: Inj2 i j))
(LimitFam j k (f :.: Inj2 i j))
-> Obj
k
(BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** k (LimitFam j k (f :.: Inj2 i j)) (LimitFam j k (f :.: Inj2 i j))
y)) (Obj (Nat (i :++: j) k) f -> f
forall (c :: * -> * -> *) (d :: * -> * -> *) f g. Nat c d f g -> f
srcF Obj (Nat (i :++: j) k) f
l) forall z.
Obj (i :++: j) z
-> Component (ConstF f (LimitFam (i :++: j) k f)) f z
forall z.
Obj (i :++: j) z
-> Component
(Const
(i :++: j)
k
(BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j))))
f
z
h
where
x :: Obj k (LimitFam i k (f :.: Inj1 i j))
x = Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
-> Obj k (LimitFam i k (f :.: Inj1 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
coneVertex Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
lim1
y :: k (LimitFam j k (f :.: Inj2 i j)) (LimitFam j k (f :.: Inj2 i j))
y = Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
-> k (LimitFam j k (f :.: Inj2 i j))
(LimitFam j k (f :.: Inj2 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
coneVertex Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
lim2
lim1 :: Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
lim1 = Obj (Nat i k) (f :.: Inj1 i j)
-> Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit (Obj (Nat (i :++: j) k) f
l Obj (Nat (i :++: j) k) f
-> Nat i (i :++: j) (Inj1 i j) (Inj1 i j)
-> Obj (Nat i k) (f :.: Inj1 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj1 i j
-> Nat (Dom (Inj1 i j)) (Cod (Inj1 i j)) (Inj1 i j) (Inj1 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj1 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1)
lim2 :: Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
lim2 = Obj (Nat j k) (f :.: Inj2 i j)
-> Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit (Obj (Nat (i :++: j) k) f
l Obj (Nat (i :++: j) k) f
-> Nat j (i :++: j) (Inj2 i j) (Inj2 i j)
-> Obj (Nat j k) (f :.: Inj2 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj2 i j
-> Nat (Dom (Inj2 i j)) (Cod (Inj2 i j)) (Inj2 i j) (Inj2 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj2 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2)
h :: Obj (i :++: j) z -> Component (ConstF f (LimitFam (i :++: j) k f)) f z
h :: Obj (i :++: j) z
-> Component (ConstF f (LimitFam (i :++: j) k f)) f z
h (I1 i a1 b1
n) = Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
lim1 Cone i k (f :.: Inj1 i j) (LimitFam i k (f :.: Inj1 i j))
-> i a1 b1
-> k (Const i k (LimitFam i k (f :.: Inj1 i j)) :% a1)
((f :.: Inj1 i j) :% b1)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! i a1 b1
n k (LimitFam i k (f :.: Inj1 i j)) (f :% I1 b1)
-> k (BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
(LimitFam i k (f :.: Inj1 i j))
-> k (BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
(f :% I1 b1)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k (LimitFam i k (f :.: Inj1 i j))
-> k (LimitFam j k (f :.: Inj2 i j))
(LimitFam j k (f :.: Inj2 i j))
-> k (BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
(LimitFam i k (f :.: Inj1 i j))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj k (LimitFam i k (f :.: Inj1 i j))
x k (LimitFam j k (f :.: Inj2 i j)) (LimitFam j k (f :.: Inj2 i j))
y
h (I2 j a2 b2
n) = Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
lim2 Cone j k (f :.: Inj2 i j) (LimitFam j k (f :.: Inj2 i j))
-> j a2 b2
-> k (Const j k (LimitFam j k (f :.: Inj2 i j)) :% a2)
((f :.: Inj2 i j) :% b2)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! j a2 b2
n k (LimitFam j k (f :.: Inj2 i j)) (f :% I2 b2)
-> k (BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
(LimitFam j k (f :.: Inj2 i j))
-> k (BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
(f :% I2 b2)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k (LimitFam i k (f :.: Inj1 i j))
-> k (LimitFam j k (f :.: Inj2 i j))
(LimitFam j k (f :.: Inj2 i j))
-> k (BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
(LimitFam j k (f :.: Inj2 i j))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj k (LimitFam i k (f :.: Inj1 i j))
x k (LimitFam j k (f :.: Inj2 i j)) (LimitFam j k (f :.: Inj2 i j))
y
limitFactorizer :: Cone (i :++: j) k f n -> k n (LimitFam (i :++: j) k f)
limitFactorizer Cone (i :++: j) k f n
c =
Cone i k (f :.: Inj1 i j) n -> k n (LimitFam i k (f :.: Inj1 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (Nat i k (Const (i :++: j) k n :.: Inj1 i j) (f :.: Inj1 i j)
-> Cone i k (f :.: Inj1 i j) n
forall (j :: * -> * -> *) (d :: * -> * -> *) (k :: * -> * -> *) x f
g.
Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g
constPostcompIn (Cone (i :++: j) k f n
c Cone (i :++: j) k f n
-> Nat i (i :++: j) (Inj1 i j) (Inj1 i j)
-> Nat i k (Const (i :++: j) k n :.: Inj1 i j) (f :.: Inj1 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj1 i j
-> Nat (Dom (Inj1 i j)) (Cod (Inj1 i j)) (Inj1 i j) (Inj1 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj1 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1))
k n (LimitFam i k (f :.: Inj1 i j))
-> k n (LimitFam j k (f :.: Inj2 i j))
-> k n
(BinaryProduct
k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&&
Cone j k (f :.: Inj2 i j) n -> k n (LimitFam j k (f :.: Inj2 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (Nat j k (Const (i :++: j) k n :.: Inj2 i j) (f :.: Inj2 i j)
-> Cone j k (f :.: Inj2 i j) n
forall (j :: * -> * -> *) (d :: * -> * -> *) (k :: * -> * -> *) x f
g.
Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g
constPostcompIn (Cone (i :++: j) k f n
c Cone (i :++: j) k f n
-> Nat j (i :++: j) (Inj2 i j) (Inj2 i j)
-> Nat j k (Const (i :++: j) k n :.: Inj2 i j) (f :.: Inj2 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj2 i j
-> Nat (Dom (Inj2 i j)) (Cod (Inj2 i j)) (Inj2 i j) (Inj2 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj2 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2))
instance HasBinaryProducts (->) where
type BinaryProduct (->) x y = (x, y)
proj1 :: Obj (->) x -> Obj (->) y -> BinaryProduct (->) x y -> x
proj1 Obj (->) x
_ Obj (->) y
_ = \(x, _) -> x
x
proj2 :: Obj (->) x -> Obj (->) y -> BinaryProduct (->) x y -> y
proj2 Obj (->) x
_ Obj (->) y
_ = \(_, y) -> y
y
a -> x
f &&& :: (a -> x) -> (a -> y) -> a -> BinaryProduct (->) x y
&&& a -> y
g = \a
x -> (a -> x
f a
x, a -> y
g a
x)
a1 -> b1
f *** :: (a1 -> b1)
-> (a2 -> b2)
-> BinaryProduct (->) a1 a2
-> BinaryProduct (->) b1 b2
*** a2 -> b2
g = \(x, y) -> (a1 -> b1
f a1
x, a2 -> b2
g a2
y)
instance HasBinaryProducts Cat where
type BinaryProduct Cat c1 c2 = c1 :**: c2
proj1 :: Obj Cat x -> Obj Cat y -> Cat (BinaryProduct Cat x y) x
proj1 (CatA ftag
_) (CatA ftag
_) = Proj1 x y -> Cat (Dom (Proj1 x y)) (Cod (Proj1 x y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Proj1 x y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Proj1 c1 c2
Proj1
proj2 :: Obj Cat x -> Obj Cat y -> Cat (BinaryProduct Cat x y) y
proj2 (CatA ftag
_) (CatA ftag
_) = Proj2 x y -> Cat (Dom (Proj2 x y)) (Cod (Proj2 x y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Proj2 x y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Proj2 c1 c2
Proj2
CatA ftag
f1 &&& :: Cat a x -> Cat a y -> Cat a (BinaryProduct Cat x y)
&&& CatA ftag
f2 = ((ftag :***: ftag) :.: DiagProd a)
-> Cat
(Dom ((ftag :***: ftag) :.: DiagProd a))
(Cod ((ftag :***: ftag) :.: DiagProd a))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA ((ftag
f1 ftag -> ftag -> ftag :***: ftag
forall f1 f2. (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2
:***: ftag
f2) (ftag :***: ftag) -> DiagProd a -> (ftag :***: ftag) :.: DiagProd a
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: DiagProd a
forall (k :: * -> * -> *). DiagProd k
DiagProd)
CatA ftag
f1 *** :: Cat a1 b1
-> Cat a2 b2
-> Cat (BinaryProduct Cat a1 a2) (BinaryProduct Cat b1 b2)
*** CatA ftag
f2 = (ftag :***: ftag)
-> Cat (Dom (ftag :***: ftag)) (Cod (ftag :***: ftag))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA (ftag
f1 ftag -> ftag -> ftag :***: ftag
forall f1 f2. (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2
:***: ftag
f2)
instance HasBinaryProducts Unit where
type BinaryProduct Unit () () = ()
proj1 :: Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) x
proj1 Obj Unit x
Unit Obj Unit y
Unit = Obj Unit ()
Unit (BinaryProduct Unit x y) x
Unit
proj2 :: Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) y
proj2 Obj Unit x
Unit Obj Unit y
Unit = Obj Unit ()
Unit (BinaryProduct Unit x y) y
Unit
Unit a x
Unit &&& :: Unit a x -> Unit a y -> Unit a (BinaryProduct Unit x y)
&&& Unit a y
Unit = Unit a (BinaryProduct Unit x y)
Obj Unit ()
Unit
Unit a1 b1
Unit *** :: Unit a1 b1
-> Unit a2 b2
-> Unit (BinaryProduct Unit a1 a2) (BinaryProduct Unit b1 b2)
*** Unit a2 b2
Unit = Obj Unit ()
Unit (BinaryProduct Unit a1 a2) (BinaryProduct Unit b1 b2)
Unit
instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where
type BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)
proj1 :: Obj (c1 :**: c2) x
-> Obj (c1 :**: c2) y
-> (:**:) c1 c2 (BinaryProduct (c1 :**: c2) x y) x
proj1 (c1 a1 b1
x1 :**: c2 a2 b2
x2) (c1 a1 b1
y1 :**: c2 a2 b2
y2) = Obj c1 a1 -> Obj c1 a1 -> c1 (BinaryProduct c1 a1 a1) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj c1 a1
c1 a1 b1
x1 Obj c1 a1
c1 a1 b1
y1 c1 (BinaryProduct c1 b1 b1) a1
-> c2 (BinaryProduct c2 b2 b2) a2
-> (:**:)
c1 c2 (BinaryProduct c1 b1 b1, BinaryProduct c2 b2 b2) (a1, a2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> Obj c2 a2 -> c2 (BinaryProduct c2 a2 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj c2 a2
c2 a2 b2
x2 Obj c2 a2
c2 a2 b2
y2
proj2 :: Obj (c1 :**: c2) x
-> Obj (c1 :**: c2) y
-> (:**:) c1 c2 (BinaryProduct (c1 :**: c2) x y) y
proj2 (c1 a1 b1
x1 :**: c2 a2 b2
x2) (c1 a1 b1
y1 :**: c2 a2 b2
y2) = Obj c1 a1 -> Obj c1 a1 -> c1 (BinaryProduct c1 a1 a1) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj c1 a1
c1 a1 b1
x1 Obj c1 a1
c1 a1 b1
y1 c1 (BinaryProduct c1 b1 b1) a1
-> c2 (BinaryProduct c2 b2 b2) a2
-> (:**:)
c1 c2 (BinaryProduct c1 b1 b1, BinaryProduct c2 b2 b2) (a1, a2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> Obj c2 a2 -> c2 (BinaryProduct c2 a2 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj c2 a2
c2 a2 b2
x2 Obj c2 a2
c2 a2 b2
y2
(c1 a1 b1
f1 :**: c2 a2 b2
f2) &&& :: (:**:) c1 c2 a x
-> (:**:) c1 c2 a y
-> (:**:) c1 c2 a (BinaryProduct (c1 :**: c2) x y)
&&& (c1 a1 b1
g1 :**: c2 a2 b2
g2) = (c1 a1 b1
f1 c1 a1 b1 -> c1 a1 b1 -> c1 a1 (BinaryProduct c1 b1 b1)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& c1 a1 b1
c1 a1 b1
g1) c1 a1 (BinaryProduct c1 b1 b1)
-> c2 a2 (BinaryProduct c2 b2 b2)
-> (:**:)
c1 c2 (a1, a2) (BinaryProduct c1 b1 b1, BinaryProduct c2 b2 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (c2 a2 b2
f2 c2 a2 b2 -> c2 a2 b2 -> c2 a2 (BinaryProduct c2 b2 b2)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& c2 a2 b2
c2 a2 b2
g2)
(c1 a1 b1
f1 :**: c2 a2 b2
f2) *** :: (:**:) c1 c2 a1 b1
-> (:**:) c1 c2 a2 b2
-> (:**:)
c1
c2
(BinaryProduct (c1 :**: c2) a1 a2)
(BinaryProduct (c1 :**: c2) b1 b2)
*** (c1 a1 b1
g1 :**: c2 a2 b2
g2) = (c1 a1 b1
f1 c1 a1 b1
-> c1 a1 b1 -> c1 (BinaryProduct c1 a1 a1) (BinaryProduct c1 b1 b1)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** c1 a1 b1
g1) c1 (BinaryProduct c1 a1 a1) (BinaryProduct c1 b1 b1)
-> c2 (BinaryProduct c2 a2 a2) (BinaryProduct c2 b2 b2)
-> (:**:)
c1
c2
(BinaryProduct c1 a1 a1, BinaryProduct c2 a2 a2)
(BinaryProduct c1 b1 b1, BinaryProduct c2 b2 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (c2 a2 b2
f2 c2 a2 b2
-> c2 a2 b2 -> c2 (BinaryProduct c2 a2 a2) (BinaryProduct c2 b2 b2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** c2 a2 b2
g2)
instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :>>: c2) where
type BinaryProduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryProduct c1 a b)
type BinaryProduct (c1 :>>: c2) (I1 a) (I2 b) = I1 a
type BinaryProduct (c1 :>>: c2) (I2 a) (I1 b) = I1 b
type BinaryProduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b)
proj1 :: Obj (c1 :>>: c2) x
-> Obj (c1 :>>: c2) y
-> (:>>:) c1 c2 (BinaryProduct (c1 :>>: c2) x y) x
proj1 (DC (I1A c a1 b1
a)) (DC (I1A c a1 b1
b)) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 (BinaryProduct c1 b1 b1))
(I1 a1)
-> (:>>:) c1 c2 (I1 (BinaryProduct c1 b1 b1)) (I1 a1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c (BinaryProduct c1 b1 b1) a1
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 (BinaryProduct c1 b1 b1))
(I1 a1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (Obj c a1 -> Obj c a1 -> c (BinaryProduct c a1 a1) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj c a1
c a1 b1
a Obj c a1
c a1 b1
b))
proj1 (DC (I1A c a1 b1
a)) (DC (I2A d a2 b2
_)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
-> (:>>:) c1 c2 (I1 a1) (I1 b1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 b1 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A c a1 b1
a)
proj1 (DC (I2A d a2 b2
a)) (DC (I1A c a1 b1
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
-> (:>>:) c1 c2 (I1 a1) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a1
-> Obj d a2
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a1, a2))
-> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a1
c a1 b1
b Obj d a2
d a2 b2
a (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
proj1 (DC (I2A d a2 b2
a)) (DC (I2A d a2 b2
b)) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 (BinaryProduct c2 b2 b2))
(I2 a2)
-> (:>>:) c1 c2 (I2 (BinaryProduct c2 b2 b2)) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d (BinaryProduct c2 b2 b2) a2
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 (BinaryProduct c2 b2 b2))
(I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (Obj d a2 -> Obj d a2 -> d (BinaryProduct d a2 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj d a2
d a2 b2
a Obj d a2
d a2 b2
b))
proj2 :: Obj (c1 :>>: c2) x
-> Obj (c1 :>>: c2) y
-> (:>>:) c1 c2 (BinaryProduct (c1 :>>: c2) x y) y
proj2 (DC (I1A c a1 b1
a)) (DC (I1A c a1 b1
b)) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 (BinaryProduct c1 b1 b1))
(I1 a1)
-> (:>>:) c1 c2 (I1 (BinaryProduct c1 b1 b1)) (I1 a1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c (BinaryProduct c1 b1 b1) a1
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 (BinaryProduct c1 b1 b1))
(I1 a1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (Obj c a1 -> Obj c a1 -> c (BinaryProduct c a1 a1) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj c a1
c a1 b1
a Obj c a1
c a1 b1
b))
proj2 (DC (I1A c a1 b1
a)) (DC (I2A d a2 b2
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
-> (:>>:) c1 c2 (I1 a1) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a1
-> Obj d a2
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a1, a2))
-> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a1
c a1 b1
a Obj d a2
d a2 b2
b (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
proj2 (DC (I2A d a2 b2
_)) (DC (I1A c a1 b1
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
-> (:>>:) c1 c2 (I1 a1) (I1 b1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 b1 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A c a1 b1
b)
proj2 (DC (I2A d a2 b2
a)) (DC (I2A d a2 b2
b)) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 (BinaryProduct c2 b2 b2))
(I2 a2)
-> (:>>:) c1 c2 (I2 (BinaryProduct c2 b2 b2)) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d (BinaryProduct c2 b2 b2) a2
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 (BinaryProduct c2 b2 b2))
(I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (Obj d a2 -> Obj d a2 -> d (BinaryProduct d a2 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj d a2
d a2 b2
a Obj d a2
d a2 b2
b))
DC (I1A c a1 b1
a) &&& :: (:>>:) c1 c2 a x
-> (:>>:) c1 c2 a y
-> (:>>:) c1 c2 a (BinaryProduct (c1 :>>: c2) x y)
&&& DC (I1A c a1 b1
b) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 a1)
(I1 (BinaryProduct c1 b1 b1))
-> (:>>:) c1 c2 (I1 a1) (I1 (BinaryProduct c1 b1 b1))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 (BinaryProduct c1 b1 b1)
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 a1)
(I1 (BinaryProduct c1 b1 b1))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (c a1 b1
a c a1 b1 -> c a1 b1 -> c a1 (BinaryProduct c b1 b1)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& c a1 b1
c a1 b1
b))
DC (I1A c a1 b1
a) &&& DC (I12 Obj c a
_ Obj d b
_ Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
-> (:>>:) c1 c2 (I1 a1) (I1 b1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 b1 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A c a1 b1
a)
DC (I12 Obj c a
_ Obj d b
_ Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) &&& DC (I1A c a1 b1
b) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
-> (:>>:) c1 c2 (I1 a1) (I1 b1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 b1 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A c a1 b1
b)
DC (I2A d a2 b2
a) &&& DC (I2A d a2 b2
b) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 a2)
(I2 (BinaryProduct c2 b2 b2))
-> (:>>:) c1 c2 (I2 a2) (I2 (BinaryProduct c2 b2 b2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 (BinaryProduct c2 b2 b2)
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 a2)
(I2 (BinaryProduct c2 b2 b2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (d a2 b2
a d a2 b2 -> d a2 b2 -> d a2 (BinaryProduct d b2 b2)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& d a2 b2
d a2 b2
b))
DC (I12 Obj c a
a Obj d b
b1 Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) &&& DC (I12 Obj c a
_ Obj d b
b2 Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) = Cograph
(Const (Op c1 :**: c2) (->) ()) (I1 a) (I2 (BinaryProduct c2 b b))
-> (:>>:) c1 c2 (I1 a) (I2 (BinaryProduct c2 b b))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a
-> Obj d (BinaryProduct c2 b b)
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a, BinaryProduct c2 b b))
-> Cograph
(Const (Op c1 :**: c2) (->) ()) (I1 a) (I2 (BinaryProduct c2 b b))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a
a (Obj d b
b1 Obj d b -> d b b -> d (BinaryProduct d b b) (BinaryProduct d b b)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** d b b
Obj d b
b2) (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
data ProductFunctor (k :: * -> * -> *) = ProductFunctor
instance HasBinaryProducts k => Functor (ProductFunctor k) where
type Dom (ProductFunctor k) = k :**: k
type Cod (ProductFunctor k) = k
type ProductFunctor k :% (a, b) = BinaryProduct k a b
ProductFunctor k
ProductFunctor % :: ProductFunctor k
-> Dom (ProductFunctor k) a b
-> Cod
(ProductFunctor k) (ProductFunctor k :% a) (ProductFunctor k :% b)
% (a1 :**: a2) = k a1 b1
a1 k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** k a2 b2
a2
prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
prodAdj :: Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
prodAdj = DiagProd k
-> ProductFunctor k
-> (forall a.
Obj k a -> Component (Id k) (ProductFunctor k :.: DiagProd k) a)
-> (forall a.
Obj (k :**: k) a
-> Component (DiagProd k :.: ProductFunctor k) (Id (k :**: k)) a)
-> Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionUnits DiagProd k
forall (k :: * -> * -> *). DiagProd k
DiagProd ProductFunctor k
forall (k :: * -> * -> *). ProductFunctor k
ProductFunctor (\Obj k a
x -> Obj k a
x Obj k a -> Obj k a -> k a (BinaryProduct k a a)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& Obj k a
x) (\(l :**: r) -> Obj k a1 -> Obj k a2 -> k (BinaryProduct k a1 a2) a1
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj k a1
k a1 b1
l Obj k a2
k a2 b2
r k (BinaryProduct k b1 b2) a1
-> k (BinaryProduct k b1 b2) a2
-> (:**:)
k k (BinaryProduct k b1 b2, BinaryProduct k b1 b2) (a1, a2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj k a1 -> Obj k a2 -> k (BinaryProduct k a1 a2) a2
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj k a1
k a1 b1
l Obj k a2
k a2 b2
r)
data p :*: q where
(:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q
instance (Category (Dom p), Category (Cod p)) => Functor (p :*: q) where
type Dom (p :*: q) = Dom p
type Cod (p :*: q) = Cod p
type (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a)
(p
p :*: q
q) % :: (p :*: q)
-> Dom (p :*: q) a b
-> Cod (p :*: q) ((p :*: q) :% a) ((p :*: q) :% b)
% Dom (p :*: q) a b
f = (p
p p -> Dom p a b -> Cod p (p :% a) (p :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom p a b
Dom (p :*: q) a b
f) Cod p (p :% a) (p :% b)
-> Cod p (q :% a) (q :% b)
-> Cod
p
(BinaryProduct (Cod p) (p :% a) (q :% a))
(BinaryProduct (Cod p) (p :% b) (q :% b))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** (q
q q -> Dom q a b -> Cod q (q :% a) (q :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom q a b
Dom (p :*: q) a b
f)
instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where
type BinaryProduct (Nat c d) x y = x :*: y
proj1 :: Obj (Nat c d) x
-> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) x
proj1 (Nat x
f x
_ forall z. Obj c z -> Component x x z
_) (Nat y
g y
_ forall z. Obj c z -> Component y y z
_) = (x :*: y)
-> x
-> (forall z. Obj c z -> Component (x :*: y) x z)
-> Nat c d (x :*: y) x
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (x
f x -> y -> x :*: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
HasBinaryProducts k) =>
p -> q -> p :*: q
:*: y
g) x
f (\Obj c z
z -> Obj d (x :% z)
-> Obj d (y :% z) -> d (BinaryProduct d (x :% z) (y :% z)) (x :% z)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 (x
f x -> Dom x z z -> Cod x (x :% z) (x :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom x z z
z) (y
g y -> Dom y z z -> Cod y (y :% z) (y :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom y z z
z))
proj2 :: Obj (Nat c d) x
-> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) y
proj2 (Nat x
f x
_ forall z. Obj c z -> Component x x z
_) (Nat y
g y
_ forall z. Obj c z -> Component y y z
_) = (x :*: y)
-> y
-> (forall z. Obj c z -> Component (x :*: y) y z)
-> Nat c d (x :*: y) y
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (x
f x -> y -> x :*: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
HasBinaryProducts k) =>
p -> q -> p :*: q
:*: y
g) y
g (\Obj c z
z -> Obj d (x :% z)
-> Obj d (y :% z) -> d (BinaryProduct d (x :% z) (y :% z)) (y :% z)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 (x
f x -> Dom x z z -> Cod x (x :% z) (x :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom x z z
z) (y
g y -> Dom y z z -> Cod y (y :% z) (y :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom y z z
z))
Nat a
a x
f forall z. Obj c z -> Component a x z
af &&& :: Nat c d a x
-> Nat c d a y -> Nat c d a (BinaryProduct (Nat c d) x y)
&&& Nat a
_ y
g forall z. Obj c z -> Component a y z
ag = a
-> (x :*: y)
-> (forall z. Obj c z -> Component a (x :*: y) z)
-> Nat c d a (x :*: y)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat a
a (x
f x -> y -> x :*: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
HasBinaryProducts k) =>
p -> q -> p :*: q
:*: y
g) (\Obj c z
z -> Obj c z -> Component a x z
forall z. Obj c z -> Component a x z
af Obj c z
z d (a :% z) (x :% z)
-> d (a :% z) (y :% z)
-> d (a :% z) (BinaryProduct d (x :% z) (y :% z))
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& Obj c z -> Component a y z
forall z. Obj c z -> Component a y z
ag Obj c z
z)
Nat a1
f1 b1
f2 forall z. Obj c z -> Component a1 b1 z
f *** :: Nat c d a1 b1
-> Nat c d a2 b2
-> Nat
c d (BinaryProduct (Nat c d) a1 a2) (BinaryProduct (Nat c d) b1 b2)
*** Nat a2
g1 b2
g2 forall z. Obj c z -> Component a2 b2 z
g = (a1 :*: a2)
-> (b1 :*: b2)
-> (forall z. Obj c z -> Component (a1 :*: a2) (b1 :*: b2) z)
-> Nat c d (a1 :*: a2) (b1 :*: b2)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (a1
f1 a1 -> a2 -> a1 :*: a2
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
HasBinaryProducts k) =>
p -> q -> p :*: q
:*: a2
g1) (b1
f2 b1 -> b2 -> b1 :*: b2
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
HasBinaryProducts k) =>
p -> q -> p :*: q
:*: b2
g2) (\Obj c z
z -> Obj c z -> Component a1 b1 z
forall z. Obj c z -> Component a1 b1 z
f Obj c z
z d (a1 :% z) (b1 :% z)
-> d (a2 :% z) (b2 :% z)
-> d (BinaryProduct d (a1 :% z) (a2 :% z))
(BinaryProduct d (b1 :% z) (b2 :% z))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj c z -> Component a2 b2 z
forall z. Obj c z -> Component a2 b2 z
g Obj c z
z)
class Category k => HasBinaryCoproducts k where
type BinaryCoproduct k (x :: Kind k) (y :: Kind k) :: Kind k
inj1 :: Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj2 :: Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
(|||) :: k x a -> k y a -> k (BinaryCoproduct k x y) a
(+++) :: k a1 b1 -> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
k a1 b1
l +++ k a2 b2
r = (Obj k b1 -> Obj k b2 -> k b1 (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 (k a1 b1 -> Obj k b1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a1 b1
l) (k a2 b2 -> Obj k b2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a2 b2
r) k b1 (BinaryCoproduct k b1 b2)
-> k a1 b1 -> k a1 (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k a1 b1
l) k a1 (BinaryCoproduct k b1 b2)
-> k a2 (BinaryCoproduct k b1 b2)
-> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| (Obj k b1 -> Obj k b2 -> k b2 (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 (k a1 b1 -> Obj k b1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a1 b1
l) (k a2 b2 -> Obj k b2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a2 b2
r) k b2 (BinaryCoproduct k b1 b2)
-> k a2 b2 -> k a2 (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k a2 b2
r)
type instance ColimitFam (i :++: j) k f = BinaryCoproduct k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j))
instance (HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (i :++: j) k where
colimit :: Obj (Nat (i :++: j) k) f
-> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
colimit = Obj (Nat (i :++: j) k) f
-> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
forall f.
Obj (Nat (i :++: j) k) f
-> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
colimit'
where
colimit' :: forall f. Obj (Nat (i :++: j) k) f -> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
colimit' :: Obj (Nat (i :++: j) k) f
-> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f)
colimit' l :: Obj (Nat (i :++: j) k) f
l@Nat{} = f
-> Const
(i :++: j)
k
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j)))
-> (forall z.
Obj (i :++: j) z
-> Component
f
(Const
(i :++: j)
k
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j))))
z)
-> Nat
(i :++: j)
k
f
(Const
(i :++: j)
k
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j))))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj (Nat (i :++: j) k) f -> f
forall (c :: * -> * -> *) (d :: * -> * -> *) f g. Nat c d f g -> f
srcF Obj (Nat (i :++: j) k) f
l) (Obj
k
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j)))
-> Const
(i :++: j)
k
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j)))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (Obj k (ColimitFam i k (f :.: Inj1 i j))
x Obj k (ColimitFam i k (f :.: Inj1 i j))
-> k (ColimitFam j k (f :.: Inj2 i j))
(ColimitFam j k (f :.: Inj2 i j))
-> Obj
k
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ k (ColimitFam j k (f :.: Inj2 i j))
(ColimitFam j k (f :.: Inj2 i j))
y)) forall z.
Obj (i :++: j) z
-> Component f (ConstF f (ColimitFam (i :++: j) k f)) z
forall z.
Obj (i :++: j) z
-> Component
f
(Const
(i :++: j)
k
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j))))
z
h
where
x :: Obj k (ColimitFam i k (f :.: Inj1 i j))
x = Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
-> Obj k (ColimitFam i k (f :.: Inj1 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
col1
y :: k (ColimitFam j k (f :.: Inj2 i j))
(ColimitFam j k (f :.: Inj2 i j))
y = Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
-> k (ColimitFam j k (f :.: Inj2 i j))
(ColimitFam j k (f :.: Inj2 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
col2
col1 :: Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
col1 = Obj (Nat i k) (f :.: Inj1 i j)
-> Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit (Obj (Nat (i :++: j) k) f
l Obj (Nat (i :++: j) k) f
-> Nat i (i :++: j) (Inj1 i j) (Inj1 i j)
-> Obj (Nat i k) (f :.: Inj1 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj1 i j
-> Nat (Dom (Inj1 i j)) (Cod (Inj1 i j)) (Inj1 i j) (Inj1 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj1 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1)
col2 :: Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
col2 = Obj (Nat j k) (f :.: Inj2 i j)
-> Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit (Obj (Nat (i :++: j) k) f
l Obj (Nat (i :++: j) k) f
-> Nat j (i :++: j) (Inj2 i j) (Inj2 i j)
-> Obj (Nat j k) (f :.: Inj2 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj2 i j
-> Nat (Dom (Inj2 i j)) (Cod (Inj2 i j)) (Inj2 i j) (Inj2 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj2 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2)
h :: Obj (i :++: j) z -> Component f (ConstF f (ColimitFam (i :++: j) k f)) z
h :: Obj (i :++: j) z
-> Component f (ConstF f (ColimitFam (i :++: j) k f)) z
h (I1 i a1 b1
n) = Obj k (ColimitFam i k (f :.: Inj1 i j))
-> k (ColimitFam j k (f :.: Inj2 i j))
(ColimitFam j k (f :.: Inj2 i j))
-> k (ColimitFam i k (f :.: Inj1 i j))
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj k (ColimitFam i k (f :.: Inj1 i j))
x k (ColimitFam j k (f :.: Inj2 i j))
(ColimitFam j k (f :.: Inj2 i j))
y k (ColimitFam i k (f :.: Inj1 i j))
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j)))
-> k (f :% I1 b1) (ColimitFam i k (f :.: Inj1 i j))
-> k (f :% I1 b1)
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
col1 Cocone i k (f :.: Inj1 i j) (ColimitFam i k (f :.: Inj1 i j))
-> i a1 b1
-> k ((f :.: Inj1 i j) :% a1)
(Const i k (ColimitFam i k (f :.: Inj1 i j)) :% b1)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! i a1 b1
n
h (I2 j a2 b2
n) = Obj k (ColimitFam i k (f :.: Inj1 i j))
-> k (ColimitFam j k (f :.: Inj2 i j))
(ColimitFam j k (f :.: Inj2 i j))
-> k (ColimitFam j k (f :.: Inj2 i j))
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj k (ColimitFam i k (f :.: Inj1 i j))
x k (ColimitFam j k (f :.: Inj2 i j))
(ColimitFam j k (f :.: Inj2 i j))
y k (ColimitFam j k (f :.: Inj2 i j))
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j)))
-> k (f :% I2 b2) (ColimitFam j k (f :.: Inj2 i j))
-> k (f :% I2 b2)
(BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j)))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
col2 Cocone j k (f :.: Inj2 i j) (ColimitFam j k (f :.: Inj2 i j))
-> j a2 b2
-> k ((f :.: Inj2 i j) :% a2)
(Const j k (ColimitFam j k (f :.: Inj2 i j)) :% b2)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! j a2 b2
n
colimitFactorizer :: Cocone (i :++: j) k f n -> k (ColimitFam (i :++: j) k f) n
colimitFactorizer Cocone (i :++: j) k f n
c =
Cocone i k (f :.: Inj1 i j) n
-> k (ColimitFam i k (f :.: Inj1 i j)) n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (Nat i k (f :.: Inj1 i j) (Const (i :++: j) k n :.: Inj1 i j)
-> Cocone i k (f :.: Inj1 i j) n
forall (j :: * -> * -> *) (d :: * -> * -> *) f (k :: * -> * -> *) x
g.
Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x)
constPostcompOut (Cocone (i :++: j) k f n
c Cocone (i :++: j) k f n
-> Nat i (i :++: j) (Inj1 i j) (Inj1 i j)
-> Nat i k (f :.: Inj1 i j) (Const (i :++: j) k n :.: Inj1 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj1 i j
-> Nat (Dom (Inj1 i j)) (Cod (Inj1 i j)) (Inj1 i j) (Inj1 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj1 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1))
k (ColimitFam i k (f :.: Inj1 i j)) n
-> k (ColimitFam j k (f :.: Inj2 i j)) n
-> k (BinaryCoproduct
k
(ColimitFam i k (f :.: Inj1 i j))
(ColimitFam j k (f :.: Inj2 i j)))
n
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
|||
Cocone j k (f :.: Inj2 i j) n
-> k (ColimitFam j k (f :.: Inj2 i j)) n
forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (Nat j k (f :.: Inj2 i j) (Const (i :++: j) k n :.: Inj2 i j)
-> Cocone j k (f :.: Inj2 i j) n
forall (j :: * -> * -> *) (d :: * -> * -> *) f (k :: * -> * -> *) x
g.
Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x)
constPostcompOut (Cocone (i :++: j) k f n
c Cocone (i :++: j) k f n
-> Nat j (i :++: j) (Inj2 i j) (Inj2 i j)
-> Nat j k (f :.: Inj2 i j) (Const (i :++: j) k n :.: Inj2 i j)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Inj2 i j
-> Nat (Dom (Inj2 i j)) (Cod (Inj2 i j)) (Inj2 i j) (Inj2 i j)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Inj2 i j
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2))
instance HasBinaryCoproducts Cat where
type BinaryCoproduct Cat c1 c2 = c1 :++: c2
inj1 :: Obj Cat x -> Obj Cat y -> Cat x (BinaryCoproduct Cat x y)
inj1 (CatA ftag
_) (CatA ftag
_) = Inj1 x y -> Cat (Dom (Inj1 x y)) (Cod (Inj1 x y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Inj1 x y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj1 c1 c2
Inj1
inj2 :: Obj Cat x -> Obj Cat y -> Cat y (BinaryCoproduct Cat x y)
inj2 (CatA ftag
_) (CatA ftag
_) = Inj2 x y -> Cat (Dom (Inj2 x y)) (Cod (Inj2 x y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Inj2 x y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Inj2 c1 c2
Inj2
CatA ftag
f1 ||| :: Cat x a -> Cat y a -> Cat (BinaryCoproduct Cat x y) a
||| CatA ftag
f2 = (CodiagCoprod a :.: (ftag :+++: ftag))
-> Cat
(Dom (CodiagCoprod a :.: (ftag :+++: ftag)))
(Cod (CodiagCoprod a :.: (ftag :+++: ftag)))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA (CodiagCoprod a
forall (k :: * -> * -> *). CodiagCoprod k
CodiagCoprod CodiagCoprod a
-> (ftag :+++: ftag) -> CodiagCoprod a :.: (ftag :+++: ftag)
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: (ftag
f1 ftag -> ftag -> ftag :+++: ftag
forall f1 f2. f1 -> f2 -> f1 :+++: f2
:+++: ftag
f2))
CatA ftag
f1 +++ :: Cat a1 b1
-> Cat a2 b2
-> Cat (BinaryCoproduct Cat a1 a2) (BinaryCoproduct Cat b1 b2)
+++ CatA ftag
f2 = (ftag :+++: ftag)
-> Cat (Dom (ftag :+++: ftag)) (Cod (ftag :+++: ftag))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA (ftag
f1 ftag -> ftag -> ftag :+++: ftag
forall f1 f2. f1 -> f2 -> f1 :+++: f2
:+++: ftag
f2)
instance HasBinaryCoproducts Unit where
type BinaryCoproduct Unit () () = ()
inj1 :: Obj Unit x -> Obj Unit y -> Unit x (BinaryCoproduct Unit x y)
inj1 Obj Unit x
Unit Obj Unit y
Unit = Unit x (BinaryCoproduct Unit x y)
Obj Unit ()
Unit
inj2 :: Obj Unit x -> Obj Unit y -> Unit y (BinaryCoproduct Unit x y)
inj2 Obj Unit x
Unit Obj Unit y
Unit = Unit y (BinaryCoproduct Unit x y)
Obj Unit ()
Unit
Unit x a
Unit ||| :: Unit x a -> Unit y a -> Unit (BinaryCoproduct Unit x y) a
||| Unit y a
Unit = Obj Unit ()
Unit (BinaryCoproduct Unit x y) a
Unit
Unit a1 b1
Unit +++ :: Unit a1 b1
-> Unit a2 b2
-> Unit (BinaryCoproduct Unit a1 a2) (BinaryCoproduct Unit b1 b2)
+++ Unit a2 b2
Unit = Obj Unit ()
Unit (BinaryCoproduct Unit a1 a2) (BinaryCoproduct Unit b1 b2)
Unit
instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where
type BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)
inj1 :: Obj (c1 :**: c2) x
-> Obj (c1 :**: c2) y
-> (:**:) c1 c2 x (BinaryCoproduct (c1 :**: c2) x y)
inj1 (c1 a1 b1
x1 :**: c2 a2 b2
x2) (c1 a1 b1
y1 :**: c2 a2 b2
y2) = Obj c1 a1 -> Obj c1 a1 -> c1 a1 (BinaryCoproduct c1 a1 a1)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj c1 a1
c1 a1 b1
x1 Obj c1 a1
c1 a1 b1
y1 c1 a1 (BinaryCoproduct c1 b1 b1)
-> c2 a2 (BinaryCoproduct c2 b2 b2)
-> (:**:)
c1 c2 (a1, a2) (BinaryCoproduct c1 b1 b1, BinaryCoproduct c2 b2 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> Obj c2 a2 -> c2 a2 (BinaryCoproduct c2 a2 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj c2 a2
c2 a2 b2
x2 Obj c2 a2
c2 a2 b2
y2
inj2 :: Obj (c1 :**: c2) x
-> Obj (c1 :**: c2) y
-> (:**:) c1 c2 y (BinaryCoproduct (c1 :**: c2) x y)
inj2 (c1 a1 b1
x1 :**: c2 a2 b2
x2) (c1 a1 b1
y1 :**: c2 a2 b2
y2) = Obj c1 a1 -> Obj c1 a1 -> c1 a1 (BinaryCoproduct c1 a1 a1)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj c1 a1
c1 a1 b1
x1 Obj c1 a1
c1 a1 b1
y1 c1 a1 (BinaryCoproduct c1 b1 b1)
-> c2 a2 (BinaryCoproduct c2 b2 b2)
-> (:**:)
c1 c2 (a1, a2) (BinaryCoproduct c1 b1 b1, BinaryCoproduct c2 b2 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 a2 -> Obj c2 a2 -> c2 a2 (BinaryCoproduct c2 a2 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj c2 a2
c2 a2 b2
x2 Obj c2 a2
c2 a2 b2
y2
(c1 a1 b1
f1 :**: c2 a2 b2
f2) ||| :: (:**:) c1 c2 x a
-> (:**:) c1 c2 y a
-> (:**:) c1 c2 (BinaryCoproduct (c1 :**: c2) x y) a
||| (c1 a1 b1
g1 :**: c2 a2 b2
g2) = (c1 a1 b1
f1 c1 a1 b1 -> c1 a1 b1 -> c1 (BinaryCoproduct c1 a1 a1) b1
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| c1 a1 b1
c1 a1 b1
g1) c1 (BinaryCoproduct c1 a1 a1) b1
-> c2 (BinaryCoproduct c2 a2 a2) b2
-> (:**:)
c1 c2 (BinaryCoproduct c1 a1 a1, BinaryCoproduct c2 a2 a2) (b1, b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (c2 a2 b2
f2 c2 a2 b2 -> c2 a2 b2 -> c2 (BinaryCoproduct c2 a2 a2) b2
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| c2 a2 b2
c2 a2 b2
g2)
(c1 a1 b1
f1 :**: c2 a2 b2
f2) +++ :: (:**:) c1 c2 a1 b1
-> (:**:) c1 c2 a2 b2
-> (:**:)
c1
c2
(BinaryCoproduct (c1 :**: c2) a1 a2)
(BinaryCoproduct (c1 :**: c2) b1 b2)
+++ (c1 a1 b1
g1 :**: c2 a2 b2
g2) = (c1 a1 b1
f1 c1 a1 b1
-> c1 a1 b1
-> c1 (BinaryCoproduct c1 a1 a1) (BinaryCoproduct c1 b1 b1)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ c1 a1 b1
g1) c1 (BinaryCoproduct c1 a1 a1) (BinaryCoproduct c1 b1 b1)
-> c2 (BinaryCoproduct c2 a2 a2) (BinaryCoproduct c2 b2 b2)
-> (:**:)
c1
c2
(BinaryCoproduct c1 a1 a1, BinaryCoproduct c2 a2 a2)
(BinaryCoproduct c1 b1 b1, BinaryCoproduct c2 b2 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (c2 a2 b2
f2 c2 a2 b2
-> c2 a2 b2
-> c2 (BinaryCoproduct c2 a2 a2) (BinaryCoproduct c2 b2 b2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ c2 a2 b2
g2)
instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :>>: c2) where
type BinaryCoproduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryCoproduct c1 a b)
type BinaryCoproduct (c1 :>>: c2) (I1 a) (I2 b) = I2 b
type BinaryCoproduct (c1 :>>: c2) (I2 a) (I1 b) = I2 a
type BinaryCoproduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryCoproduct c2 a b)
inj1 :: Obj (c1 :>>: c2) x
-> Obj (c1 :>>: c2) y
-> (:>>:) c1 c2 x (BinaryCoproduct (c1 :>>: c2) x y)
inj1 (DC (I1A c a1 b1
a)) (DC (I1A c a1 b1
b)) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 a1)
(I1 (BinaryCoproduct c1 b1 b1))
-> (:>>:) c1 c2 (I1 a1) (I1 (BinaryCoproduct c1 b1 b1))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 (BinaryCoproduct c1 b1 b1)
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 a1)
(I1 (BinaryCoproduct c1 b1 b1))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (Obj c a1 -> Obj c a1 -> c a1 (BinaryCoproduct c a1 a1)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj c a1
c a1 b1
a Obj c a1
c a1 b1
b))
inj1 (DC (I1A c a1 b1
a)) (DC (I2A d a2 b2
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
-> (:>>:) c1 c2 (I1 a1) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a1
-> Obj d a2
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a1, a2))
-> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a1
c a1 b1
a Obj d a2
d a2 b2
b (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
inj1 (DC (I2A d a2 b2
a)) (DC (I1A c a1 b1
_)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
-> (:>>:) c1 c2 (I2 a2) (I2 b2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 b2 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A d a2 b2
a)
inj1 (DC (I2A d a2 b2
a)) (DC (I2A d a2 b2
b)) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 a2)
(I2 (BinaryCoproduct c2 b2 b2))
-> (:>>:) c1 c2 (I2 a2) (I2 (BinaryCoproduct c2 b2 b2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 (BinaryCoproduct c2 b2 b2)
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 a2)
(I2 (BinaryCoproduct c2 b2 b2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (Obj d a2 -> Obj d a2 -> d a2 (BinaryCoproduct d a2 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj d a2
d a2 b2
a Obj d a2
d a2 b2
b))
inj2 :: Obj (c1 :>>: c2) x
-> Obj (c1 :>>: c2) y
-> (:>>:) c1 c2 y (BinaryCoproduct (c1 :>>: c2) x y)
inj2 (DC (I1A c a1 b1
a)) (DC (I1A c a1 b1
b)) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 a1)
(I1 (BinaryCoproduct c1 b1 b1))
-> (:>>:) c1 c2 (I1 a1) (I1 (BinaryCoproduct c1 b1 b1))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c a1 (BinaryCoproduct c1 b1 b1)
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 a1)
(I1 (BinaryCoproduct c1 b1 b1))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (Obj c a1 -> Obj c a1 -> c a1 (BinaryCoproduct c a1 a1)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj c a1
c a1 b1
a Obj c a1
c a1 b1
b))
inj2 (DC (I1A c a1 b1
_)) (DC (I2A d a2 b2
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
-> (:>>:) c1 c2 (I2 a2) (I2 b2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 b2 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A d a2 b2
b)
inj2 (DC (I2A d a2 b2
a)) (DC (I1A c a1 b1
b)) = Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
-> (:>>:) c1 c2 (I1 a1) (I2 a2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c a1
-> Obj d a2
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (a1, a2))
-> Cograph (Const (Op c1 :**: c2) (->) ()) (I1 a1) (I2 a2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 Obj c a1
c a1 b1
b Obj d a2
d a2 b2
a (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
inj2 (DC (I2A d a2 b2
a)) (DC (I2A d a2 b2
b)) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 a2)
(I2 (BinaryCoproduct c2 b2 b2))
-> (:>>:) c1 c2 (I2 a2) (I2 (BinaryCoproduct c2 b2 b2))
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 (BinaryCoproduct c2 b2 b2)
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 a2)
(I2 (BinaryCoproduct c2 b2 b2))
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (Obj d a2 -> Obj d a2 -> d a2 (BinaryCoproduct d a2 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj d a2
d a2 b2
a Obj d a2
d a2 b2
b))
DC (I1A c a1 b1
a) ||| :: (:>>:) c1 c2 x a
-> (:>>:) c1 c2 y a
-> (:>>:) c1 c2 (BinaryCoproduct (c1 :>>: c2) x y) a
||| DC (I1A c a1 b1
b) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 (BinaryCoproduct c1 a1 a1))
(I1 b1)
-> (:>>:) c1 c2 (I1 (BinaryCoproduct c1 a1 a1)) (I1 b1)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (c (BinaryCoproduct c1 a1 a1) b1
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 (BinaryCoproduct c1 a1 a1))
(I1 b1)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a1 b1.
(Dom f ~ (Op c :**: d)) =>
c a1 b1 -> Cograph f (I1 a1) (I1 b1)
I1A (c a1 b1
a c a1 b1 -> c a1 b1 -> c (BinaryCoproduct c a1 a1) b1
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| c a1 b1
c a1 b1
b))
DC (I2A d a2 b2
a) ||| DC (I12 Obj c a
_ Obj d b
_ Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) = Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
-> (:>>:) c1 c2 (I2 a2) (I2 b2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 b2 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A d a2 b2
a)
DC (I12 Obj c a
_ Obj d b
_ Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) ||| DC (I2A d a2 b2
b) = Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
-> (:>>:) c1 c2 (I2 a2) (I2 b2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d a2 b2 -> Cograph (Const (Op c1 :**: c2) (->) ()) (I2 a2) (I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A d a2 b2
b)
DC (I2A d a2 b2
a) ||| DC (I2A d a2 b2
b) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 (BinaryCoproduct c2 a2 a2))
(I2 b2)
-> (:>>:) c1 c2 (I2 (BinaryCoproduct c2 a2 a2)) (I2 b2)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (d (BinaryCoproduct c2 a2 a2) b2
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I2 (BinaryCoproduct c2 a2 a2))
(I2 b2)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a2 b2.
(Dom f ~ (Op c :**: d)) =>
d a2 b2 -> Cograph f (I2 a2) (I2 b2)
I2A (d a2 b2
a d a2 b2 -> d a2 b2 -> d (BinaryCoproduct d a2 a2) b2
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| d a2 b2
d a2 b2
b))
DC (I12 Obj c a
a1 Obj d b
b Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) ||| DC (I12 Obj c a
a2 Obj d b
_ Const (Op c1 :**: c2) (->) ()
_ Const (Op c1 :**: c2) (->) () :% (a, b)
_) = Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 (BinaryCoproduct c1 a a))
(I2 b)
-> (:>>:) c1 c2 (I1 (BinaryCoproduct c1 a a)) (I2 b)
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a b.
Cograph (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
DC (Obj c (BinaryCoproduct c1 a a)
-> Obj d b
-> Const (Op c1 :**: c2) (->) ()
-> (Const (Op c1 :**: c2) (->) () :% (BinaryCoproduct c1 a a, b))
-> Cograph
(Const (Op c1 :**: c2) (->) ())
(I1 (BinaryCoproduct c1 a a))
(I2 b)
forall f (c :: * -> * -> *) (d :: * -> * -> *) a b.
(Dom f ~ (Op c :**: d)) =>
Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph f (I1 a) (I2 b)
I12 (Obj c a
a1 Obj c a
-> c a a -> c (BinaryCoproduct c a a) (BinaryCoproduct c a a)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ c a a
Obj c a
a2) Obj d b
b (Obj (->) () -> Const (Op c1 :**: c2) (->) ()
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\() -> ())) ())
data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor
instance HasBinaryCoproducts k => Functor (CoproductFunctor k) where
type Dom (CoproductFunctor k) = k :**: k
type Cod (CoproductFunctor k) = k
type CoproductFunctor k :% (a, b) = BinaryCoproduct k a b
CoproductFunctor k
CoproductFunctor % :: CoproductFunctor k
-> Dom (CoproductFunctor k) a b
-> Cod
(CoproductFunctor k)
(CoproductFunctor k :% a)
(CoproductFunctor k :% b)
% (a1 :**: a2) = k a1 b1
a1 k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ k a2 b2
a2
coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)
coprodAdj :: Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)
coprodAdj = CoproductFunctor k
-> DiagProd k
-> (forall a.
Obj (k :**: k) a
-> Component (Id (k :**: k)) (DiagProd k :.: CoproductFunctor k) a)
-> (forall a.
Obj k a -> Component (CoproductFunctor k :.: DiagProd k) (Id k) a)
-> Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionUnits CoproductFunctor k
forall (k :: * -> * -> *). CoproductFunctor k
CoproductFunctor DiagProd k
forall (k :: * -> * -> *). DiagProd k
DiagProd (\(l :**: r) -> Obj k a1 -> Obj k a2 -> k a1 (BinaryCoproduct k a1 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj k a1
k a1 b1
l Obj k a2
k a2 b2
r k a1 (BinaryCoproduct k b1 b2)
-> k a2 (BinaryCoproduct k b1 b2)
-> (:**:)
k k (a1, a2) (BinaryCoproduct k b1 b2, BinaryCoproduct k b1 b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj k a1 -> Obj k a2 -> k a2 (BinaryCoproduct k a1 a2)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj k a1
k a1 b1
l Obj k a2
k a2 b2
r) (\Obj k a
x -> Obj k a
x Obj k a -> Obj k a -> k (BinaryCoproduct k a a) a
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| Obj k a
x)
data p :+: q where
(:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q
instance (Category (Dom p), Category (Cod p)) => Functor (p :+: q) where
type Dom (p :+: q) = Dom p
type Cod (p :+: q) = Cod p
type (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a)
(p
p :+: q
q) % :: (p :+: q)
-> Dom (p :+: q) a b
-> Cod (p :+: q) ((p :+: q) :% a) ((p :+: q) :% b)
% Dom (p :+: q) a b
f = (p
p p -> Dom p a b -> Cod p (p :% a) (p :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom p a b
Dom (p :+: q) a b
f) Cod p (p :% a) (p :% b)
-> Cod p (q :% a) (q :% b)
-> Cod
p
(BinaryCoproduct (Cod p) (p :% a) (q :% a))
(BinaryCoproduct (Cod p) (p :% b) (q :% b))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ (q
q q -> Dom q a b -> Cod q (q :% a) (q :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom q a b
Dom (p :+: q) a b
f)
instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where
type BinaryCoproduct (Nat c d) x y = x :+: y
inj1 :: Obj (Nat c d) x
-> Obj (Nat c d) y -> Nat c d x (BinaryCoproduct (Nat c d) x y)
inj1 (Nat x
f x
_ forall z. Obj c z -> Component x x z
_) (Nat y
g y
_ forall z. Obj c z -> Component y y z
_) = x
-> (x :+: y)
-> (forall z. Obj c z -> Component x (x :+: y) z)
-> Nat c d x (x :+: y)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat x
f (x
f x -> y -> x :+: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
HasBinaryCoproducts k) =>
p -> q -> p :+: q
:+: y
g) (\Obj c z
z -> Obj d (x :% z)
-> Obj d (y :% z)
-> d (x :% z) (BinaryCoproduct d (x :% z) (y :% z))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 (x
f x -> Dom x z z -> Cod x (x :% z) (x :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom x z z
z) (y
g y -> Dom y z z -> Cod y (y :% z) (y :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom y z z
z))
inj2 :: Obj (Nat c d) x
-> Obj (Nat c d) y -> Nat c d y (BinaryCoproduct (Nat c d) x y)
inj2 (Nat x
f x
_ forall z. Obj c z -> Component x x z
_) (Nat y
g y
_ forall z. Obj c z -> Component y y z
_) = y
-> (x :+: y)
-> (forall z. Obj c z -> Component y (x :+: y) z)
-> Nat c d y (x :+: y)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat y
g (x
f x -> y -> x :+: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
HasBinaryCoproducts k) =>
p -> q -> p :+: q
:+: y
g) (\Obj c z
z -> Obj d (x :% z)
-> Obj d (y :% z)
-> d (y :% z) (BinaryCoproduct d (x :% z) (y :% z))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 (x
f x -> Dom x z z -> Cod x (x :% z) (x :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom x z z
z) (y
g y -> Dom y z z -> Cod y (y :% z) (y :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom y z z
z))
Nat x
f a
a forall z. Obj c z -> Component x a z
fa ||| :: Nat c d x a
-> Nat c d y a -> Nat c d (BinaryCoproduct (Nat c d) x y) a
||| Nat y
g a
_ forall z. Obj c z -> Component y a z
ga = (x :+: y)
-> a
-> (forall z. Obj c z -> Component (x :+: y) a z)
-> Nat c d (x :+: y) a
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (x
f x -> y -> x :+: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
HasBinaryCoproducts k) =>
p -> q -> p :+: q
:+: y
g) a
a (\Obj c z
z -> Obj c z -> Component x a z
forall z. Obj c z -> Component x a z
fa Obj c z
z d (x :% z) (a :% z)
-> d (y :% z) (a :% z)
-> d (BinaryCoproduct d (x :% z) (y :% z)) (a :% z)
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| Obj c z -> Component y a z
forall z. Obj c z -> Component y a z
ga Obj c z
z)
Nat a1
f1 b1
f2 forall z. Obj c z -> Component a1 b1 z
f +++ :: Nat c d a1 b1
-> Nat c d a2 b2
-> Nat
c
d
(BinaryCoproduct (Nat c d) a1 a2)
(BinaryCoproduct (Nat c d) b1 b2)
+++ Nat a2
g1 b2
g2 forall z. Obj c z -> Component a2 b2 z
g = (a1 :+: a2)
-> (b1 :+: b2)
-> (forall z. Obj c z -> Component (a1 :+: a2) (b1 :+: b2) z)
-> Nat c d (a1 :+: a2) (b1 :+: b2)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (a1
f1 a1 -> a2 -> a1 :+: a2
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
HasBinaryCoproducts k) =>
p -> q -> p :+: q
:+: a2
g1) (b1
f2 b1 -> b2 -> b1 :+: b2
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
HasBinaryCoproducts k) =>
p -> q -> p :+: q
:+: b2
g2) (\Obj c z
z -> Obj c z -> Component a1 b1 z
forall z. Obj c z -> Component a1 b1 z
f Obj c z
z d (a1 :% z) (b1 :% z)
-> d (a2 :% z) (b2 :% z)
-> d (BinaryCoproduct d (a1 :% z) (a2 :% z))
(BinaryCoproduct d (b1 :% z) (b2 :% z))
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ Obj c z -> Component a2 b2 z
forall z. Obj c z -> Component a2 b2 z
g Obj c z
z)
instance HasInitialObject k => HasTerminalObject (Op k) where
type TerminalObject (Op k) = InitialObject k
terminalObject :: Obj (Op k) (TerminalObject (Op k))
terminalObject = k (InitialObject k) (InitialObject k)
-> Op k (InitialObject k) (InitialObject k)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k (InitialObject k) (InitialObject k)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject
terminate :: Obj (Op k) a -> Op k a (TerminalObject (Op k))
terminate (Op k a a
f) = k (InitialObject k) a -> Op k a (InitialObject k)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k a a -> k (InitialObject k) a
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize k a a
f)
instance HasTerminalObject k => HasInitialObject (Op k) where
type InitialObject (Op k) = TerminalObject k
initialObject :: Obj (Op k) (InitialObject (Op k))
initialObject = k (TerminalObject k) (TerminalObject k)
-> Op k (TerminalObject k) (TerminalObject k)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k (TerminalObject k) (TerminalObject k)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject
initialize :: Obj (Op k) a -> Op k (InitialObject (Op k)) a
initialize (Op k a a
f) = k a (TerminalObject k) -> Op k (TerminalObject k) a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k a a -> k a (TerminalObject k)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate k a a
f)
instance HasBinaryCoproducts k => HasBinaryProducts (Op k) where
type BinaryProduct (Op k) x y = BinaryCoproduct k x y
proj1 :: Obj (Op k) x -> Obj (Op k) y -> Op k (BinaryProduct (Op k) x y) x
proj1 (Op k x x
x) (Op k y y
y) = k x (BinaryCoproduct k x y) -> Op k (BinaryCoproduct k x y) x
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k x x -> k y y -> k x (BinaryCoproduct k x y)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 k x x
x k y y
y)
proj2 :: Obj (Op k) x -> Obj (Op k) y -> Op k (BinaryProduct (Op k) x y) y
proj2 (Op k x x
x) (Op k y y
y) = k y (BinaryCoproduct k x y) -> Op k (BinaryCoproduct k x y) y
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k x x -> k y y -> k y (BinaryCoproduct k x y)
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 k x x
x k y y
y)
Op k x a
f &&& :: Op k a x -> Op k a y -> Op k a (BinaryProduct (Op k) x y)
&&& Op k y a
g = k (BinaryCoproduct k x y) a -> Op k a (BinaryCoproduct k x y)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k x a
f k x a -> k y a -> k (BinaryCoproduct k x y) a
forall k (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| k y a
g)
Op k b1 a1
f *** :: Op k a1 b1
-> Op k a2 b2
-> Op k (BinaryProduct (Op k) a1 a2) (BinaryProduct (Op k) b1 b2)
*** Op k b2 a2
g = k (BinaryCoproduct k b1 b2) (BinaryCoproduct k a1 a2)
-> Op k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k b1 a1
f k b1 a1
-> k b2 a2 -> k (BinaryCoproduct k b1 b2) (BinaryCoproduct k a1 a2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ k b2 a2
g)
instance HasBinaryProducts k => HasBinaryCoproducts (Op k) where
type BinaryCoproduct (Op k) x y = BinaryProduct k x y
inj1 :: Obj (Op k) x -> Obj (Op k) y -> Op k x (BinaryCoproduct (Op k) x y)
inj1 (Op k x x
x) (Op k y y
y) = k (BinaryProduct k x y) x -> Op k x (BinaryProduct k x y)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k x x -> k y y -> k (BinaryProduct k x y) x
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 k x x
x k y y
y)
inj2 :: Obj (Op k) x -> Obj (Op k) y -> Op k y (BinaryCoproduct (Op k) x y)
inj2 (Op k x x
x) (Op k y y
y) = k (BinaryProduct k x y) y -> Op k y (BinaryProduct k x y)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k x x -> k y y -> k (BinaryProduct k x y) y
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 k x x
x k y y
y)
Op k a x
f ||| :: Op k x a -> Op k y a -> Op k (BinaryCoproduct (Op k) x y) a
||| Op k a y
g = k a (BinaryProduct k x y) -> Op k (BinaryProduct k x y) a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k a x
f k a x -> k a y -> k a (BinaryProduct k x y)
forall k (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& k a y
g)
Op k b1 a1
f +++ :: Op k a1 b1
-> Op k a2 b2
-> Op
k (BinaryCoproduct (Op k) a1 a2) (BinaryCoproduct (Op k) b1 b2)
+++ Op k b2 a2
g = k (BinaryProduct k b1 b2) (BinaryProduct k a1 a2)
-> Op k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k b1 a1
f k b1 a1
-> k b2 a2 -> k (BinaryProduct k b1 b2) (BinaryProduct k a1 a2)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
(b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** k b2 a2
g)
type instance LimitFam Unit k f = f :% ()
instance Category k => HasLimits Unit k where
limit :: Obj (Nat Unit k) f -> Cone Unit k f (LimitFam Unit k f)
limit (Nat f
f f
_ forall z. Obj Unit z -> Component f f z
_) = Const Unit k (f :% ())
-> f
-> (forall z. Obj Unit z -> Component (Const Unit k (f :% ())) f z)
-> Nat Unit k (Const Unit k (f :% ())) f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj k (f :% ()) -> Const Unit k (f :% ())
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f -> Dom f () () -> Cod f (f :% ()) (f :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f () ()
Obj Unit ()
Unit)) f
f (\Obj Unit z
Unit -> f
f f -> Dom f () () -> Cod f (f :% ()) (f :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f () ()
Obj Unit ()
Unit)
limitFactorizer :: Cone Unit k f n -> k n (LimitFam Unit k f)
limitFactorizer Cone Unit k f n
n = Cone Unit k f n
n Cone Unit k f n
-> Obj Unit () -> k (Const Unit k n :% ()) (f :% ())
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj Unit ()
Unit
type instance LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)
instance (HasInitialObject (i :>>: j), Category i, Category j, Category k) => HasLimits (i :>>: j) k where
limit :: Obj (Nat (i :>>: j) k) f
-> Cone (i :>>: j) k f (LimitFam (i :>>: j) k f)
limit (Nat f
f f
_ forall z. Obj (i :>>: j) z -> Component f f z
_) = Const (i :>>: j) k (f :% I1 (InitialObject i))
-> f
-> (forall z.
Obj (i :>>: j) z
-> Component (Const (i :>>: j) k (f :% I1 (InitialObject i))) f z)
-> Nat
(i :>>: j) k (Const (i :>>: j) k (f :% I1 (InitialObject i))) f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj k (f :% I1 (InitialObject i))
-> Const (i :>>: j) k (f :% I1 (InitialObject i))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f
-> Dom f (I1 (InitialObject i)) (I1 (InitialObject i))
-> Cod f (f :% I1 (InitialObject i)) (f :% I1 (InitialObject i))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f (I1 (InitialObject i)) (I1 (InitialObject i))
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject)) f
f (\Obj (i :>>: j) z
z -> f
f f
-> Dom f (I1 (InitialObject i)) z
-> Cod f (f :% I1 (InitialObject i)) (f :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (i :>>: j) z -> (:>>:) i j (InitialObject (i :>>: j)) z
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj (i :>>: j) z
z)
limitFactorizer :: Cone (i :>>: j) k f n -> k n (LimitFam (i :>>: j) k f)
limitFactorizer Cone (i :>>: j) k f n
n = Cone (i :>>: j) k f n
n Cone (i :>>: j) k f n
-> (:>>:) i j (I1 (InitialObject i)) (I1 (InitialObject i))
-> k (Const (i :>>: j) k n :% I1 (InitialObject i))
(f :% I1 (InitialObject i))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! (:>>:) i j (I1 (InitialObject i)) (I1 (InitialObject i))
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject
type instance ColimitFam Unit k f = f :% ()
instance Category k => HasColimits Unit k where
colimit :: Obj (Nat Unit k) f -> Cocone Unit k f (ColimitFam Unit k f)
colimit (Nat f
f f
_ forall z. Obj Unit z -> Component f f z
_) = f
-> Const Unit k (f :% ())
-> (forall z. Obj Unit z -> Component f (Const Unit k (f :% ())) z)
-> Nat Unit k f (Const Unit k (f :% ()))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (Obj k (f :% ()) -> Const Unit k (f :% ())
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f -> Dom f () () -> Cod f (f :% ()) (f :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f () ()
Obj Unit ()
Unit)) (\Obj Unit z
Unit -> f
f f -> Dom f () () -> Cod f (f :% ()) (f :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f () ()
Obj Unit ()
Unit)
colimitFactorizer :: Cocone Unit k f n -> k (ColimitFam Unit k f) n
colimitFactorizer Cocone Unit k f n
n = Cocone Unit k f n
n Cocone Unit k f n
-> Obj Unit () -> k (f :% ()) (Const Unit k n :% ())
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj Unit ()
Unit
type instance ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)
instance (HasTerminalObject (i :>>: j), Category i, Category j, Category k) => HasColimits (i :>>: j) k where
colimit :: Obj (Nat (i :>>: j) k) f
-> Cocone (i :>>: j) k f (ColimitFam (i :>>: j) k f)
colimit (Nat f
f f
_ forall z. Obj (i :>>: j) z -> Component f f z
_) = f
-> Const (i :>>: j) k (f :% I2 (TerminalObject j))
-> (forall z.
Obj (i :>>: j) z
-> Component f (Const (i :>>: j) k (f :% I2 (TerminalObject j))) z)
-> Nat
(i :>>: j) k f (Const (i :>>: j) k (f :% I2 (TerminalObject j)))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (Obj k (f :% I2 (TerminalObject j))
-> Const (i :>>: j) k (f :% I2 (TerminalObject j))
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f
-> Dom f (I2 (TerminalObject j)) (I2 (TerminalObject j))
-> Cod f (f :% I2 (TerminalObject j)) (f :% I2 (TerminalObject j))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f (I2 (TerminalObject j)) (I2 (TerminalObject j))
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject)) (\Obj (i :>>: j) z
z -> f
f f
-> Dom f z (I2 (TerminalObject j))
-> Cod f (f :% z) (f :% I2 (TerminalObject j))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (i :>>: j) z -> (:>>:) i j z (TerminalObject (i :>>: j))
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj (i :>>: j) z
z)
colimitFactorizer :: Cocone (i :>>: j) k f n -> k (ColimitFam (i :>>: j) k f) n
colimitFactorizer Cocone (i :>>: j) k f n
n = Cocone (i :>>: j) k f n
n Cocone (i :>>: j) k f n
-> (:>>:) i j (I2 (TerminalObject j)) (I2 (TerminalObject j))
-> k (f :% I2 (TerminalObject j))
(Const (i :>>: j) k n :% I2 (TerminalObject j))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! (:>>:) i j (I2 (TerminalObject j)) (I2 (TerminalObject j))
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject
data ForAll f = ForAll (forall a. Obj (->) a -> f :% a)
type instance LimitFam (->) (->) f = ForAll f
instance HasLimits (->) (->) where
limit :: Obj (Nat (->) (->)) f -> Cone (->) (->) f (LimitFam (->) (->) f)
limit (Nat f
f f
_ forall z. Obj (->) z -> Component f f z
_) = Const (->) (->) (ForAll f)
-> f
-> (forall z.
Obj (->) z -> Component (Const (->) (->) (ForAll f)) f z)
-> Nat (->) (->) (Const (->) (->) (ForAll f)) f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj (->) (ForAll f) -> Const (->) (->) (ForAll f)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\ForAll f
x -> ForAll f
x)) f
f (\Obj (->) z
a (ForAll forall a. Obj (->) a -> f :% a
g) -> Obj (->) z -> f :% z
forall a. Obj (->) a -> f :% a
g Obj (->) z
a)
limitFactorizer :: Cone (->) (->) f n -> n -> LimitFam (->) (->) f
limitFactorizer Cone (->) (->) f n
n = \n
z -> (forall a. Obj (->) a -> f :% a) -> ForAll f
forall f. (forall a. Obj (->) a -> f :% a) -> ForAll f
ForAll (\Obj (->) a
a -> (Cone (->) (->) f n
n Cone (->) (->) f n
-> Obj (->) a -> (Const (->) (->) n :% a) -> f :% a
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj (->) a
a) n
z)
data Exists f = forall a. Exists (Obj (->) a) (f :% a)
type instance ColimitFam (->) (->) f = Exists f
instance HasColimits (->) (->) where
colimit :: Obj (Nat (->) (->)) f
-> Cocone (->) (->) f (ColimitFam (->) (->) f)
colimit (Nat f
f f
_ forall z. Obj (->) z -> Component f f z
_) = f
-> Const (->) (->) (Exists f)
-> (forall z.
Obj (->) z -> Component f (Const (->) (->) (Exists f)) z)
-> Nat (->) (->) f (Const (->) (->) (Exists f))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (Obj (->) (Exists f) -> Const (->) (->) (Exists f)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (\Exists f
x -> Exists f
x)) forall z. Obj (->) z -> Component f (Const (->) (->) (Exists f)) z
forall f a. Obj (->) a -> (f :% a) -> Exists f
Exists
colimitFactorizer :: Cocone (->) (->) f n -> ColimitFam (->) (->) f -> n
colimitFactorizer Cocone (->) (->) f n
n = \(Exists a fa) -> (Cocone (->) (->) f n
n Cocone (->) (->) f n
-> (a -> a) -> (f :% a) -> Const (->) (->) n :% a
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! a -> a
a) f :% a
fa