{-# LANGUAGE
TypeOperators,
TypeFamilies,
GADTs,
PolyKinds,
DataKinds,
Rank2Types,
PatternSynonyms,
ScopedTypeVariables,
UndecidableInstances,
TypeSynonymInstances,
FlexibleInstances,
NoImplicitPrelude #-}
module Data.Category.CartesianClosed where
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Product
import Data.Category.Limit
import Data.Category.Adjunction
import Data.Category.Monoidal as M
import Data.Category.Yoneda
import qualified Data.Category.Unit as U
class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where
type Exponential k (y :: Kind k) (z :: Kind k) :: Kind k
apply :: Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
tuple :: Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
(^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
data ExpFunctor (k :: * -> * -> *) = ExpFunctor
instance CartesianClosed k => Functor (ExpFunctor k) where
type Dom (ExpFunctor k) = Op k :**: k
type Cod (ExpFunctor k) = k
type ExpFunctor k :% (y, z) = Exponential k y z
ExpFunctor k
ExpFunctor % :: ExpFunctor k
-> Dom (ExpFunctor k) a b
-> Cod (ExpFunctor k) (ExpFunctor k :% a) (ExpFunctor k :% b)
% (Op y :**: z) = k a2 b2
z k a2 b2 -> k b1 a1 -> k (Exponential k a1 a2) (Exponential k b1 b2)
forall k (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
(y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ k b1 a1
y
flip :: CartesianClosed k => Obj k a -> Obj k b -> Obj k c -> k (Exponential k a (Exponential k b c)) (Exponential k b (Exponential k a c))
flip :: Obj k a
-> Obj k b
-> Obj k c
-> k (Exponential k a (Exponential k b c))
(Exponential k b (Exponential k a c))
flip Obj k a
a Obj k b
b Obj k c
c = Obj k a
-> Obj k b
-> Obj k c
-> k (Exponential k a (Exponential k b c))
(Exponential k b (Exponential k a c))
forall k (k :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianClosed k =>
Obj k a
-> Obj k b
-> Obj k c
-> k (Exponential k a (Exponential k b c))
(Exponential k b (Exponential k a c))
flip Obj k a
a Obj k b
b Obj k c
c
instance CartesianClosed (->) where
type Exponential (->) y z = y -> z
apply :: Obj (->) y
-> Obj (->) z -> BinaryProduct (->) (Exponential (->) y z) y -> z
apply Obj (->) y
_ Obj (->) z
_ (f, y) = y -> z
f y
y
tuple :: Obj (->) y
-> Obj (->) z -> z -> Exponential (->) y (BinaryProduct (->) z y)
tuple Obj (->) y
_ Obj (->) z
_ z
z = \y
y -> (z
z, y
y)
z1 -> z2
f ^^^ :: (z1 -> z2)
-> (y2 -> y1) -> Exponential (->) y1 z1 -> Exponential (->) y2 z2
^^^ y2 -> y1
h = \Exponential (->) y1 z1
g -> z1 -> z2
f (z1 -> z2) -> (y2 -> z1) -> y2 -> z2
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Exponential (->) y1 z1
y1 -> z1
g (y1 -> z1) -> (y2 -> y1) -> y2 -> z1
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. y2 -> y1
h
instance CartesianClosed U.Unit where
type Exponential U.Unit () () = ()
apply :: Obj Unit y
-> Obj Unit z
-> Unit (BinaryProduct Unit (Exponential Unit y z) y) z
apply Obj Unit y
U.Unit Obj Unit z
U.Unit = Unit () ()
Unit (BinaryProduct Unit (Exponential Unit y z) y) z
U.Unit
tuple :: Obj Unit y
-> Obj Unit z
-> Unit z (Exponential Unit y (BinaryProduct Unit z y))
tuple Obj Unit y
U.Unit Obj Unit z
U.Unit = Unit z (Exponential Unit y (BinaryProduct Unit z y))
Unit () ()
U.Unit
Unit z1 z2
U.Unit ^^^ :: Unit z1 z2
-> Unit y2 y1
-> Unit (Exponential Unit y1 z1) (Exponential Unit y2 z2)
^^^ Unit y2 y1
U.Unit = Unit () ()
Unit (Exponential Unit y1 z1) (Exponential Unit y2 z2)
U.Unit
instance CartesianClosed Cat where
type Exponential Cat c d = Nat c d
apply :: Obj Cat y
-> Obj Cat z -> Cat (BinaryProduct Cat (Exponential Cat y z) y) z
apply CatA{} CatA{} = Apply z y -> Cat (Dom (Apply z y)) (Cod (Apply z y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Apply z y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Apply c1 c2
Apply
tuple :: Obj Cat y
-> Obj Cat z -> Cat z (Exponential Cat y (BinaryProduct Cat z y))
tuple CatA{} CatA{} = Tuple z y -> Cat (Dom (Tuple z y)) (Cod (Tuple z y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Tuple z y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Tuple c1 c2
Tuple
CatA ftag
f ^^^ :: Cat z1 z2
-> Cat y2 y1 -> Cat (Exponential Cat y1 z1) (Exponential Cat y2 z2)
^^^ CatA ftag
h = Wrap ftag ftag -> Cat (Dom (Wrap ftag ftag)) (Cod (Wrap ftag ftag))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA (ftag -> ftag -> Wrap ftag ftag
forall f h. f -> h -> Wrap f h
Wrap ftag
f ftag
h)
type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite
( ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y
:.: YonedaEmbedding k
)
pattern PshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z
pattern $bPshExponential :: Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
$mPshExponential :: forall r (k :: * -> * -> *) y z.
Category k =>
PShExponential k y z
-> (Obj (Presheaves k) y -> Obj (Presheaves k) z -> r)
-> (Void# -> r)
-> r
PshExponential y z = Hom_X z :.: Opposite (ProductFunctor :.: Tuple2 y :.: YonedaEmbedding)
instance Category k => CartesianClosed (Presheaves k) where
type Exponential (Presheaves k) y z = PShExponential k y z
apply :: Obj (Presheaves k) y
-> Obj (Presheaves k) z
-> Presheaves
k
(BinaryProduct (Presheaves k) (Exponential (Presheaves k) y z) y)
z
apply yn :: Obj (Presheaves k) y
yn@(Nat y
y y
_ forall z. Obj (Op k) z -> Component y y z
_) zn :: Obj (Presheaves k) z
zn@(Nat z
z z
_ forall z. Obj (Op k) z -> Component z z z
_) = (((Presheaves k :-*: z)
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
:*: y)
-> z
-> (forall z.
Obj (Op k) z
-> Component
(((Presheaves k :-*: z)
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
:*: y)
z
z)
-> Nat
(Op k)
(->)
(((Presheaves k :-*: z)
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
:*: y)
z
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential Obj (Presheaves k) y
yn Obj (Presheaves k) z
zn ((Presheaves k :-*: z)
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
-> y
-> ((Presheaves k :-*: z)
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
:*: 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
y) z
z (\(Op i) (Nat
(Op k)
(->)
((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y)
z
n, y :% z
yi) -> (Nat
(Op k)
(->)
((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y)
z
n Nat
(Op k)
(->)
((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y)
z
-> Obj (Op k) z
-> (((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y)
:% z)
-> z :% 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)
! k z z -> Obj (Op k) z
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k z z
i) (k z z
i, y :% z
yi))
tuple :: Obj (Presheaves k) y
-> Obj (Presheaves k) z
-> Presheaves
k
z
(Exponential (Presheaves k) y (BinaryProduct (Presheaves k) z y))
tuple Obj (Presheaves k) y
yn zn :: Obj (Presheaves k) z
zn@(Nat z
z z
_ forall z. Obj (Op k) z -> Component z z z
_) = z
-> ((Presheaves k :-*: (z :*: y))
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
-> (forall z.
Obj (Op k) z
-> Component
z
((Presheaves k :-*: (z :*: y))
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
z)
-> Nat
(Op k)
(->)
z
((Presheaves k :-*: (z :*: y))
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
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 z
z (Obj (Presheaves k) y
-> Obj (Presheaves k) (z :*: y) -> PShExponential k y (z :*: y)
forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential Obj (Presheaves k) y
yn (Obj (Presheaves k) z
zn Obj (Presheaves k) z
-> Obj (Presheaves k) y
-> Nat
(Op k)
(->)
(BinaryProduct (Presheaves k) z y)
(BinaryProduct (Presheaves k) z y)
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 (Presheaves k) y
yn)) (\(Op i) z :% z
zi -> ((k :-*: z)
-> z
-> (forall z. Obj (Op k) z -> Component (k :-*: z) z z)
-> Nat (Op k) (->) (k :-*: z) z
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj k z -> k :-*: z
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X Obj k z
i) z
z (\Obj (Op k) z
_ k z z
j2i -> (z
z z -> Dom z z z -> Cod z (z :% z) (z :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k z z -> Op k z z
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k z z
j2i) z :% z
zi) Nat (Op k) (->) (k :-*: z) z
-> Obj (Presheaves k) y
-> Nat
(Op k)
(->)
(BinaryProduct (Presheaves k) (k :-*: z) y)
(BinaryProduct (Presheaves k) z y)
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 (Presheaves k) y
yn))
Presheaves k z1 z2
zn ^^^ :: Presheaves k z1 z2
-> Presheaves k y2 y1
-> Presheaves
k
(Exponential (Presheaves k) y1 z1)
(Exponential (Presheaves k) y2 z2)
^^^ Presheaves k y2 y1
yn = ((Presheaves k :-*: z1)
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y1)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
-> ((Presheaves k :-*: z2)
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y2)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
-> (forall z.
Obj (Op k) z
-> Component
((Presheaves k :-*: z1)
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y1)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
((Presheaves k :-*: z2)
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y2)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
z)
-> Nat
(Op k)
(->)
((Presheaves k :-*: z1)
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y1)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
((Presheaves k :-*: z2)
:.: Opposite
((ProductFunctor (Presheaves k)
:.: Tuple2 (Presheaves k) (Presheaves k) y2)
:.: ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: Tuple1
(Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: Tuple1
(Nat (k :**: Op k) (Op k :**: k))
(Nat (Op k) (k :**: Op k))
(Swap k (Op k)))
:.: Tuple k (Op k)))))
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 (Presheaves k) y1
-> Obj (Presheaves k) z1 -> PShExponential k y1 z1
forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential (Presheaves k y2 y1 -> Obj (Presheaves k) y1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Presheaves k y2 y1
yn) (Presheaves k z1 z2 -> Obj (Presheaves k) z1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Presheaves k z1 z2
zn)) (Obj (Presheaves k) y2
-> Obj (Presheaves k) z2 -> PShExponential k y2 z2
forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential (Presheaves k y2 y1 -> Obj (Presheaves k) y2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Presheaves k y2 y1
yn) (Presheaves k z1 z2 -> Obj (Presheaves k) z2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Presheaves k z1 z2
zn)) (\(Op i) Nat
(Op k)
(->)
((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y1)
z1
n -> Presheaves k z1 z2
zn Presheaves k z1 z2
-> Nat
(Op k)
(->)
((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y2)
z1
-> Nat
(Op k)
(->)
((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y2)
z2
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Nat
(Op k)
(->)
((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y1)
z1
n Nat
(Op k)
(->)
((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y1)
z1
-> Nat
(Op k)
(->)
((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y2)
((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y1)
-> Nat
(Op k)
(->)
((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
:*: y2)
z1
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. ((Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
-> Nat
(Dom
(Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k)))))
(Cod
(Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k)))))
(Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
(Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (Obj k z
-> Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k)))
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X Obj k z
i) Nat
(Op k)
(->)
(Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
(Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
-> Presheaves k y2 y1
-> Nat
(Op k)
(->)
(BinaryProduct
(Presheaves k)
(Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
y2)
(BinaryProduct
(Presheaves k)
(Hom k
:.: (Swap k (Op k)
:.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
y1)
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)
*** Presheaves k y2 y1
yn))
curryAdj :: CartesianClosed k
=> Obj k y
-> Adjunction k k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj :: Obj k y
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k y
y = (ProductFunctor k :.: Tuple2 k k y)
-> (ExpFunctor k :.: Tuple1 (Op k) k y)
-> (forall a.
Obj k a
-> Component
(Id k)
((ExpFunctor k :.: Tuple1 (Op k) k y)
:.: (ProductFunctor k :.: Tuple2 k k y))
a)
-> (forall a.
Obj k a
-> Component
((ProductFunctor k :.: Tuple2 k k y)
:.: (ExpFunctor k :.: Tuple1 (Op k) k y))
(Id k)
a)
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
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 (ProductFunctor k
forall (k :: * -> * -> *). ProductFunctor k
ProductFunctor ProductFunctor k
-> Tuple2 k k y -> ProductFunctor k :.: Tuple2 k k y
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: Obj k y -> Tuple2 k k y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c2 a -> Tuple2 c1 c2 a
Tuple2 Obj k y
y) (ExpFunctor k
forall (k :: * -> * -> *). ExpFunctor k
ExpFunctor ExpFunctor k
-> Tuple1 (Op k) k y -> ExpFunctor k :.: Tuple1 (Op k) k y
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: Obj (Op k) y -> Tuple1 (Op k) k y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c1 a -> Tuple1 c1 c2 a
Tuple1 (Obj k y -> Obj (Op k) y
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op Obj k y
y)) (Obj k y -> k a a -> k a (Exponential k y (BinaryProduct k a y))
forall k (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
tuple Obj k y
y) (Obj k y -> k a a -> k (BinaryProduct k (Exponential k y a) y) a
forall k (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
apply Obj k y
y)
curry :: (CartesianClosed k, Kind k ~ *) => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)
curry :: Obj k x
-> Obj k y
-> Obj k z
-> k (BinaryProduct k x y) z
-> k x (Exponential k y z)
curry Obj k x
x Obj k y
y Obj k z
_ = Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
-> Obj k x
-> k ((ProductFunctor k :.: Tuple2 k k y) :% x) z
-> k x ((ExpFunctor k :.: Tuple1 (Op k) k y) :% z)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct (Obj k y
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k y
y) Obj k x
x
uncurry :: (CartesianClosed k, Kind k ~ *) => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z
uncurry :: Obj k x
-> Obj k y
-> Obj k z
-> k x (Exponential k y z)
-> k (BinaryProduct k x y) z
uncurry Obj k x
_ Obj k y
y Obj k z
z = Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
-> Obj k z
-> k x ((ExpFunctor k :.: Tuple1 (Op k) k y) :% z)
-> k ((ProductFunctor k :.: Tuple2 k k y) :% x) 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 (Obj k y
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k y
y) Obj k z
z
type State k s a = Exponential k s (BinaryProduct k a s)
stateMonadReturn :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k a (State k s a)
stateMonadReturn :: Obj k s -> Obj k a -> k a (State k s a)
stateMonadReturn Obj k s
s Obj k a
a = MonoidObject
(EndoFunctorCompose k)
((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
-> Cod
(EndoFunctorCompose k)
(Unit (EndoFunctorCompose k))
((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
forall f a. MonoidObject f a -> Cod f (Unit f) a
M.unit (Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k s)
(ExpFunctor k :.: Tuple1 (Op k) k s)
-> Monad
((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Monad (g :.: f)
adjunctionMonad (Obj k s
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k s)
(ExpFunctor k :.: Tuple1 (Op k) k s)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) Nat
k
k
(Id k)
((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
-> Obj k a
-> k (Id k :% a)
(((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
:% 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 k a
a
stateMonadJoin :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)
stateMonadJoin :: Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)
stateMonadJoin Obj k s
s Obj k a
a = MonoidObject
(EndoFunctorCompose k)
((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
-> Cod
(EndoFunctorCompose k)
(EndoFunctorCompose k
:% ((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s),
(ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s)))
((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
M.multiply (Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k s)
(ExpFunctor k :.: Tuple1 (Op k) k s)
-> Monad
((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Monad (g :.: f)
adjunctionMonad (Obj k s
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k s)
(ExpFunctor k :.: Tuple1 (Op k) k s)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) Nat
k
k
(((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
:.: ((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s)))
((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
-> Obj k a
-> k ((((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
:.: ((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s)))
:% a)
(((ExpFunctor k :.: Tuple1 (Op k) k s)
:.: (ProductFunctor k :.: Tuple2 k k s))
:% 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 k a
a
type Context k s a = BinaryProduct k (Exponential k s a) s
contextComonadExtract :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (Context k s a) a
Obj k s
s Obj k a
a = ComonoidObject
(EndoFunctorCompose k)
((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
-> Cod
(EndoFunctorCompose k)
((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
(Unit (EndoFunctorCompose k))
forall f a. ComonoidObject f a -> Cod f a (Unit f)
M.counit (Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k s)
(ExpFunctor k :.: Tuple1 (Op k) k s)
-> Comonad
((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Comonad (f :.: g)
adjunctionComonad (Obj k s
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k s)
(ExpFunctor k :.: Tuple1 (Op k) k s)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) Nat
k
k
((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
(Id k)
-> Obj k a
-> k (((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
:% a)
(Id k :% 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 k a
a
contextComonadDuplicate :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))
contextComonadDuplicate :: Obj k s
-> Obj k a -> k (Context k s a) (Context k s (Context k s a))
contextComonadDuplicate Obj k s
s Obj k a
a = ComonoidObject
(EndoFunctorCompose k)
((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
-> Cod
(EndoFunctorCompose k)
((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
(EndoFunctorCompose k
:% ((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s),
(ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s)))
forall f a. ComonoidObject f a -> Cod f a (f :% (a, a))
M.comultiply (Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k s)
(ExpFunctor k :.: Tuple1 (Op k) k s)
-> Comonad
((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Comonad (f :.: g)
adjunctionComonad (Obj k s
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k s)
(ExpFunctor k :.: Tuple1 (Op k) k s)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
k
k
(ProductFunctor k :.: Tuple2 k k y)
(ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) Nat
k
k
((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
(((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
:.: ((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s)))
-> Obj k a
-> k (((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
:% a)
((((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s))
:.: ((ProductFunctor k :.: Tuple2 k k s)
:.: (ExpFunctor k :.: Tuple1 (Op k) k s)))
:% 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 k a
a