{-# LANGUAGE AllowAmbiguousTypes #-} module Proarrow.Category.Bicategory.Prof where import Data.Kind (Constraint) import Prelude (($)) import Proarrow.Category.Bicategory (Bicategory(..), Monad(..), Bimodule(..), Adjunction(..)) import Proarrow.Category.Bicategory.Kan (RightKanExtension(..), RightKanLift (..)) import Proarrow.Core (PRO, CategoryOf(..), Profunctor(..), (:~>), CAT, Promonad (..), dimapDefault, lmap, rmap, UN, Is, arr, IsCategoryOf, (//)) import Proarrow.Profunctor.Representable (Representable) import Proarrow.Profunctor.Corepresentable (Corepresentable) import Proarrow.Category.Instance.Prof () import Proarrow.Profunctor.Composition ((:.:)(..)) import Proarrow.Object (src, tgt) import Proarrow.Adjunction qualified as A import Proarrow.Profunctor.Ran qualified as R import Proarrow.Profunctor.Rift qualified as R import Proarrow.Category.Opposite (OPPOSITE(..)) type data ProfCl = ProfC | ProfRepC | ProfCorepC type family ProfConstraint (cl :: ProfCl) :: PRO j k -> Constraint type instance ProfConstraint ProfC = Profunctor type instance ProfConstraint ProfRepC = Representable type instance ProfConstraint ProfCorepC = Corepresentable type data ProfK (cl :: ProfCl) j k = PK (PRO j k) type instance UN PK (PK p) = p type PROFK = ProfK ProfC type Prof :: CAT (ProfK cl j k) data Prof p q where Prof :: (Ob p, Ob q) => UN PK p :~> UN PK q -> Prof p q instance Profunctor Prof where dimap :: forall (c :: ProfK cl j k) (a :: ProfK cl j k) (b :: ProfK cl j k) (d :: ProfK cl j k). (c ~> a) -> (b ~> d) -> Prof a b -> Prof c d dimap = (c ~> a) -> (b ~> d) -> Prof a b -> Prof c d Prof c a -> Prof b d -> Prof a b -> Prof c d forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k). Promonad p => p c a -> p b d -> p a b -> p c d dimapDefault (Ob a, Ob b) => r r \\ :: forall (a :: ProfK cl j k) (b :: ProfK cl j k) r. ((Ob a, Ob b) => r) -> Prof a b -> r \\ Prof UN PK a :~> UN PK b n = r (Ob (UN PK a Any Any), Ob (UN PK b Any Any)) => r (Ob a, Ob b) => r r ((Ob (UN PK a Any Any), Ob (UN PK b Any Any)) => r) -> (UN PK a Any Any -> UN PK b Any Any) -> r forall a b r. ((Ob a, Ob b) => r) -> (a -> b) -> r forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r. Profunctor p => ((Ob a, Ob b) => r) -> p a b -> r \\ UN PK a Any Any -> UN PK b Any Any UN PK a :~> UN PK b n instance Promonad Prof where id :: forall (a :: ProfK cl j k). Ob a => Prof a a id = (UN PK a :~> UN PK a) -> Prof a a forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof UN PK a a b -> UN PK a a b UN PK a :~> UN PK a forall a. Ob a => a -> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id Prof UN PK b :~> UN PK c m . :: forall (b :: ProfK cl j k) (c :: ProfK cl j k) (a :: ProfK cl j k). Prof b c -> Prof a b -> Prof a c . Prof UN PK a :~> UN PK b n = (UN PK a :~> UN PK c) -> Prof a c forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof (UN PK b a b -> UN PK c a b UN PK b :~> UN PK c m (UN PK b a b -> UN PK c a b) -> (UN PK a a b -> UN PK b a b) -> UN PK a a b -> UN PK c a 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 . UN PK a a b -> UN PK b a b UN PK a :~> UN PK b n) instance CategoryOf (ProfK cl j k) where type (~>) = Prof type Ob @(ProfK cl j k) p = (Is PK p, Profunctor (UN PK p), ProfConstraint cl (UN PK p), ProfConstraint cl ((~>) @j), ProfConstraint cl ((~>) @k)) class ProfConstraint cl (p :.: q) => ComposeConstraint cl i j k (p :: PRO i j) (q :: PRO j k) instance ProfConstraint cl (p :.: q) => ComposeConstraint cl i j k (p :: PRO i j) (q :: PRO j k) instance (forall i j k (p :: PRO i j) (q :: PRO j k). (ProfConstraint cl p, ProfConstraint cl q) => ComposeConstraint cl i j k p q) => Bicategory (ProfK cl) where type Ob0 (ProfK cl) k = (CategoryOf k, ProfConstraint cl ((~>) :: CAT k)) type I = PK (~>) type p `O` q = PK (UN PK p :.: UN PK q) Prof UN PK a :~> UN PK b m o :: forall {k1} i j (a :: ProfK cl i j) (b :: ProfK cl i j) (c :: ProfK cl j k1) (d :: ProfK cl j k1). (a ~> b) -> (c ~> d) -> O a c ~> O b d `o` Prof UN PK c :~> UN PK d n = (UN PK (PK (UN PK a :.: UN PK c)) :~> UN PK (PK (UN PK b :.: UN PK d))) -> Prof (PK (UN PK a :.: UN PK c)) (PK (UN PK b :.: UN PK d)) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof ((UN PK (PK (UN PK a :.: UN PK c)) :~> UN PK (PK (UN PK b :.: UN PK d))) -> Prof (PK (UN PK a :.: UN PK c)) (PK (UN PK b :.: UN PK d))) -> (UN PK (PK (UN PK a :.: UN PK c)) :~> UN PK (PK (UN PK b :.: UN PK d))) -> Prof (PK (UN PK a :.: UN PK c)) (PK (UN PK b :.: UN PK d)) forall a b. (a -> b) -> a -> b $ \(UN PK a a b p :.: UN PK c b b q) -> UN PK a a b -> UN PK b a b UN PK a :~> UN PK b m UN PK a a b p UN PK b a b -> UN PK d b b -> (:.:) (UN PK b) (UN PK d) a b forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k) (c :: k). p a b -> q b c -> (:.:) p q a c :.: UN PK c b b -> UN PK d b b UN PK c :~> UN PK d n UN PK c b b q (Ob0 (ProfK cl) i, Ob0 (ProfK cl) j, Ob ps, Ob qs) => r r \\\ :: forall i j (ps :: ProfK cl i j) (qs :: ProfK cl i j) r. ((Ob0 (ProfK cl) i, Ob0 (ProfK cl) j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r \\\ Prof{} = r (Ob0 (ProfK cl) i, Ob0 (ProfK cl) j, Ob ps, Ob qs) => r r leftUnitor :: forall i j (a :: ProfK cl i j). Obj a -> O I a ~> a leftUnitor Prof{} = (UN PK (PK ((~>) :.: UN PK a)) :~> UN PK (PK (UN PK a))) -> Prof (PK ((~>) :.: UN PK a)) (PK (UN PK a)) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof ((UN PK (PK ((~>) :.: UN PK a)) :~> UN PK (PK (UN PK a))) -> Prof (PK ((~>) :.: UN PK a)) (PK (UN PK a))) -> (UN PK (PK ((~>) :.: UN PK a)) :~> UN PK (PK (UN PK a))) -> Prof (PK ((~>) :.: UN PK a)) (PK (UN PK a)) forall a b. (a -> b) -> a -> b $ \(a ~> b h :.: UN PK a b b q) -> (a ~> b) -> UN PK a b b -> UN PK a a b forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k). Profunctor p => (c ~> a) -> p a b -> p c b lmap a ~> b h UN PK a b b q leftUnitorInv :: forall i j (a :: ProfK cl i j). Obj a -> a ~> O I a leftUnitorInv Prof{} = (UN PK (PK (UN PK a)) :~> UN PK (PK ((~>) :.: UN PK a))) -> Prof (PK (UN PK a)) (PK ((~>) :.: UN PK a)) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof ((UN PK (PK (UN PK a)) :~> UN PK (PK ((~>) :.: UN PK a))) -> Prof (PK (UN PK a)) (PK ((~>) :.: UN PK a))) -> (UN PK (PK (UN PK a)) :~> UN PK (PK ((~>) :.: UN PK a))) -> Prof (PK (UN PK a)) (PK ((~>) :.: UN PK a)) forall a b. (a -> b) -> a -> b $ \UN PK (PK (UN PK a)) a b p -> UN PK a a b -> a ~> a forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src UN PK a a b UN PK (PK (UN PK a)) a b p (a ~> a) -> UN PK a a b -> (:.:) (~>) (UN PK a) a b forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k) (c :: k). p a b -> q b c -> (:.:) p q a c :.: UN PK a a b UN PK (PK (UN PK a)) a b p rightUnitor :: forall i j (a :: ProfK cl i j). Obj a -> O a I ~> a rightUnitor Prof{} = (UN PK (PK (UN PK a :.: (~>))) :~> UN PK (PK (UN PK a))) -> Prof (PK (UN PK a :.: (~>))) (PK (UN PK a)) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof ((UN PK (PK (UN PK a :.: (~>))) :~> UN PK (PK (UN PK a))) -> Prof (PK (UN PK a :.: (~>))) (PK (UN PK a))) -> (UN PK (PK (UN PK a :.: (~>))) :~> UN PK (PK (UN PK a))) -> Prof (PK (UN PK a :.: (~>))) (PK (UN PK a)) forall a b. (a -> b) -> a -> b $ \(UN PK a a b p :.: b ~> b h) -> (b ~> b) -> UN PK a a b -> UN PK a a b forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j). Profunctor p => (b ~> d) -> p a b -> p a d rmap b ~> b h UN PK a a b p rightUnitorInv :: forall i j (a :: ProfK cl i j). Obj a -> a ~> O a I rightUnitorInv Prof{} = (UN PK (PK (UN PK a)) :~> UN PK (PK (UN PK a :.: (~>)))) -> Prof (PK (UN PK a)) (PK (UN PK a :.: (~>))) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof ((UN PK (PK (UN PK a)) :~> UN PK (PK (UN PK a :.: (~>)))) -> Prof (PK (UN PK a)) (PK (UN PK a :.: (~>)))) -> (UN PK (PK (UN PK a)) :~> UN PK (PK (UN PK a :.: (~>)))) -> Prof (PK (UN PK a)) (PK (UN PK a :.: (~>))) forall a b. (a -> b) -> a -> b $ \UN PK (PK (UN PK a)) a b p -> UN PK a a b UN PK (PK (UN PK a)) a b p UN PK a a b -> (b ~> b) -> (:.:) (UN PK a) (~>) a b forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k) (c :: k). p a b -> q b c -> (:.:) p q a c :.: UN PK a a b -> b ~> b forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt UN PK a a b UN PK (PK (UN PK a)) a b p associator :: forall {j1} {k1} i j2 (a :: ProfK cl i j2) (b :: ProfK cl j2 j1) (c :: ProfK cl j1 k1). Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c) associator Prof{} Prof{} Prof{} = (UN PK (PK ((UN PK a :.: UN PK b) :.: UN PK c)) :~> UN PK (PK (UN PK a :.: (UN PK b :.: UN PK c)))) -> Prof (PK ((UN PK a :.: UN PK b) :.: UN PK c)) (PK (UN PK a :.: (UN PK b :.: UN PK c))) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof ((UN PK (PK ((UN PK a :.: UN PK b) :.: UN PK c)) :~> UN PK (PK (UN PK a :.: (UN PK b :.: UN PK c)))) -> Prof (PK ((UN PK a :.: UN PK b) :.: UN PK c)) (PK (UN PK a :.: (UN PK b :.: UN PK c)))) -> (UN PK (PK ((UN PK a :.: UN PK b) :.: UN PK c)) :~> UN PK (PK (UN PK a :.: (UN PK b :.: UN PK c)))) -> Prof (PK ((UN PK a :.: UN PK b) :.: UN PK c)) (PK (UN PK a :.: (UN PK b :.: UN PK c))) forall a b. (a -> b) -> a -> b $ \((UN PK a a b p :.: UN PK b b b q) :.: UN PK c b b r) -> UN PK a a b p UN PK a a b -> (:.:) (UN PK b) (UN PK c) b b -> (:.:) (UN PK a) (UN PK b :.: UN PK c) a b forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k) (c :: k). p a b -> q b c -> (:.:) p q a c :.: (UN PK b b b q UN PK b b b -> UN PK c b b -> (:.:) (UN PK b) (UN PK c) b b forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k) (c :: k). p a b -> q b c -> (:.:) p q a c :.: UN PK c b b r) associatorInv :: forall {j1} {k1} i j2 (a :: ProfK cl i j2) (b :: ProfK cl j2 j1) (c :: ProfK cl j1 k1). Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c associatorInv Prof{} Prof{} Prof{} = (UN PK (PK (UN PK a :.: (UN PK b :.: UN PK c))) :~> UN PK (PK ((UN PK a :.: UN PK b) :.: UN PK c))) -> Prof (PK (UN PK a :.: (UN PK b :.: UN PK c))) (PK ((UN PK a :.: UN PK b) :.: UN PK c)) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof ((UN PK (PK (UN PK a :.: (UN PK b :.: UN PK c))) :~> UN PK (PK ((UN PK a :.: UN PK b) :.: UN PK c))) -> Prof (PK (UN PK a :.: (UN PK b :.: UN PK c))) (PK ((UN PK a :.: UN PK b) :.: UN PK c))) -> (UN PK (PK (UN PK a :.: (UN PK b :.: UN PK c))) :~> UN PK (PK ((UN PK a :.: UN PK b) :.: UN PK c))) -> Prof (PK (UN PK a :.: (UN PK b :.: UN PK c))) (PK ((UN PK a :.: UN PK b) :.: UN PK c)) forall a b. (a -> b) -> a -> b $ \(UN PK a a b p :.: (UN PK b b b q :.: UN PK c b b r)) -> (UN PK a a b p UN PK a a b -> UN PK b b b -> (:.:) (UN PK a) (UN PK b) a b forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k) (c :: k). p a b -> q b c -> (:.:) p q a c :.: UN PK b b b q) (:.:) (UN PK a) (UN PK b) a b -> UN PK c b b -> (:.:) (UN PK a :.: UN PK b) (UN PK c) a b forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k) (c :: k). p a b -> q b c -> (:.:) p q a c :.: UN PK c b b r instance Promonad p => Monad (PK p :: PROFK k k) where eta :: I ~> PK p eta = (UN PK (PK (~>)) :~> UN PK (PK p)) -> Prof (PK (~>)) (PK p) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof UN PK (PK (~>)) a b -> UN PK (PK p) a b (a ~> b) -> p a b UN PK (PK (~>)) :~> UN PK (PK p) forall {k} (p :: PRO k k) (a :: k) (b :: k). Promonad p => (a ~> b) -> p a b arr mu :: O (PK p) (PK p) ~> PK p mu = (UN PK (PK (p :.: p)) :~> UN PK (PK p)) -> Prof (PK (p :.: p)) (PK p) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof \(p a b p :.: p b b q) -> p b b q p b b -> p a b -> p a b forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p 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 . p a b p instance (IsCategoryOf j cj, IsCategoryOf k ck, Profunctor p) => Bimodule (PK cj) (PK ck) (PK p :: PROFK j k) where leftAction :: O (PK cj) (PK p) ~> PK p leftAction = (UN PK (PK (cj :.: p)) :~> UN PK (PK p)) -> Prof (PK (cj :.: p)) (PK p) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof \(cj a b f :.: p b b p) -> (a ~> b) -> p b b -> p a b forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k). Profunctor p => (c ~> a) -> p a b -> p c b lmap cj a b a ~> b f p b b p rightAction :: O (PK p) (PK ck) ~> PK p rightAction = (UN PK (PK (p :.: ck)) :~> UN PK (PK p)) -> Prof (PK (p :.: ck)) (PK p) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof \(p a b p :.: ck b b f) -> (b ~> b) -> p a b -> p a b forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j). Profunctor p => (b ~> d) -> p a b -> p a d rmap ck b b b ~> b f p a b p instance (A.Adjunction l r) => Adjunction (PK l :: PROFK c d) (PK r) where unit :: I ~> O (PK r) (PK l) unit = (UN PK (PK (~>)) :~> UN PK (PK (r :.: l))) -> Prof (PK (~>)) (PK (r :.: l)) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof \UN PK (PK (~>)) a b f -> (a ~> b) -> (:.:) r l b b -> (:.:) r l a b forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k). Profunctor p => (c ~> a) -> p a b -> p c b lmap UN PK (PK (~>)) a b a ~> b f (:.:) r l b b forall (a :: d). Ob a => (:.:) r l a a forall {j} {k} (p :: PRO k j) (q :: PRO j k) (a :: j). (Adjunction p q, Ob a) => (:.:) q p a a A.unit ((Ob a, Ob b) => (:.:) r l a b) -> (a ~> b) -> (:.:) r l a b forall (a :: d) (b :: d) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r. Profunctor p => ((Ob a, Ob b) => r) -> p a b -> r \\ UN PK (PK (~>)) a b a ~> b f counit :: O (PK l) (PK r) ~> I counit = (UN PK (PK (l :.: r)) :~> UN PK (PK (~>))) -> Prof (PK (l :.: r)) (PK (~>)) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof UN PK (PK (l :.: r)) a b -> UN PK (PK (~>)) a b (:.:) l r a b -> a ~> b UN PK (PK (l :.: r)) :~> UN PK (PK (~>)) (l :.: r) :~> (~>) forall {j} {k} (p :: PRO k j) (q :: PRO j k). Adjunction p q => (p :.: q) :~> (~>) A.counit instance (Profunctor f, Profunctor j) => RightKanExtension (PK j :: PROFK c d) (PK f :: PROFK c e) where type Ran (PK j) (PK f) = PK (R.Ran (OP j) f) ran :: O (PK j) (Ran (PK j) (PK f)) ~> PK f ran = (UN PK (PK (j :.: Ran ('OP j) f)) :~> UN PK (PK f)) -> Prof (PK (j :.: Ran ('OP j) f)) (PK f) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof \(j a b j :.: Ran ('OP j) f b b r) -> j a b -> Ran ('OP j) f b b -> f a b forall {i} {j1} {k} (j2 :: PRO i j1) (x :: i) (a :: j1) (p :: PRO i k) (b :: k). Profunctor j2 => j2 x a -> Ran ('OP j2) p a b -> p x b R.runRan j a b j Ran ('OP j) f b b r ranUniv :: forall (g :: ProfK ProfC d e). Ob g => (O (PK j) g ~> PK f) -> g ~> Ran (PK j) (PK f) ranUniv (Prof UN PK (PK (j :.: UN PK g)) :~> UN PK (PK f) n) = (UN PK (PK (UN PK g)) :~> UN PK (PK (Ran ('OP j) f))) -> Prof (PK (UN PK g)) (PK (Ran ('OP j) f)) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof \UN PK (PK (UN PK g)) a b g -> UN PK g a b UN PK (PK (UN PK g)) a b g UN PK g a b -> ((Ob a, Ob b) => Ran ('OP j) f a b) -> Ran ('OP j) f a b forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r // (forall (x :: c). Ob x => j x a -> f x b) -> Ran ('OP j) f a b forall {j} {k} {i} (a :: j) (b :: k) (j2 :: PRO i j) (p :: PRO i k). (Ob a, Ob b) => (forall (x :: i). Ob x => j2 x a -> p x b) -> Ran ('OP j2) p a b R.Ran \j x a j -> UN PK (PK (j :.: UN PK g)) x b -> UN PK (PK f) x b UN PK (PK (j :.: UN PK g)) :~> UN PK (PK f) n (j x a j j x a -> UN PK g a b -> (:.:) j (UN PK g) x b forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k) (c :: k). p a b -> q b c -> (:.:) p q a c :.: UN PK g a b UN PK (PK (UN PK g)) a b g) instance (Profunctor f, Profunctor j) => RightKanLift (PK j :: PROFK d c) (PK f :: PROFK e c) where type Rift (PK j) (PK f) = PK (R.Rift (OP j) f) rift :: O (Rift (PK j) (PK f)) (PK j) ~> PK f rift = (UN PK (PK (Rift ('OP j) f :.: j)) :~> UN PK (PK f)) -> Prof (PK (Rift ('OP j) f :.: j)) (PK f) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof \(Rift ('OP j) f a b r :.: j b b j) -> j b b -> Rift ('OP j) f a b -> f a b forall {k} {i} {j1} (j2 :: PRO k i) (b :: k) (x :: i) (p :: PRO j1 i) (a :: j1). Profunctor j2 => j2 b x -> Rift ('OP j2) p a b -> p a x R.runRift j b b j Rift ('OP j) f a b r riftUniv :: forall (g :: ProfK ProfC e d). Ob g => (O g (PK j) ~> PK f) -> g ~> Rift (PK j) (PK f) riftUniv (Prof UN PK (PK (UN PK g :.: j)) :~> UN PK (PK f) n) = (UN PK (PK (UN PK g)) :~> UN PK (PK (Rift ('OP j) f))) -> Prof (PK (UN PK g)) (PK (Rift ('OP j) f)) forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN PK p :~> UN PK q) -> Prof p q Prof \UN PK (PK (UN PK g)) a b g -> UN PK g a b UN PK (PK (UN PK g)) a b g UN PK g a b -> ((Ob a, Ob b) => Rift ('OP j) f a b) -> Rift ('OP j) f a b forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r // (forall (x :: c). Ob x => j b x -> f a x) -> Rift ('OP j) f a b forall {j} {k} {i} (a :: j) (b :: k) (j2 :: PRO k i) (p :: PRO j i). (Ob a, Ob b) => (forall (x :: i). Ob x => j2 b x -> p a x) -> Rift ('OP j2) p a b R.Rift \j b x j -> UN PK (PK (UN PK g :.: j)) a x -> UN PK (PK f) a x UN PK (PK (UN PK g :.: j)) :~> UN PK (PK f) n (UN PK g a b UN PK (PK (UN PK g)) a b g UN PK g a b -> j b x -> (:.:) (UN PK g) j a x forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k) (c :: k). p a b -> q b c -> (:.:) p q a c :.: j b x j)