{-# 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))