{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Bicategory.Kan where

import Data.Kind (Constraint, Type)

import Proarrow.Category.Bicategory (Bicategory(..))
import Proarrow.Category.Bicategory.MonoidalAsBi (MonK(..), Mon2 (..))
import Proarrow.Core (CAT, Ob, obj, CategoryOf (..), Promonad (..))
import Data.Functor.Compose (Compose(..))
import Prelude (($))
import Proarrow.Category.Instance.Nat (Nat(..))
import Proarrow.Functor (map, Functor)


type LeftKanExtension :: forall {k} {kk :: CAT k} {c} {d} {e}. kk c d -> kk c e -> Constraint
class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Lan j f)) => LeftKanExtension (j :: kk c d) (f :: kk c e) where
  type Lan j f :: kk d e
  lan :: f ~> j `O` Lan j f
  lanUniv :: Ob g => (f ~> j `O` g) -> Lan j f ~> g

mapLan :: forall j f g. (LeftKanExtension j f, LeftKanExtension j g) => (f ~> g) -> Lan j f ~> Lan j g
mapLan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk c e).
(LeftKanExtension j f, LeftKanExtension j g) =>
(f ~> g) -> Lan j f ~> Lan j g
mapLan f ~> g
fg = forall (j :: kk c d) (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O j g) -> Lan j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O j g) -> Lan j f ~> g
lanUniv @j (forall (j :: kk c d) (f :: kk c e).
LeftKanExtension j f =>
f ~> O j (Lan j f)
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O j (Lan j f)
lan @j (g ~> O j (Lan j g)) -> (f ~> g) -> f ~> O j (Lan j g)
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. f ~> g
fg)

rebaseLan :: forall i j f. (LeftKanExtension j f, LeftKanExtension i f) => (i ~> j) -> Lan j f ~> Lan i f
rebaseLan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (i :: kk c d)
       (j :: kk c d) (f :: kk c e).
(LeftKanExtension j f, LeftKanExtension i f) =>
(i ~> j) -> Lan j f ~> Lan i f
rebaseLan i ~> j
ij = forall (j :: kk c d) (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O j g) -> Lan j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O j g) -> Lan j f ~> g
lanUniv @j ((i ~> j
ij (i ~> j) -> (Lan i f ~> Lan i f) -> O i (Lan i f) ~> O j (Lan i f)
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk d e). (CategoryOf (kk d e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Lan i f)) (O i (Lan i f) ~> O j (Lan i f))
-> (f ~> O i (Lan i f)) -> f ~> O j (Lan i f)
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk c d) (f :: kk c e).
LeftKanExtension j f =>
f ~> O j (Lan j f)
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O j (Lan j f)
lan @i @f)


type RightKanExtension :: forall {k} {kk :: CAT k} {c} {d} {e}. kk c d -> kk c e -> Constraint
class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Ran j f)) => RightKanExtension (j :: kk c d) (f :: kk c e) where
  type Ran j f :: kk d e
  ran :: j `O` Ran j f ~> f
  ranUniv :: Ob g => (j `O` g ~> f) -> g ~> Ran j f

mapRan :: forall j f g. (RightKanExtension j f, RightKanExtension j g) => (f ~> g) -> Ran j f ~> Ran j g
mapRan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk c e).
(RightKanExtension j f, RightKanExtension j g) =>
(f ~> g) -> Ran j f ~> Ran j g
mapRan f ~> g
fg = forall (j :: kk c d) (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O j g ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O j g ~> f) -> g ~> Ran j f
ranUniv @j (f ~> g
fg (f ~> g) -> (O j (Ran j f) ~> f) -> O j (Ran j f) ~> g
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk c d) (f :: kk c e).
RightKanExtension j f =>
O j (Ran j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O j (Ran j f) ~> f
ran @j)

rebaseRan :: forall i j f. (RightKanExtension j f, RightKanExtension i f) => (i ~> j) -> Ran j f ~> Ran i f
rebaseRan :: forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (i :: kk c d)
       (j :: kk c d) (f :: kk c e).
(RightKanExtension j f, RightKanExtension i f) =>
(i ~> j) -> Ran j f ~> Ran i f
rebaseRan i ~> j
ij = forall (j :: kk c d) (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O j g ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O j g ~> f) -> g ~> Ran j f
ranUniv @i @f (forall (j :: kk c d) (f :: kk c e).
RightKanExtension j f =>
O j (Ran j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O j (Ran j f) ~> f
ran @j (O j (Ran j f) ~> f)
-> (O i (Ran j f) ~> O j (Ran j f)) -> O i (Ran j f) ~> f
forall (b :: kk c e) (c :: kk c e) (a :: kk c e).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (i ~> j
ij (i ~> j) -> (Ran j f ~> Ran j f) -> O i (Ran j f) ~> O j (Ran j f)
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk d e). (CategoryOf (kk d e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Ran j f)))


type LeftKanLift :: forall {k} {kk :: CAT k} {c} {d} {e}. kk d c -> kk e c -> Constraint
class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Lift j f)) => LeftKanLift (j :: kk d c) (f :: kk e c) where
  type Lift j f :: kk e d
  lift :: f ~> Lift j f `O` j
  liftUniv :: Ob g => (f ~> g `O` j) -> Lift j f ~> g

mapLift :: forall j f g. (LeftKanLift j f, LeftKanLift j g) => (f ~> g) -> Lift j f ~> Lift j g
mapLift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e c).
(LeftKanLift j f, LeftKanLift j g) =>
(f ~> g) -> Lift j f ~> Lift j g
mapLift f ~> g
fg = forall (j :: kk d c) (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O g j) -> Lift j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O g j) -> Lift j f ~> g
liftUniv @j (forall (j :: kk d c) (f :: kk e c).
LeftKanLift j f =>
f ~> O (Lift j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
LeftKanLift j f =>
f ~> O (Lift j f) j
lift @j (g ~> O (Lift j g) j) -> (f ~> g) -> f ~> O (Lift j g) j
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. f ~> g
fg)

rebaseLift :: forall i j f. (LeftKanLift j f, LeftKanLift i f) => (i ~> j) -> Lift j f ~> Lift i f
rebaseLift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (i :: kk d c)
       (j :: kk d c) (f :: kk e c).
(LeftKanLift j f, LeftKanLift i f) =>
(i ~> j) -> Lift j f ~> Lift i f
rebaseLift i ~> j
ij = forall (j :: kk d c) (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O g j) -> Lift j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O g j) -> Lift j f ~> g
liftUniv @j ((forall (a :: kk e d). (CategoryOf (kk e d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Lift i f) Obj (Lift i f) -> (i ~> j) -> O (Lift i f) i ~> O (Lift i f) j
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` i ~> j
ij) (O (Lift i f) i ~> O (Lift i f) j)
-> (f ~> O (Lift i f) i) -> f ~> O (Lift i f) j
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk d c) (f :: kk e c).
LeftKanLift j f =>
f ~> O (Lift j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
LeftKanLift j f =>
f ~> O (Lift j f) j
lift @i @f)


type RightKanLift :: forall {k} {kk :: CAT k} {c} {d} {e}. kk d c -> kk e c -> Constraint
class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Rift j f)) => RightKanLift (j :: kk d c) (f :: kk e c) where
  type Rift j f :: kk e d
  rift :: Rift j f `O` j ~> f
  riftUniv :: Ob g => (g `O` j ~> f) -> g ~> Rift j f

mapRift :: forall j f g. (RightKanLift j f, RightKanLift j g) => (f ~> g) -> Rift j f ~> Rift j g
mapRift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e c).
(RightKanLift j f, RightKanLift j g) =>
(f ~> g) -> Rift j f ~> Rift j g
mapRift f ~> g
fg = forall (j :: kk d c) (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O g j ~> f) -> g ~> Rift j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O g j ~> f) -> g ~> Rift j f
riftUniv @j (f ~> g
fg (f ~> g) -> (O (Rift j f) j ~> f) -> O (Rift j f) j ~> g
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk d c) (f :: kk e c).
RightKanLift j f =>
O (Rift j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O (Rift j f) j ~> f
rift @j)

rebaseRift :: forall i j f. (RightKanLift j f, RightKanLift i f) => (i ~> j) -> Rift j f ~> Rift i f
rebaseRift :: forall {k} {kk :: CAT k} {d :: k} {c :: k} {e :: k} (i :: kk d c)
       (j :: kk d c) (f :: kk e c).
(RightKanLift j f, RightKanLift i f) =>
(i ~> j) -> Rift j f ~> Rift i f
rebaseRift i ~> j
ij = forall (j :: kk d c) (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O g j ~> f) -> g ~> Rift j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O g j ~> f) -> g ~> Rift j f
riftUniv @i (forall (j :: kk d c) (f :: kk e c).
RightKanLift j f =>
O (Rift j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O (Rift j f) j ~> f
rift @j @f (O (Rift j f) j ~> f)
-> (O (Rift j f) i ~> O (Rift j f) j) -> O (Rift j f) i ~> f
forall (b :: kk e c) (c :: kk e c) (a :: kk e c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: kk e d). (CategoryOf (kk e d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Rift j f) Obj (Rift j f) -> (i ~> j) -> O (Rift j f) i ~> O (Rift j f) j
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` i ~> j
ij))


newtype HaskRan g h a = Ran { forall {k} (g :: k -> Type) (h :: k -> Type) a.
HaskRan g h a -> forall (b :: k). (a -> g b) -> h b
runRan :: forall b. (a -> g b) -> h b }
instance Functor (HaskRan g h) where
  map :: forall a b. (a ~> b) -> HaskRan g h a ~> HaskRan g h b
map a ~> b
f (Ran forall (b :: k). (a -> g b) -> h b
k) = (forall (b :: k). (b -> g b) -> h b) -> HaskRan g h b
forall {k} (g :: k -> Type) (h :: k -> Type) a.
(forall (b :: k). (a -> g b) -> h b) -> HaskRan g h a
Ran ((forall (b :: k). (b -> g b) -> h b) -> HaskRan g h b)
-> (forall (b :: k). (b -> g b) -> h b) -> HaskRan g h b
forall a b. (a -> b) -> a -> b
$ \b -> g b
g -> (a -> g b) -> h b
forall (b :: k). (a -> g b) -> h b
k (b -> g b
g (b -> g b) -> (a -> b) -> a -> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
a -> b
f)
instance (Functor j, Functor f) => RightKanExtension (MK (j :: Type -> Type)) (MK f) where
  type Ran (MK j) (MK f) = MK (HaskRan j f)
  ran :: O ('MK j) (Ran ('MK j) ('MK f)) ~> 'MK f
ran = (Compose (HaskRan j f) j ~> f)
-> Mon2 ('MK (Compose (HaskRan j f) j)) ('MK f)
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 ((Compose (HaskRan j f) j ~> f)
 -> Mon2 ('MK (Compose (HaskRan j f) j)) ('MK f))
-> (Compose (HaskRan j f) j ~> f)
-> Mon2 ('MK (Compose (HaskRan j f) j)) ('MK f)
forall a b. (a -> b) -> a -> b
$ (Compose (HaskRan j f) j .~> f) -> Nat (Compose (HaskRan j f) j) f
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \(Compose HaskRan j f (j a)
rj) -> HaskRan j f (j a) -> forall b. (j a -> j b) -> f b
forall {k} (g :: k -> Type) (h :: k -> Type) a.
HaskRan g h a -> forall (b :: k). (a -> g b) -> h b
runRan HaskRan j f (j a)
rj j a -> j a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  ranUniv :: forall (g :: MonK (Type -> Type) d e).
Ob g =>
(O ('MK j) g ~> 'MK f) -> g ~> Ran ('MK j) ('MK f)
ranUniv (Mon2 (Nat Compose (UN 'MK g) j .~> f
n)) = (UN 'MK g ~> HaskRan j f)
-> Mon2 ('MK (UN 'MK g)) ('MK (HaskRan j f))
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 ((UN 'MK g ~> HaskRan j f)
 -> Mon2 ('MK (UN 'MK g)) ('MK (HaskRan j f)))
-> (UN 'MK g ~> HaskRan j f)
-> Mon2 ('MK (UN 'MK g)) ('MK (HaskRan j f))
forall a b. (a -> b) -> a -> b
$ (UN 'MK g .~> HaskRan j f) -> Nat (UN 'MK g) (HaskRan j f)
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \UN 'MK g a
g -> (forall b. (a -> j b) -> f b) -> HaskRan j f a
forall {k} (g :: k -> Type) (h :: k -> Type) a.
(forall (b :: k). (a -> g b) -> h b) -> HaskRan g h a
Ran \a -> j b
f -> Compose (UN 'MK g) j b ~> f b
Compose (UN 'MK g) j b -> f b
Compose (UN 'MK g) j .~> f
n (UN 'MK g (j b) -> Compose (UN 'MK g) j b
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((a ~> j b) -> UN 'MK g a ~> UN 'MK g (j b)
forall a b. (a ~> b) -> UN 'MK g a ~> UN 'MK g b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> j b
a -> j b
f UN 'MK g a
g))

data HaskLan j f a where
  Lan :: (j b -> a) -> f b -> HaskLan j f a
instance Functor (HaskLan j f) where
  map :: forall a b. (a ~> b) -> HaskLan j f a ~> HaskLan j f b
map a ~> b
g (Lan j b -> a
k f b
f) = (j b -> b) -> f b -> HaskLan j f b
forall {k} (j :: k -> Type) (b :: k) a (f :: k -> Type).
(j b -> a) -> f b -> HaskLan j f a
Lan (a ~> b
a -> b
g (a -> b) -> (j b -> a) -> j b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. j b -> a
k) f b
f
instance (Functor j, Functor f) => LeftKanExtension (MK (j :: Type -> Type)) (MK f) where
  type Lan (MK j) (MK f) = MK (HaskLan j f)
  lan :: 'MK f ~> O ('MK j) (Lan ('MK j) ('MK f))
lan = (f ~> Compose (HaskLan j f) j)
-> Mon2 ('MK f) ('MK (Compose (HaskLan j f) j))
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 ((f ~> Compose (HaskLan j f) j)
 -> Mon2 ('MK f) ('MK (Compose (HaskLan j f) j)))
-> (f ~> Compose (HaskLan j f) j)
-> Mon2 ('MK f) ('MK (Compose (HaskLan j f) j))
forall a b. (a -> b) -> a -> b
$ (f .~> Compose (HaskLan j f) j) -> Nat f (Compose (HaskLan j f) j)
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (HaskLan j f (j a) -> Compose (HaskLan j f) j a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (HaskLan j f (j a) -> Compose (HaskLan j f) j a)
-> (f a -> HaskLan j f (j a)) -> f a -> Compose (HaskLan j f) j a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (j a -> j a) -> f a -> HaskLan j f (j a)
forall {k} (j :: k -> Type) (b :: k) a (f :: k -> Type).
(j b -> a) -> f b -> HaskLan j f a
Lan j a -> j a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  lanUniv :: forall (g :: MonK (Type -> Type) d e).
Ob g =>
('MK f ~> O ('MK j) g) -> Lan ('MK j) ('MK f) ~> g
lanUniv (Mon2 (Nat f .~> Compose (UN 'MK g) j
n)) = (HaskLan j f ~> UN 'MK g)
-> Mon2 ('MK (HaskLan j f)) ('MK (UN 'MK g))
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 ((HaskLan j f ~> UN 'MK g)
 -> Mon2 ('MK (HaskLan j f)) ('MK (UN 'MK g)))
-> (HaskLan j f ~> UN 'MK g)
-> Mon2 ('MK (HaskLan j f)) ('MK (UN 'MK g))
forall a b. (a -> b) -> a -> b
$ (HaskLan j f .~> UN 'MK g) -> Nat (HaskLan j f) (UN 'MK g)
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \(Lan j b -> a
k f b
f) -> (j b ~> a) -> UN 'MK g (j b) ~> UN 'MK g a
forall a b. (a ~> b) -> UN 'MK g a ~> UN 'MK g b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map j b ~> a
j b -> a
k (Compose (UN 'MK g) j b -> UN 'MK g (j b)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (f b ~> Compose (UN 'MK g) j b
f b -> Compose (UN 'MK g) j b
f .~> Compose (UN 'MK g) j
n f b
f))