{-# LANGUAGE DataKinds, RankNTypes, GADTs #-}
module Data.Functor.Kan.Square where
import Data.Square
import Data.Profunctor
import Data.Profunctor.Composition
import Data.Functor.Compose.List
import Data.Functor.Kan.Lan
import Data.Functor.Kan.Ran
lanSquare :: Functor f => Square '[] '[] '[f] '[j, Lan j f]
lanSquare :: forall (f :: * -> *) (j :: * -> *).
Functor f =>
Square '[] '[] '[f] '[j, Lan j f]
lanSquare = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
(gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
Profunctor (PList qs)) =>
(forall a b.
PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare forall a b. (a -> b) -> a -> b
$ \PlainP '[] a b
k -> forall {k} (h :: k -> *) (a :: k) (g :: k -> *).
h a -> Lan g h (g a)
glan forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlainP '[] a b
k
lanFactor :: Functor g => Square '[] '[] '[f] '[j, g] -> Square '[] '[] '[Lan j f] '[g]
lanFactor :: forall (g :: * -> *) (f :: * -> *) (j :: * -> *).
Functor g =>
Square '[] '[] '[f] '[j, g] -> Square '[] '[] '[Lan j f] '[g]
lanFactor Square '[] '[] '[f] '[j, g]
sq = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
(gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
Profunctor (PList qs)) =>
(forall a b.
PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare forall a b. (a -> b) -> a -> b
$ \PlainP '[] a b
k -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlainP '[] a b
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: * -> *) (h :: k -> *) (g :: k -> *) b.
Functor f =>
(forall (a :: k). h a -> f (g a)) -> Lan g h b -> f b
toLan (forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
(gs :: [* -> *]) a b.
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
Profunctor (PList qs)) =>
Square ps qs fs gs
-> PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b)
runSquare Square '[] '[] '[f] '[j, g]
sq forall a. a -> a
id)
ranSquare :: Functor g => Square '[] '[] '[j, Ran j g] '[g]
ranSquare :: forall (g :: * -> *) (j :: * -> *).
Functor g =>
Square '[] '[] '[j, Ran j g] '[g]
ranSquare = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
(gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
Profunctor (PList qs)) =>
(forall a b.
PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare forall a b. (a -> b) -> a -> b
$ \PlainP '[] a b
k -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlainP '[] a b
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (g :: k -> *) (h :: k -> *) (a :: k).
Ran g h (g a) -> h a
gran
ranFactor :: Functor f => Square '[] '[] '[j, f] '[g] -> Square '[] '[] '[f] '[Ran j g]
ranFactor :: forall (f :: * -> *) (j :: * -> *) (g :: * -> *).
Functor f =>
Square '[] '[] '[j, f] '[g] -> Square '[] '[] '[f] '[Ran j g]
ranFactor Square '[] '[] '[j, f] '[g]
sq = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
(gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
Profunctor (PList qs)) =>
(forall a b.
PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare forall a b. (a -> b) -> a -> b
$ \PlainP '[] a b
k -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlainP '[] a b
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (k2 :: * -> *) (g :: k1 -> *) (h :: k1 -> *) b.
Functor k2 =>
(forall (a :: k1). k2 (g a) -> h a) -> k2 b -> Ran g h b
toRan (forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
(gs :: [* -> *]) a b.
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
Profunctor (PList qs)) =>
Square ps qs fs gs
-> PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b)
runSquare Square '[] '[] '[j, f] '[g]
sq forall a. a -> a
id)