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

import Data.Kind (Type)

import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Adjunction
import Data.Category.Limit
import Data.Category.Unit


-- | An instance of @HasRightKan p k@ says there are right Kan extensions for all functors with codomain @k@.
class (Functor p, Category k) => HasRightKan p k where
  -- | The right Kan extension of a functor @p@ for functors @f@ with codomain @k@.
  type RanFam p k (f :: Type) :: Type
  -- | 'ran' gives the defining natural transformation of the right Kan extension of @f@ along @p@.
  ran           :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f
  -- | 'ranFactorizer' shows that this extension is universal.
  ranFactorizer :: Nat (Dom p) k (h :.: p) f -> Nat (Cod p) k h (RanFam p k f)

type Ran p f = RanFam p (Cod f) f

ranF :: HasRightKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (RanFam p k f)
ranF :: forall p (k :: * -> * -> *) f.
HasRightKan p k =>
p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (RanFam p k f)
ranF p
p Obj (Nat (Dom p) k) f
f = forall p (k :: * -> * -> *) f.
Nat (Dom p) k (RanFam p k f :.: p) f
-> Obj (Nat (Cod p) k) (RanFam p k f)
ranF' (forall p (k :: * -> * -> *) f.
HasRightKan p k =>
p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f
ran p
p Obj (Nat (Dom p) k) f
f)

ranF' :: Nat (Dom p) k (RanFam p k f :.: p) f -> Obj (Nat (Cod p) k) (RanFam p k f)
ranF' :: forall p (k :: * -> * -> *) f.
Nat (Dom p) k (RanFam p k f :.: p) f
-> Obj (Nat (Cod p) k) (RanFam p k f)
ranF' (Nat (RanFam p k f
r :.: p
_) f
_ forall z. Obj (Dom p) z -> Component (RanFam p k f :.: p) f z
_) = forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId RanFam p k f
r

newtype RanFunctor (p :: Type) (k :: Type -> Type -> Type) = RanFunctor p
instance HasRightKan p k => Functor (RanFunctor p k) where
  type Dom (RanFunctor p k) = Nat (Dom p) k
  type Cod (RanFunctor p k) = Nat (Cod p) k
  type RanFunctor p k :% f = RanFam p k f

  RanFunctor p
p % :: forall a b.
RanFunctor p k
-> Dom (RanFunctor p k) a b
-> Cod (RanFunctor p k) (RanFunctor p k :% a) (RanFunctor p k :% b)
% Dom (RanFunctor p k) a b
n = forall p (k :: * -> * -> *) h f.
HasRightKan p k =>
Nat (Dom p) k (h :.: p) f -> Nat (Cod p) k h (RanFam p k f)
ranFactorizer (Dom (RanFunctor p k) a b
n forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall p (k :: * -> * -> *) f.
HasRightKan p k =>
p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f
ran p
p (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (RanFunctor p k) a b
n))

-- | The right Kan extension along @p@ is right adjoint to precomposition with @p@.
ranAdj :: forall p k. HasRightKan p k => p -> Adjunction (Nat (Dom p) k) (Nat (Cod p) k) (Precompose p k) (RanFunctor p k)
ranAdj :: forall p (k :: * -> * -> *).
HasRightKan p k =>
p
-> Adjunction
     (Nat (Dom p) k) (Nat (Cod p) k) (Precompose p k) (RanFunctor p k)
ranAdj p
p = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall b. Obj c b -> c (f :% (g :% b)) b)
-> Adjunction c d f g
mkAdjunctionTerm (forall (e :: * -> * -> *) f.
(Category e, Functor f) =>
f -> Precompose f e
Precompose p
p) (forall p (k :: * -> * -> *). p -> RanFunctor p k
RanFunctor p
p) (\Obj
  (Dom
     (FunctorCompose (Dom p) (Cod p) k
      :.: Tuple2 (Nat (Cod p) k) (Nat (Dom p) (Cod p)) p))
  a
_ -> forall p (k :: * -> * -> *) h f.
HasRightKan p k =>
Nat (Dom p) k (h :.: p) f -> Nat (Cod p) k h (RanFam p k f)
ranFactorizer) (forall p (k :: * -> * -> *) f.
HasRightKan p k =>
p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f
ran p
p)


-- | An instance of @HasLeftKan p k@ says there are left Kan extensions for all functors with codomain @k@.
class (Functor p, Category k) => HasLeftKan p k where
  -- | The left Kan extension of a functor @p@ for functors @f@ with codomain @k@.
  type LanFam (p :: Type) (k :: Type -> Type -> Type) (f :: Type) :: Type
  -- | 'lan' gives the defining natural transformation of the left Kan extension of @f@ along @p@.
  lan           :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)
  -- | 'lanFactorizer' shows that this extension is universal.
  lanFactorizer :: Nat (Dom p) k f (h :.: p) -> Nat (Cod p) k (LanFam p k f) h

type Lan p f = LanFam p (Cod f) f

lanF :: HasLeftKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (LanFam p k f)
lanF :: forall p (k :: * -> * -> *) f.
HasLeftKan p k =>
p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (LanFam p k f)
lanF p
p Obj (Nat (Dom p) k) f
f = forall p (k :: * -> * -> *) f.
Nat (Dom p) k f (LanFam p k f :.: p)
-> Obj (Nat (Cod p) k) (LanFam p k f)
lanF' (forall p (k :: * -> * -> *) f.
HasLeftKan p k =>
p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)
lan p
p Obj (Nat (Dom p) k) f
f)

lanF' :: Nat (Dom p) k f (LanFam p k f :.: p) -> Obj (Nat (Cod p) k) (LanFam p k f)
lanF' :: forall p (k :: * -> * -> *) f.
Nat (Dom p) k f (LanFam p k f :.: p)
-> Obj (Nat (Cod p) k) (LanFam p k f)
lanF' (Nat f
_ (LanFam p k f
r :.: p
_) forall z. Obj (Dom p) z -> Component f (LanFam p k f :.: p) z
_) = forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId LanFam p k f
r

newtype LanFunctor (p :: Type) (k :: Type -> Type -> Type) = LanFunctor p
instance HasLeftKan p k => Functor (LanFunctor p k) where
  type Dom (LanFunctor p k) = Nat (Dom p) k
  type Cod (LanFunctor p k) = Nat (Cod p) k
  type LanFunctor p k :% f = LanFam p k f

  LanFunctor p
p % :: forall a b.
LanFunctor p k
-> Dom (LanFunctor p k) a b
-> Cod (LanFunctor p k) (LanFunctor p k :% a) (LanFunctor p k :% b)
% Dom (LanFunctor p k) a b
n = forall p (k :: * -> * -> *) f h.
HasLeftKan p k =>
Nat (Dom p) k f (h :.: p) -> Nat (Cod p) k (LanFam p k f) h
lanFactorizer (forall p (k :: * -> * -> *) f.
HasLeftKan p k =>
p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)
lan p
p (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (LanFunctor p k) a b
n) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Dom (LanFunctor p k) a b
n)

-- | The left Kan extension along @p@ is left adjoint to precomposition with @p@.
lanAdj :: forall p k. HasLeftKan p k => p -> Adjunction (Nat (Cod p) k) (Nat (Dom p) k) (LanFunctor p k) (Precompose p k)
lanAdj :: forall p (k :: * -> * -> *).
HasLeftKan p k =>
p
-> Adjunction
     (Nat (Cod p) k) (Nat (Dom p) k) (LanFunctor p k) (Precompose p k)
lanAdj p
p = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> d a (g :% (f :% a)))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionInit (forall p (k :: * -> * -> *). p -> LanFunctor p k
LanFunctor p
p) (forall (e :: * -> * -> *) f.
(Category e, Functor f) =>
f -> Precompose f e
Precompose p
p) (forall p (k :: * -> * -> *) f.
HasLeftKan p k =>
p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)
lan p
p) (\Obj (Nat (Cod p) k) b
_ -> forall p (k :: * -> * -> *) f h.
HasLeftKan p k =>
Nat (Dom p) k f (h :.: p) -> Nat (Cod p) k (LanFam p k f) h
lanFactorizer)


-- | The right Kan extension of @f@ along a functor to the unit category is the limit of @f@.
instance HasLimits j k => HasRightKan (Const j Unit ()) k where
  type RanFam (Const j Unit ()) k f = Const Unit k (LimitFam j k f)
  ran :: forall f.
Const j Unit ()
-> Obj (Nat (Dom (Const j Unit ())) k) f
-> Nat
     (Dom (Const j Unit ()))
     k
     (RanFam (Const j Unit ()) k f :.: Const j Unit ())
     f
ran Const j Unit ()
p f :: Obj (Nat (Dom (Const j Unit ())) k) f
f@Nat{} = let cone :: Cone j k f (LimitFam j k f)
cone = forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasLimits j k =>
Obj (Nat j k) f -> Cone j k f (LimitFam j k f)
limit Obj (Nat (Dom (Const j Unit ())) k) f
f in forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cone j k f n -> Obj k n
coneVertex Cone j k f (LimitFam j k f)
cone) forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: Const j Unit ()
p) (forall (c :: * -> * -> *) (d :: * -> * -> *) f g. Nat c d f g -> f
srcF Obj (Nat (Dom (Const j Unit ())) k) f
f) (Cone j k f (LimitFam j k f)
cone forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)
  ranFactorizer :: forall h f.
Nat (Dom (Const j Unit ())) k (h :.: Const j Unit ()) f
-> Nat (Cod (Const j Unit ())) k h (RanFam (Const j Unit ()) k f)
ranFactorizer n :: Nat (Dom (Const j Unit ())) k (h :.: Const j Unit ()) f
n@(Nat (h
h :.: Const j Unit ()
_) f
_ forall z.
Obj (Dom (Const j Unit ())) z
-> Component (h :.: Const j Unit ()) f z
_) = let fact :: k (h :% ()) (LimitFam j k f)
fact = forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasLimits j k =>
Cone j k f n -> k n (LimitFam j k f)
limitFactorizer (forall (j :: * -> * -> *) (d :: * -> * -> *) f (c :: * -> * -> *) x
       g.
Nat j d (f :.: Const j c x) g -> Nat j d (Const j d (f :% x)) g
constPrecompIn Nat (Dom (Const j Unit ())) k (h :.: Const j Unit ()) f
n) in 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 h
h (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k (h :% ()) (LimitFam j k f)
fact)) (\Obj Unit z
Unit -> k (h :% ()) (LimitFam j k f)
fact)

-- | The left Kan extension of @f@ along a functor to the unit category is the colimit of @f@.
instance HasColimits j k => HasLeftKan (Const j Unit ()) k where
  type LanFam (Const j Unit ()) k f = Const Unit k (ColimitFam j k f)
  lan :: forall f.
Const j Unit ()
-> Obj (Nat (Dom (Const j Unit ())) k) f
-> Nat
     (Dom (Const j Unit ()))
     k
     f
     (LanFam (Const j Unit ()) k f :.: Const j Unit ())
lan Const j Unit ()
p f :: Obj (Nat (Dom (Const j Unit ())) k) f
f@Nat{} = let cocone :: Cocone j k f (ColimitFam j k f)
cocone = forall (j :: * -> * -> *) (k :: * -> * -> *) f.
HasColimits j k =>
Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)
colimit Obj (Nat (Dom (Const j Unit ())) k) f
f in forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (forall (c :: * -> * -> *) (d :: * -> * -> *) f g. Nat c d f g -> f
srcF Obj (Nat (Dom (Const j Unit ())) k) f
f) (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
Cocone j k f n -> Obj k n
coconeVertex Cocone j k f (ColimitFam j k f)
cocone) forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: Const j Unit ()
p) (Cocone j k f (ColimitFam j k f)
cocone forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)
  lanFactorizer :: forall f h.
Nat (Dom (Const j Unit ())) k f (h :.: Const j Unit ())
-> Nat (Cod (Const j Unit ())) k (LanFam (Const j Unit ()) k f) h
lanFactorizer n :: Nat (Dom (Const j Unit ())) k f (h :.: Const j Unit ())
n@(Nat f
_ (h
h :.: Const j Unit ()
_) forall z.
Obj (Dom (Const j Unit ())) z
-> Component f (h :.: Const j Unit ()) z
_) = let fact :: k (ColimitFam j k f) (h :% ())
fact = forall (j :: * -> * -> *) (k :: * -> * -> *) f n.
HasColimits j k =>
Cocone j k f n -> k (ColimitFam j k f) n
colimitFactorizer (forall (j :: * -> * -> *) (d :: * -> * -> *) f g (c :: * -> * -> *)
       x.
Nat j d f (g :.: Const j c x) -> Nat j d f (Const j d (g :% x))
constPrecompOut Nat (Dom (Const j Unit ())) k f (h :.: Const j Unit ())
n) in forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k (ColimitFam j k f) (h :% ())
fact)) h
h (\Obj Unit z
Unit -> k (ColimitFam j k f) (h :% ())
fact)


-- | Ran id = id
instance (Category j, Category k) => HasRightKan (Id j) k where
  type RanFam (Id j) k f = f
  ran :: forall f.
Id j
-> Obj (Nat (Dom (Id j)) k) f
-> Nat (Dom (Id j)) k (RanFam (Id j) k f :.: Id j) f
ran Id j
Id (Nat f
f f
_ forall z. Obj (Dom (Id j)) z -> Component f f z
_) = forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp f
f
  ranFactorizer :: forall h f.
Nat (Dom (Id j)) k (h :.: Id j) f
-> Nat (Cod (Id j)) k h (RanFam (Id j) k f)
ranFactorizer n :: Nat (Dom (Id j)) k (h :.: Id j) f
n@(Nat (h
h :.: Id j
Id) f
_ forall z. Obj (Dom (Id j)) z -> Component (h :.: Id j) f z
_) = Nat (Dom (Id j)) k (h :.: Id j) f
n forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv h
h

-- | Lan id = id
instance (Category j, Category k) => HasLeftKan (Id j) k where
  type LanFam (Id j) k f = f
  lan :: forall f.
Id j
-> Obj (Nat (Dom (Id j)) k) f
-> Nat (Dom (Id j)) k f (LanFam (Id j) k f :.: Id j)
lan Id j
Id (Nat f
f f
_ forall z. Obj (Dom (Id j)) z -> Component f f z
_) = forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv f
f
  lanFactorizer :: forall f h.
Nat (Dom (Id j)) k f (h :.: Id j)
-> Nat (Cod (Id j)) k (LanFam (Id j) k f) h
lanFactorizer n :: Nat (Dom (Id j)) k f (h :.: Id j)
n@(Nat f
_ (h
h :.: Id j
Id) forall z. Obj (Dom (Id j)) z -> Component f (h :.: Id j) z
_) = forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp h
h forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Nat (Dom (Id j)) k f (h :.: Id j)
n


-- | Ran (q . p) = Ran q . Ran p
instance (HasRightKan q k, HasRightKan p k) => HasRightKan (q :.: p) k where
  type RanFam (q :.: p) k f = RanFam q k (RanFam p k f)
  ran :: forall f.
(q :.: p)
-> Obj (Nat (Dom (q :.: p)) k) f
-> Nat (Dom (q :.: p)) k (RanFam (q :.: p) k f :.: (q :.: p)) f
ran (q
q :.: p
p) Obj (Nat (Dom (q :.: p)) k) f
f = let ranp :: Nat (Dom p) k (RanFam p k f :.: p) f
ranp = forall p (k :: * -> * -> *) f.
HasRightKan p k =>
p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f
ran p
p Obj (Nat (Dom (q :.: p)) k) f
f in case forall p (k :: * -> * -> *) f.
HasRightKan p k =>
p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f
ran q
q (forall p (k :: * -> * -> *) f.
Nat (Dom p) k (RanFam p k f :.: p) f
-> Obj (Nat (Cod p) k) (RanFam p k f)
ranF' Nat (Dom p) k (RanFam p k f :.: p) f
ranp) of
      ranq :: Nat (Dom q) k (RanFam q k (RanFam p k f) :.: q) (RanFam p k f)
ranq@(Nat (RanFam q k (RanFam p k f)
r :.: q
_) RanFam p k f
_ forall z.
Obj (Dom q) z
-> Component (RanFam q k (RanFam p k f) :.: q) (RanFam p k f) z
_) -> Nat (Dom p) k (RanFam p k f :.: p) f
ranp forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Nat (Dom q) k (RanFam q k (RanFam p k f) :.: q) (RanFam p k f)
ranq forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId p
p) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f g h.
(Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) =>
f
-> g
-> h
-> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
compAssocInv RanFam q k (RanFam p k f)
r q
q p
p
  ranFactorizer :: forall h f.
Nat (Dom (q :.: p)) k (h :.: (q :.: p)) f
-> Nat (Cod (q :.: p)) k h (RanFam (q :.: p) k f)
ranFactorizer n :: Nat (Dom (q :.: p)) k (h :.: (q :.: p)) f
n@(Nat (h
h :.: (q
q :.: p
p)) f
_ forall z. Obj (Dom (q :.: p)) z -> Component (h :.: (q :.: p)) f z
_) = forall p (k :: * -> * -> *) h f.
HasRightKan p k =>
Nat (Dom p) k (h :.: p) f -> Nat (Cod p) k h (RanFam p k f)
ranFactorizer (forall p (k :: * -> * -> *) h f.
HasRightKan p k =>
Nat (Dom p) k (h :.: p) f -> Nat (Cod p) k h (RanFam p k f)
ranFactorizer (Nat (Dom (q :.: p)) k (h :.: (q :.: p)) f
n forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f g h.
(Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) =>
f
-> g
-> h
-> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
compAssoc h
h q
q p
p))

-- | Lan (q . p) = Lan q . Lan p
instance (HasLeftKan q k, HasLeftKan p k) => HasLeftKan (q :.: p) k where
  type LanFam (q :.: p) k f = LanFam q k (LanFam p k f)
  lan :: forall f.
(q :.: p)
-> Obj (Nat (Dom (q :.: p)) k) f
-> Nat (Dom (q :.: p)) k f (LanFam (q :.: p) k f :.: (q :.: p))
lan (q
q :.: p
p) Obj (Nat (Dom (q :.: p)) k) f
f = let lanp :: Nat (Dom p) k f (LanFam p k f :.: p)
lanp = forall p (k :: * -> * -> *) f.
HasLeftKan p k =>
p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)
lan p
p Obj (Nat (Dom (q :.: p)) k) f
f in case forall p (k :: * -> * -> *) f.
HasLeftKan p k =>
p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)
lan q
q (forall p (k :: * -> * -> *) f.
Nat (Dom p) k f (LanFam p k f :.: p)
-> Obj (Nat (Cod p) k) (LanFam p k f)
lanF' Nat (Dom p) k f (LanFam p k f :.: p)
lanp) of
      lanq :: Nat (Dom q) k (LanFam p k f) (LanFam q k (LanFam p k f) :.: q)
lanq@(Nat LanFam p k f
_ (LanFam q k (LanFam p k f)
l :.: q
_) forall z.
Obj (Dom q) z
-> Component (LanFam p k f) (LanFam q k (LanFam p k f) :.: q) z
_) -> forall f g h.
(Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) =>
f
-> g
-> h
-> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
compAssoc LanFam q k (LanFam p k f)
l q
q p
p forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Nat (Dom q) k (LanFam p k f) (LanFam q k (LanFam p k f) :.: q)
lanq forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId p
p) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Nat (Dom p) k f (LanFam p k f :.: p)
lanp
  lanFactorizer :: forall f h.
Nat (Dom (q :.: p)) k f (h :.: (q :.: p))
-> Nat (Cod (q :.: p)) k (LanFam (q :.: p) k f) h
lanFactorizer n :: Nat (Dom (q :.: p)) k f (h :.: (q :.: p))
n@(Nat f
_ (h
h :.: (q
q :.: p
p)) forall z. Obj (Dom (q :.: p)) z -> Component f (h :.: (q :.: p)) z
_) = forall p (k :: * -> * -> *) f h.
HasLeftKan p k =>
Nat (Dom p) k f (h :.: p) -> Nat (Cod p) k (LanFam p k f) h
lanFactorizer (forall p (k :: * -> * -> *) f h.
HasLeftKan p k =>
Nat (Dom p) k f (h :.: p) -> Nat (Cod p) k (LanFam p k f) h
lanFactorizer (forall f g h.
(Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) =>
f
-> g
-> h
-> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
compAssocInv h
h q
q p
p forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Nat (Dom (q :.: p)) k f (h :.: (q :.: p))
n))


newtype RanHask p f a = RanHask (forall c. Obj (Dom p) c -> Cod p a (p :% c) -> f :% c)
data RanHaskF p f = RanHaskF
instance Functor p => Functor (RanHaskF p f) where
  type Dom (RanHaskF p f) = Cod p
  type Cod (RanHaskF p f) = (->)
  type RanHaskF p f :% a = RanHask p f a
  RanHaskF p f
RanHaskF % :: forall a b.
RanHaskF p f
-> Dom (RanHaskF p f) a b
-> Cod (RanHaskF p f) (RanHaskF p f :% a) (RanHaskF p f :% b)
% Dom (RanHaskF p f) a b
ab = \(RanHask forall c. Obj (Dom p) c -> Cod p a (p :% c) -> f :% c
r) -> forall p f a.
(forall c. Obj (Dom p) c -> Cod p a (p :% c) -> f :% c)
-> RanHask p f a
RanHask (\Obj (Dom p) c
c Cod p b (p :% c)
bpc -> forall c. Obj (Dom p) c -> Cod p a (p :% c) -> f :% c
r Obj (Dom p) c
c (Cod p b (p :% c)
bpc forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Dom (RanHaskF p f) a b
ab))

instance Functor p => HasRightKan (Any p) (->) where
  type RanFam (Any p) (->) f = RanHaskF p f
  ran :: forall f.
Any p
-> Obj (Nat (Dom (Any p)) (->)) f
-> Nat (Dom (Any p)) (->) (RanFam (Any p) (->) f :.: Any p) f
ran (Any p
p) (Nat f
f f
_ forall z. Obj (Dom (Any p)) z -> Component f f z
_) = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (forall p f. RanHaskF p f
RanHaskF forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: forall f. f -> Any f
Any p
p) f
f (\Obj (Dom f) z
z (RanHask forall c. Obj (Dom p) c -> Cod p (p :% z) (p :% c) -> f :% c
r) -> forall c. Obj (Dom p) c -> Cod p (p :% z) (p :% c) -> f :% c
r Obj (Dom f) z
z (p
p forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (Dom f) z
z))
  ranFactorizer :: forall h f.
Nat (Dom (Any p)) (->) (h :.: Any p) f
-> Nat (Cod (Any p)) (->) h (RanFam (Any p) (->) f)
ranFactorizer (Nat (h
h :.: Any p
_) f
_ forall z. Obj (Dom (Any p)) z -> Component (h :.: Any p) f z
n) = 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 h
h forall p f. RanHaskF p f
RanHaskF (\Obj (Dom h) z
_ h :% z
hz -> forall p f a.
(forall c. Obj (Dom p) c -> Cod p a (p :% c) -> f :% c)
-> RanHask p f a
RanHask (\Obj (Dom p) c
c Cod p z (p :% c)
zpc -> forall z. Obj (Dom (Any p)) z -> Component (h :.: Any p) f z
n Obj (Dom p) c
c ((h
h forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Cod p z (p :% c)
zpc) h :% z
hz)))

data LanHask p f a where
  LanHask :: Obj (Dom p) c -> Cod p (p :% c) a -> f :% c -> LanHask p f a
data LanHaskF p f = LanHaskF
instance Functor p => Functor (LanHaskF p f) where
  type Dom (LanHaskF p f) = Cod p
  type Cod (LanHaskF p f) = (->)
  type LanHaskF p f :% a = LanHask p f a
  LanHaskF p f
LanHaskF % :: forall a b.
LanHaskF p f
-> Dom (LanHaskF p f) a b
-> Cod (LanHaskF p f) (LanHaskF p f :% a) (LanHaskF p f :% b)
% Dom (LanHaskF p f) a b
ab = \(LanHask Obj (Dom p) c
c Cod p (p :% c) a
pca f :% c
fc) -> forall p c a f.
Obj (Dom p) c -> Cod p (p :% c) a -> (f :% c) -> LanHask p f a
LanHask Obj (Dom p) c
c (Dom (LanHaskF p f) a b
ab forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cod p (p :% c) a
pca) f :% c
fc

instance Functor p => HasLeftKan (Any p) (->) where
  type LanFam (Any p) (->) f = LanHaskF p f
  lan :: forall f.
Any p
-> Obj (Nat (Dom (Any p)) (->)) f
-> Nat (Dom (Any p)) (->) f (LanFam (Any p) (->) f :.: Any p)
lan (Any p
p) (Nat f
f f
_ forall z. Obj (Dom (Any p)) z -> Component f f z
_) = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (forall p f. LanHaskF p f
LanHaskF forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: forall f. f -> Any f
Any p
p) (\Obj (Dom f) z
z f :% z
fz -> forall p c a f.
Obj (Dom p) c -> Cod p (p :% c) a -> (f :% c) -> LanHask p f a
LanHask Obj (Dom f) z
z (p
p forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (Dom f) z
z) f :% z
fz)
  lanFactorizer :: forall f h.
Nat (Dom (Any p)) (->) f (h :.: Any p)
-> Nat (Cod (Any p)) (->) (LanFam (Any p) (->) f) h
lanFactorizer (Nat f
_ (h
h :.: Any p
_) forall z. Obj (Dom (Any p)) z -> Component f (h :.: Any p) z
n) = 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 p f. LanHaskF p f
LanHaskF h
h (\Obj (Cod p) z
_ (LanHask Obj (Dom p) c
c Cod p (p :% c) z
pcz f :% c
fc) -> (h
h forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Cod p (p :% c) z
pcz) (forall z. Obj (Dom (Any p)) z -> Component f (h :.: Any p) z
n Obj (Dom p) c
c f :% c
fc))