Right Kan lifts

g . Rift g f => f

This could alternately be defined directly from the (co)universal propertly in which case, we'd get toRift = UniversalRift, but then the usage would suffer.

data UniversalRift g f a = forall z. Functor z =>
     UniversalRift (forall x. g (z x) -> f x) (z a)

We can witness the isomorphism between Rift and UniversalRift using:

riftIso1 :: Functor g => UniversalRift g f a -> Rift g f a
riftIso1 (UniversalRift h z) = Rift $ \g -> h $ fmap (\k -> k <$> z) g

riftIso2 :: Rift g f a -> UniversalRift g f a
riftIso2 (Rift e) = UniversalRift e id

riftIso1 (riftIso2 (Rift h)) =
riftIso1 (UniversalRift h id) =          -- by definition
Rift $ \g -> h $ fmap (\k -> k <$> id) g -- by definition
Rift $ \g -> h $ fmap id g               -- <$> = (.) and (.id)
Rift $ \g -> h g                         -- by functor law
Rift h                                   -- eta reduction

The other direction is left as an exercise for the reader.

There are several monads that we can form from Rift.

When g is corepresentable (e.g. is a right adjoint) then there exists x such that g ~ (->) x, then it follows that

Rift g g a ~
forall r. (x -> a -> r) -> x -> r ~
forall r. (a -> x -> r) -> x -> r ~
forall r. (a -> g r) -> g r ~
Codensity g r

When f is a left adjoint, so that f -| g then

Rift f f a ~
forall r. f (a -> r) -> f r ~
forall r. (a -> r) -> g (f r) ~
forall r. (a -> r) -> Adjoint f g r ~
Yoneda (Adjoint f g r)

An alternative way to view that is to note that whenever f is a left adjoint then f -| Rift f Identity, and since Rift f f is isomorphic to Rift f Identity (f a), this is the Monad formed by the adjunction.

Rift Identity m can be a Monad for any Monad m, as it is isomorphic to Yoneda m.

The universal property of Rift

When f -| u, then f -| Rift f Identity and

toRift . fromRift ≡ id
fromRift . toRift ≡ id

composeRift . decomposeRift ≡ id
decomposeRift . composeRift ≡ id

Rift f Identity a is isomorphic to the right adjoint to f if one exists.

adjointToRift . riftToAdjoint ≡ id
riftToAdjoint . adjointToRift ≡ id

Rift f Identity a is isomorphic to the right adjoint to f if one exists.

Rift f h a is isomorphic to the post-composition of the right adjoint of f onto h if such a right adjoint exists.

Rift f h a is isomorphic to the post-composition of the right adjoint of f onto h if such a right adjoint exists.

riftToComposedAdjoint . composedAdjointToRift ≡ id
composedAdjointToRift . riftToComposedAdjoint ≡ id

The natural isomorphism between f and Rift f f. lowerRift . liftRift ≡ id liftRift . lowerRift ≡ id

lowerRift (liftRift x)     -- definition
lowerRift (Rift (<*> x))   -- definition
(<*> x) (pure id)          -- beta reduction
pure id <*> x              -- Applicative identity law
x

Lower Rift by applying pure id to the continuation.

See liftRift.

Indexed applicative composition of right Kan lifts.