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

import Data.Kind (Type)

import Data.Category
import Data.Category.Functor
import Data.Category.Product
import Data.Category.NaturalTransformation
import qualified Data.Category.Limit as L


type WeightedCone w d e = forall a. Obj (Dom w) a -> w :% a -> Cod d e (d :% a)

-- | @w@-weighted limits in the category @k@.
class (Functor w, Cod w ~ (->), Category k) => HasWLimits k w where
  type WeightedLimit k w d :: Type
  limitObj :: FunctorOf (Dom w) k d => w -> d -> Obj k (WLimit w d)
  limit :: FunctorOf (Dom w) k d => w -> d -> WeightedCone w d (WLimit w d)
  limitFactorizer :: FunctorOf (Dom w) k d => w -> d -> Obj k e -> WeightedCone w d e -> k e (WLimit w d)

type WLimit w d = WeightedLimit (Cod d) w d

data LimitFunctor (k :: Type -> Type -> Type) w = LimitFunctor w
instance HasWLimits k w => Functor (LimitFunctor k w) where
  type Dom (LimitFunctor k w) = Nat (Dom w) k
  type Cod (LimitFunctor k w) = k
  type LimitFunctor k w :% d = WeightedLimit k w d

  LimitFunctor w
w % :: forall a b.
LimitFunctor k w
-> Dom (LimitFunctor k w) a b
-> Cod
     (LimitFunctor k w) (LimitFunctor k w :% a) (LimitFunctor k w :% b)
% Nat a
d b
d' forall z. Obj (Dom w) z -> Component a b z
n = forall (k :: * -> * -> *) w d e.
(HasWLimits k w, FunctorOf (Dom w) k d) =>
w -> d -> Obj k e -> WeightedCone w d e -> k e (WLimit w d)
limitFactorizer w
w b
d' (forall (k :: * -> * -> *) w d.
(HasWLimits k w, FunctorOf (Dom w) k d) =>
w -> d -> Obj k (WLimit w d)
limitObj w
w a
d) (\Obj (Dom w) a
a w :% a
wa -> forall z. Obj (Dom w) z -> Component a b z
n Obj (Dom w) a
a forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) w d.
(HasWLimits k w, FunctorOf (Dom w) k d) =>
w -> d -> WeightedCone w d (WLimit w d)
limit w
w a
d Obj (Dom w) a
a w :% a
wa)


-- | Regular limits as weigthed limits, weighted by the constant functor to '()'.
instance L.HasLimits j k => HasWLimits k (Const j (->) ()) where
  type WeightedLimit k (Const j (->) ()) d = L.Limit d
  limitObj :: forall d.
FunctorOf (Dom (Const j (->) ())) k d =>
Const j (->) () -> d -> Obj k (WLimit (Const j (->) ()) d)
limitObj Const{} d
d = forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
L.coneVertex (forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
L.limit (forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId d
d))
  limit :: forall d.
FunctorOf (Dom (Const j (->) ())) k d =>
Const j (->) ()
-> d
-> WeightedCone (Const j (->) ()) d (WLimit (Const j (->) ()) d)
limit Const{} d
d Obj (Dom (Const j (->) ())) a
a () = forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
L.limit (forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId d
d) 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 (Dom (Const j (->) ())) a
a
  limitFactorizer :: forall d e.
FunctorOf (Dom (Const j (->) ())) k d =>
Const j (->) ()
-> d
-> Obj k e
-> WeightedCone (Const j (->) ()) d e
-> k e (WLimit (Const j (->) ()) d)
limitFactorizer Const{} d
d Obj k e
e WeightedCone (Const j (->) ()) d e
f = forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
L.limitFactorizer (forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj k e
e) d
d (WeightedCone (Const j (->) ()) d e
`f` ()))


class Category v => HasEnds v where
  type End (v :: Type -> Type -> Type) t :: Type
  end :: FunctorOf (Op k :**: k) v t => t -> Obj v (End v t)
  endCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (End v t) (t :% (a, a))
  endFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v x (t :% (a, a))) -> v x (End v t)

-- | Ends as Hom-weighted limits
instance HasEnds k => HasWLimits k (Hom k) where
  type WeightedLimit k (Hom k) d = End k d
  limitObj :: forall d.
FunctorOf (Dom (Hom k)) k d =>
Hom k -> d -> Obj k (WLimit (Hom k) d)
limitObj Hom k
Hom d
d = forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, FunctorOf (Op k :**: k) v t) =>
t -> Obj v (End v t)
end d
d
  limit :: forall d.
FunctorOf (Dom (Hom k)) k d =>
Hom k -> d -> WeightedCone (Hom k) d (WLimit (Hom k) d)
limit Hom k
Hom d
d (Op k b1 a1
a :**: k a2 b2
_) Hom k :% a
ab = d
d forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k b1 a1
a forall (c1 :: * -> * -> *) k a (c2 :: * -> * -> *) a2 b2.
c1 k a -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (a, b2)
:**: Hom k :% a
ab) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasEnds v, FunctorOf (Op k :**: k) v t) =>
t -> Obj k a -> v (End v t) (t :% (a, a))
endCounit d
d k b1 a1
a
  limitFactorizer :: forall d e.
FunctorOf (Dom (Hom k)) k d =>
Hom k
-> d
-> Obj k e
-> WeightedCone (Hom k) d e
-> k e (WLimit (Hom k) d)
limitFactorizer Hom k
Hom d
d Obj k e
_ WeightedCone (Hom k) d e
f = forall (v :: * -> * -> *) (k :: * -> * -> *) t x.
(HasEnds v, FunctorOf (Op k :**: k) v t) =>
t -> (forall a. Obj k a -> v x (t :% (a, a))) -> v x (End v t)
endFactorizer d
d (\Obj k a
a -> WeightedCone (Hom k) d e
f (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj k a
a forall (c1 :: * -> * -> *) k a (c2 :: * -> * -> *) a2 b2.
c1 k a -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (a, b2)
:**: Obj k a
a) Obj k a
a)

data EndFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) = EndFunctor
instance (HasEnds v, Category k) => Functor (EndFunctor k v) where
  type Dom (EndFunctor k v) = Nat (Op k :**: k) v
  type Cod (EndFunctor k v) = v
  type EndFunctor k v :% t = End v t

  EndFunctor k v
EndFunctor % :: forall a b.
EndFunctor k v
-> Dom (EndFunctor k v) a b
-> Cod (EndFunctor k v) (EndFunctor k v :% a) (EndFunctor k v :% b)
% Nat a
f b
g forall z. Obj (Op k :**: k) z -> Component a b z
n = forall (v :: * -> * -> *) (k :: * -> * -> *) t x.
(HasEnds v, FunctorOf (Op k :**: k) v t) =>
t -> (forall a. Obj k a -> v x (t :% (a, a))) -> v x (End v t)
endFactorizer b
g (\Obj k a
a -> forall z. Obj (Op k :**: k) z -> Component a b z
n (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj k a
a forall (c1 :: * -> * -> *) k a (c2 :: * -> * -> *) a2 b2.
c1 k a -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (a, b2)
:**: Obj k a
a) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasEnds v, FunctorOf (Op k :**: k) v t) =>
t -> Obj k a -> v (End v t) (t :% (a, a))
endCounit a
f Obj k a
a)

newtype HaskEnd t = HaskEnd { forall t.
HaskEnd t
-> forall (k :: * -> * -> *) a.
   FunctorOf (Op k :**: k) (->) t =>
   t -> Obj k a -> t :% (a, a)
getHaskEnd :: forall k a. FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a) }
instance HasEnds (->) where
  type End (->) t = HaskEnd t
  end :: forall (k :: * -> * -> *) t.
FunctorOf (Op k :**: k) (->) t =>
t -> Obj (->) (End (->) t)
end t
_ End (->) t
e = End (->) t
e
  endCounit :: forall (k :: * -> * -> *) t a.
FunctorOf (Op k :**: k) (->) t =>
t -> Obj k a -> End (->) t -> (t :% (a, a))
endCounit t
t Obj k a
a (HaskEnd forall (k :: * -> * -> *) a.
FunctorOf (Op k :**: k) (->) t =>
t -> Obj k a -> t :% (a, a)
f) = forall (k :: * -> * -> *) a.
FunctorOf (Op k :**: k) (->) t =>
t -> Obj k a -> t :% (a, a)
f t
t Obj k a
a
  endFactorizer :: forall (k :: * -> * -> *) t x.
FunctorOf (Op k :**: k) (->) t =>
t -> (forall a. Obj k a -> x -> (t :% (a, a))) -> x -> End (->) t
endFactorizer t
_ forall a. Obj k a -> x -> (t :% (a, a))
e x
x = forall t.
(forall (k :: * -> * -> *) a.
 FunctorOf (Op k :**: k) (->) t =>
 t -> Obj k a -> t :% (a, a))
-> HaskEnd t
HaskEnd (\t
_ Obj k a
a -> forall a. Obj k a -> x -> (t :% (a, a))
e Obj k a
a x
x)


type WeightedCocone w d e = forall a. Obj (Dom w) a -> w :% a -> Cod d (d :% a) e

-- | @w@-weighted colimits in the category @k@.
class (Functor w, Cod w ~ (->), Category k) => HasWColimits k w where
  type WeightedColimit k w d :: Type
  colimitObj :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k (WColimit w d)
  colimit :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> WeightedCocone w d (WColimit w d)
  colimitFactorizer :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k e -> WeightedCocone w d e -> k (WColimit w d) e

type WColimit w d = WeightedColimit (Cod d) w d

data ColimitFunctor (k :: Type -> Type -> Type) w = ColimitFunctor w
instance (Functor w, Category k, HasWColimits k (w :.: OpOp (Dom w))) => Functor (ColimitFunctor k w) where
  type Dom (ColimitFunctor k w) = Nat (Op (Dom w)) k
  type Cod (ColimitFunctor k w) = k
  type ColimitFunctor k w :% d = WeightedColimit k (w :.: OpOp (Dom w)) d

  ColimitFunctor w
w % :: forall a b.
ColimitFunctor k w
-> Dom (ColimitFunctor k w) a b
-> Cod
     (ColimitFunctor k w)
     (ColimitFunctor k w :% a)
     (ColimitFunctor k w :% b)
% Nat a
d b
d' forall z. Obj (Op (Dom w)) z -> Component a b z
n = forall (k :: * -> * -> *) w (j :: * -> * -> *) d e.
(HasWColimits k w, FunctorOf j k d, Op j ~ Dom w) =>
w -> d -> Obj k e -> WeightedCocone w d e -> k (WColimit w d) e
colimitFactorizer (w
w forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: forall (k :: * -> * -> *). OpOp k
OpOp) a
d (forall (k :: * -> * -> *) w (j :: * -> * -> *) d.
(HasWColimits k w, FunctorOf j k d, Op j ~ Dom w) =>
w -> d -> Obj k (WColimit w d)
colimitObj (w
w forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: forall (k :: * -> * -> *). OpOp k
OpOp) b
d') (\(Op Op (Dom w) a a
a) (w :.: OpOp (Dom w)) :% a
wa -> forall (k :: * -> * -> *) w (j :: * -> * -> *) d.
(HasWColimits k w, FunctorOf j k d, Op j ~ Dom w) =>
w -> d -> WeightedCocone w d (WColimit w d)
colimit (w
w forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: forall (k :: * -> * -> *). OpOp k
OpOp) b
d' (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Op (Dom w) a a
a) (w :.: OpOp (Dom w)) :% a
wa forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall z. Obj (Op (Dom w)) z -> Component a b z
n Op (Dom w) a a
a)


-- | Regular colimits as weigthed colimits, weighted by the constant functor to '()'.
instance L.HasColimits j k => HasWColimits k (Const (Op j) (->) ()) where
  type WeightedColimit k (Const (Op j) (->) ()) d = L.Colimit d
  colimitObj :: forall (j :: * -> * -> *) d.
(FunctorOf j k d, Op j ~ Dom (Const (Op j) (->) ())) =>
Const (Op j) (->) ()
-> d -> Obj k (WColimit (Const (Op j) (->) ()) d)
colimitObj (Const Obj (->) ()
_) d
d = forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
L.coconeVertex (forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
L.colimit (forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId d
d))
  colimit :: forall (j :: * -> * -> *) d.
(FunctorOf j k d, Op j ~ Dom (Const (Op j) (->) ())) =>
Const (Op j) (->) ()
-> d
-> WeightedCocone
     (Const (Op j) (->) ()) d (WColimit (Const (Op j) (->) ()) d)
colimit (Const Obj (->) ()
_) d
d (Op j a a
a) () = forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
L.colimit (forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId d
d) 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 a a
a
  colimitFactorizer :: forall (j :: * -> * -> *) d e.
(FunctorOf j k d, Op j ~ Dom (Const (Op j) (->) ())) =>
Const (Op j) (->) ()
-> d
-> Obj k e
-> WeightedCocone (Const (Op j) (->) ()) d e
-> k (WColimit (Const (Op j) (->) ()) d) e
colimitFactorizer (Const Obj (->) ()
_) d
d Obj k e
e WeightedCocone (Const (Op j) (->) ()) d e
f = forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
L.colimitFactorizer (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 d
d (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj k e
e) (\Obj j z
z -> WeightedCocone (Const (Op j) (->) ()) d e
f (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj j z
z) ()))


class Category v => HasCoends v where
  type Coend (v :: Type -> Type -> Type) t :: Type
  coend :: FunctorOf (Op k :**: k) v t => t -> Obj v (Coend v t)
  coendCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (t :% (a, a)) (Coend v t)
  coendFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v (t :% (a, a)) x) -> v (Coend v t) x

data OpHom (k :: Type -> Type -> Type) = OpHom
-- | The Hom-functor but with opposite domain.
instance Category k => Functor (OpHom k) where
  type Dom (OpHom k) = Op (Op k :**: k)
  type Cod (OpHom k) = (->)
  type OpHom k :% (a1, a2) = k a2 a1
  OpHom k
OpHom % :: forall a b.
OpHom k
-> Dom (OpHom k) a b -> Cod (OpHom k) (OpHom k :% a) (OpHom k :% b)
% Op (Op k b1 a1
f1 :**: k a2 b2
f2) = \k b2 b1
g -> k b1 a1
f1 forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k b2 b1
g 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
f2

-- | Coends as OpHom-weighted colimits
instance HasCoends k => HasWColimits k (OpHom k) where
  type WeightedColimit k (OpHom k) d = Coend k d
  colimitObj :: forall (j :: * -> * -> *) d.
(FunctorOf j k d, Op j ~ Dom (OpHom k)) =>
OpHom k -> d -> Obj k (WColimit (OpHom k) d)
colimitObj OpHom k
OpHom d
d = forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasCoends v, FunctorOf (Op k :**: k) v t) =>
t -> Obj v (Coend v t)
coend d
d
  colimit :: forall (j :: * -> * -> *) d.
(FunctorOf j k d, Op j ~ Dom (OpHom k)) =>
OpHom k -> d -> WeightedCocone (OpHom k) d (WColimit (OpHom k) d)
colimit OpHom k
OpHom d
d (Op (Op k b1 a1
a :**: k a2 b2
_)) OpHom k :% a
ab = forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasCoends v, FunctorOf (Op k :**: k) v t) =>
t -> Obj k a -> v (t :% (a, a)) (Coend v t)
coendCounit d
d k b1 a1
a forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. d
d forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k b1 a1
a forall (c1 :: * -> * -> *) k a (c2 :: * -> * -> *) a2 b2.
c1 k a -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (a, b2)
:**: OpHom k :% a
ab)
  colimitFactorizer :: forall (j :: * -> * -> *) d e.
(FunctorOf j k d, Op j ~ Dom (OpHom k)) =>
OpHom k
-> d
-> Obj k e
-> WeightedCocone (OpHom k) d e
-> k (WColimit (OpHom k) d) e
colimitFactorizer OpHom k
OpHom d
d Obj k e
_ WeightedCocone (OpHom k) d e
f = forall (v :: * -> * -> *) (k :: * -> * -> *) t x.
(HasCoends v, FunctorOf (Op k :**: k) v t) =>
t -> (forall a. Obj k a -> v (t :% (a, a)) x) -> v (Coend v t) x
coendFactorizer d
d (\Obj k a
a -> WeightedCocone (OpHom k) d e
f (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj k a
a forall (c1 :: * -> * -> *) k a (c2 :: * -> * -> *) a2 b2.
c1 k a -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (a, b2)
:**: Obj k a
a)) Obj k a
a)

data CoendFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) = CoendFunctor
instance (HasCoends v, Category k) => Functor (CoendFunctor k v) where
  type Dom (CoendFunctor k v) = Nat (Op k :**: k) v
  type Cod (CoendFunctor k v) = v
  type CoendFunctor k v :% t = Coend v t

  CoendFunctor k v
CoendFunctor % :: forall a b.
CoendFunctor k v
-> Dom (CoendFunctor k v) a b
-> Cod
     (CoendFunctor k v) (CoendFunctor k v :% a) (CoendFunctor k v :% b)
% Nat a
f b
g forall z. Obj (Op k :**: k) z -> Component a b z
n = forall (v :: * -> * -> *) (k :: * -> * -> *) t x.
(HasCoends v, FunctorOf (Op k :**: k) v t) =>
t -> (forall a. Obj k a -> v (t :% (a, a)) x) -> v (Coend v t) x
coendFactorizer a
f (\Obj k a
a -> forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasCoends v, FunctorOf (Op k :**: k) v t) =>
t -> Obj k a -> v (t :% (a, a)) (Coend v t)
coendCounit b
g Obj k a
a forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall z. Obj (Op k :**: k) z -> Component a b z
n (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj k a
a forall (c1 :: * -> * -> *) k a (c2 :: * -> * -> *) a2 b2.
c1 k a -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (a, b2)
:**: Obj k a
a))

data HaskCoend t where
  HaskCoend :: FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a) -> HaskCoend t
instance HasCoends (->) where
  type Coend (->) t = HaskCoend t
  coend :: forall (k :: * -> * -> *) t.
FunctorOf (Op k :**: k) (->) t =>
t -> Obj (->) (Coend (->) t)
coend t
_ Coend (->) t
e = Coend (->) t
e
  coendCounit :: forall (k :: * -> * -> *) t a.
FunctorOf (Op k :**: k) (->) t =>
t -> Obj k a -> (t :% (a, a)) -> Coend (->) t
coendCounit t
t Obj k a
a t :% (a, a)
taa = forall (k :: * -> * -> *) t a.
FunctorOf (Op k :**: k) (->) t =>
t -> Obj k a -> (t :% (a, a)) -> HaskCoend t
HaskCoend t
t Obj k a
a t :% (a, a)
taa
  coendFactorizer :: forall (k :: * -> * -> *) t x.
FunctorOf (Op k :**: k) (->) t =>
t -> (forall a. Obj k a -> (t :% (a, a)) -> x) -> Coend (->) t -> x
coendFactorizer t
_ forall a. Obj k a -> (t :% (a, a)) -> x
f (HaskCoend t
_ Obj k a
a t :% (a, a)
taa) = forall a. Obj k a -> (t :% (a, a)) -> x
f Obj k a
a t :% (a, a)
taa